-
Notifications
You must be signed in to change notification settings - Fork 380
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
[ doc ] Improve docs for let and := #3159
base: main
Are you sure you want to change the base?
Conversation
:doc `(:=)` was not very helpful. This has now been expanded, and the expanded version lifted out to its own string so as to be (re)used in both `:=` and `let`'s documentation. With thanks to skykanin, buzden, gallais, and MithicSpirit on Discord for inspiration to refactor these docs and explaining the bits I weren't clear on.
src/Idris/Doc/Keywords.idr
Outdated
in square * square | ||
``` | ||
Here, `square` will only be computed once instead of every time (which might | ||
have happened had we used `=` instead of `:=`). |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I may misunderstand the wording, but this gives an impression that =
instead of :=
is enough.
let x = val in e
and
let x := val in e
are absolutely the same, where
let x : _
x = val
in e
may be different (i.e. reevaluate)
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Ah no that's absolutely my own misunderstanding; I thought =
and :=
were always different, not just when used with a type annotation. I'll correct that : )
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I think I've now correctly described the behaviour? : )
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I thought
=
and:=
were always different, not just when used with a type annotation
Historically, as far as I remember, :=
-syntax was added to be able to disambiguate expressions like let x : a = b = <equality-providing-expresion> in ...
The type annotation matters for those two, it turns out.
src/Idris/Doc/Keywords.idr
Outdated
in square * square | ||
``` | ||
Without the type annotation, `:=` behaves the same as `=` and gets | ||
elaborated to the lambda expression `(\square => square * square) n * n`. |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
You need brackets around n * n
here, function application has more priority than *
operator
src/Idris/Doc/Keywords.idr
Outdated
Let bindings will not unfold in the type of subsequent terms so may not be | ||
appropriate in all cases. |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
As far as I understand what you mean by this is that let bindings do not reduce to their values, unlike functions. They won't reduce not only in types, but, say, in rewrite
expressions and other stuff that needs reducing the expressions, so the wording should be generalised, I think.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I agree with that. I have run into this myself, and did not understand what was happening.
src/Idris/Doc/Keywords.idr
Outdated
elaborated to the lambda expression `(\square => square * square) n * n`. | ||
With the type annotation, `square` is the value of a computation, not its | ||
generalisation, and so will only be computed once instead of potentially on | ||
every reference. |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Nit: either wrap to so same paragraph, or put a blank line between statements.
Thanks for doing this. I am not officially a contributor here, but it gets my vote. |
Based on feedback from buzden and emdash. Thank you both for looking things through! : )
src/Idris/Doc/Keywords.idr
Outdated
Without the type annotation, `:=` behaves the same as `=` and gets | ||
elaborated to the lambda expression `(\square => square * square) (n * n)`. | ||
|
||
With the type annotation, `square` is the value of a computation, not its | ||
generalisation, and so will only be computed once instead of potentially on | ||
every reference. |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I don't understand these paragraphs
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I've attempted a clarification in the latest commit. Does that help? : )
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
It makes sense to me. I'd be inclined to ship this, as it's better than the current help text. But it's not up to me.
One thing I would like more clarification on is how the two forms might affect type inference. I.e. certain things work with one form or the other, and that can be quite surprising. I still don't have a good intuition for this. But maybe this could be a separate change?
|
In the first example, the type annotation is omitted and so `:=` gets | ||
elaborated to the lambda expression `(\square => square * square) (n * n)`. | ||
|
||
The second example does have a type annotation and as a result, `square` | ||
gets computed rather than lambda-abstracted, meaning the result will be | ||
reused on reference, instead of potentially being recomputed every time. |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I don't think that's true. The code for parsing let bindings is as follows:
letBinder : Rule LetBinder
letBinder = do s <- bounds (MkPair <$> multiplicity fname <*> expr plhs fname indents)
(rig, pat) <- pure s.val
ty <- option (PImplicit (virtualiseFC $ boundToFC fname s))
(decoratedSymbol fname ":" *> typeExpr (pnoeq pdef) fname indents)
(decoratedSymbol fname "=" <|> decoratedSymbol fname ":=")
val <- typeExpr pnowith fname indents
alts <- block (patAlt fname)
pure (MkLetBinder rig pat ty val alts)
As you can see if there is no type annotation, we replace it with a hole.
And so computationally the two expressions are the same.
Description
Prompted by discussion on the Discord: there was confusion as to when computations would be re-evaluated, whether type annotations made a difference (and when), the difference between
let
with=
and with:=
.The string for
:doc (:=)
was not very helpful; only a single line mentioning what the symbol could be used for. This has now been expanded, and the expanded version lifted out to its own string so as to be (re)used in both:=
andlet
's documentation.Should this change go in the CHANGELOG?
implementation, I have updated
CHANGELOG.md
(and potentially alsoCONTRIBUTORS.md
).