[ doc ] Improve docs for let and :=

[CodingCellist]

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 := and let's documentation.

Should this change go in the CHANGELOG?

• If this is a fix, user-facing change, a compiler change, or a new paper
  implementation, I have updated CHANGELOG.md (and potentially also
  CONTRIBUTORS.md).

[buzden]

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)

[CodingCellist]

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 : )

[CodingCellist]

I think I've now correctly described the behaviour? : )

[buzden]

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

[buzden]

You need brackets around n * n here, function application has more priority than * operator

[buzden]

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.

[emdash]

I agree with that. I have run into this myself, and did not understand what was happening.

[emdash]

Nit: either wrap to so same paragraph, or put a blank line between statements.

[emdash]

Thanks for doing this. I am not officially a contributor here, but it gets my vote.

[CodingCellist]

@emdash @buzden, thank you both for looking this over! I think I've incorporated the feedback, let me know what yous think (after the holidays if you're away; please don't take time away from a break to look at this) : )

[gallais]

I don't understand these paragraphs

[CodingCellist]

I've attempted a clarification in the latest commit. Does that help? : )

[emdash]

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?

[mattpolzin]

The changelog entry on this PR will need to be updated now that v0.7.0 was released. [Done]

[gallais]

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.