Skip to content
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

Open
wants to merge 6 commits into
base: main
Choose a base branch
from
Open
Show file tree
Hide file tree
Changes from 2 commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
1 change: 1 addition & 0 deletions CHANGELOG.md
Original file line number Diff line number Diff line change
Expand Up @@ -314,6 +314,7 @@
* Updates the docs for `envvars` to categorise when environment variables are
used (runtime, build-time, or both).
* Fixed build failure occuring when `make -j` is in effect.
* Improved the docs for `let` and `:=` to (hopefully) avoid confusion.

## v0.6.0

Expand Down
96 changes: 76 additions & 20 deletions src/Idris/Doc/Keywords.idr
Original file line number Diff line number Diff line change
Expand Up @@ -505,31 +505,69 @@ withabstraction = vcat $
```
"""]

letbinding : Doc IdrisDocAnn
letbinding = vcat $
-- to keep docs consistent between `:doc let` and `:doc (:=)`
letBinding : String
letBinding =
"""
* Let bindings are defined using the `:=` syntax and can be used to bind the
result of intermediate computations. A type annotation can be added but is
not required, for example:
```idris
power4 : Nat -> Nat
power4 n = let square := n * n
in square * square

power4T : Nat -> Nat
power4T n = let square : Nat := n * n
in square * square
```
Without the type annotation, `:=` behaves the same as `=` and gets
elaborated to the lambda expression `(\square => square * square) n * n`.
Copy link
Contributor

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

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.
Copy link

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.

Let bindings will not unfold in the type of subsequent terms so may not be
appropriate in all cases.
Copy link
Contributor

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.

Copy link

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.

"""

letKeyword : Doc IdrisDocAnn
letKeyword = vcat $
header "Let binding" :: ""
:: map (indent 2) [
"""
The `let` keyword is used for both local definitions and let bindings.
Local definitions are just like top-level definitions except that they are
defined in whatever extended context is available at the definition site.

Let bindings can be used to bind the result of intermediate computations.
They do not necessitate but can have a type annotation. They will not unfold
in the type of subsequent terms so may not be appropriate in all cases.
NOTE: We distinguish between "local let" (local definitions) and let
bindings, as well as between function definitions and values.

For instance, in the following definition the let-bound value `square`
ensures that `n * n` is only computed once:
* Local definitions are effectively lambdas, that is the expression
```idris
power4 : Nat -> Nat
power4 n = let square := n * n in square * square
let a = foo in b
```
is equivalent to
```idris
(\a => b) foo
```

It is also possible to pattern-match on the result of the intermediate
computation. The main pattern is written in place of the variable and
an alternative list of clauses can be given using the `|` separator.
For instance, we can shortcut the `square * square` computation in case
the returned value is 0 like so:
\{letBinding}

* Local function definitions allow for more complex computational behaviour,
and are defined in a similar manner to local definitions, with the addition
of annotating the `let`-expression with a type. For example:
```idris
let bar : Nat -> Nat -> Nat
bar k n = k * n + k
in e
```
Local definitions are just like top-level definitions except that they are
defined in whatever extended context is available at the definition site.
Be careful that if `e` uses `bar` multiple times, and `bar` is an expensive
computation, this may lead to `bar` being evaluated every time. Consider
using a "proper" let binding (`:=`) instead, if possible.

* Finally, it is also possible to pattern-match on the result of the
intermediate computation. The main pattern is written in place of the
variable and an alternative list of clauses can be given using the `|`
separator. For instance, we can shortcut the `square * square` computation
in case the returned value is 0 like so:
```idris
power4 : Nat -> Nat
power4 n = let square@(S _) := n * n
Expand All @@ -543,7 +581,7 @@ keywordsDoc =
"data" ::= datatypes
:: "module" ::= "Keyword to start a module definition"
:: "where" ::= whereblock
:: "let" ::= letbinding
:: "let" ::= letKeyword
:: "in" ::= "Used by `let` and `rewrite`. See either of them for more details."
:: "do" ::= doblock
:: "record" ::= recordtypes
Expand Down Expand Up @@ -699,6 +737,24 @@ recordUpdate = vcat $ header "Record updates" :: ""
"""
]

letOrRecord : Doc IdrisDocAnn
letOrRecord = vcat $
header "Let binding or record assignment"
CodingCellist marked this conversation as resolved.
Show resolved Hide resolved
:: ""
:: map (indent 2) [
"""
\{letBinding}


* Record assignment uses `:=` to assign individual fields to a new value.
CodingCellist marked this conversation as resolved.
Show resolved Hide resolved
For example, given a record `r` with a field `name` of type `String`, we can
reassign the value of the field using `:=` with the following syntax:
```idris
r = { name := "Olwyn Griffiths" } r
```
"""
]

symbolsDoc : All DocFor (Source.symbols ++ Source.reservedInfixSymbols)
symbolsDoc
= "," ::= ""
Expand All @@ -715,7 +771,7 @@ symbolsDoc
declares a new toplevel definition `id` of type `a -> a`.
"""
:: "=" ::= "Definition or equality type"
:: ":=" ::= "Let binding or record assignment"
:: ":=" ::= letOrRecord -- "Let binding or record assignment"
:: "$=" ::= recordUpdate
:: "|" ::= "Additional patterns showing up in a `with` clause"
:: "|||" ::= "Document string attached to the following definition"
Expand Down
Loading