Understanding do-notation syntax

Stream: Program verification

[Clément Blaudeau]

I'm trying to understand the do-notation syntax (as we're using it as a target of our translation of Rust code to lean). I'm puzzled by the fact that chaining monadic let-bindings on the right-hand side is not allowed :

def this_fails (_: Nat) : Option Nat := do
  let x : Nat ←
    let y : Nat ← pure 0  -- fails here
    pure (y + 1)
  pure x

while putting a match of if-then-else works fine :

def works_match (_: Nat) : Option Nat := do
  let x : Nat ←
    match () with
    | _ =>
      let y : Nat ← pure 0
      pure (y+1)
  pure x

def works_ite (_: Nat) : Option Nat := do
  let x : Nat ←
    if h: true then
      let y : Nat ← pure 0
      pure (y+1)
    else
      by apply False.elim; apply h; rfl
  pure x

Here are the examples in the playground. It feels like a bug in the syntax, but I wanted to ask if I was not missing something obvious before opening an actual issue on github.

[Sebastian Graf]

Short answer: The parser only accepts a single do element/statement in the RHS of let x <- rhs; rest, so it's a feature :)

Long answer: In order to relax this restriction, it would be necessary to handle let mut reassignments in rhs. (The case let x <- y := y + 1 currently is conveniently disallowed, probably for the same reason.) Whenever there's a reassignment in a nested construct, do elaboration currently introduces a join point to pass the updated mut vars. But it only does so for select control flow constructs such as if and match, where it's also important to not duplicate the continuation into the branches. Changing this would be a major rewrite of the do elaborator, I think.

One could rewrite rhs to box up the mut vars along with the result, let (x, newY) <- let y := y + 1; pure ((), newY). That would be the "StateT rather than StateCpsT encoding of the mut vars and it has the downside of boxing up a tuple rather than doing a multi-ar function call to what will end up pretty likely as a non-escaping function closure with the current StateCpsT strategy. Also it would mean more complexity, and it is incompatible with the current translation of early return, which can just be pure (because returns always leave the outermost do and the elaborator uses said CPS strategy.)

So: I see no chance that this "bugfix" will happen with the current do elaborator. But I'm working on rewriting do elaboration this Q, and will consider this as a feature request.

[Clément Blaudeau]

Thank you for the answer (short and long) and for the work on this feature!
To understand why wrapping my rhs let-binding into a dummy match () with | _ => works: is it correct to say that the match provides a join point, while having just a rhs let-binding does not ?

So: I see no chance that this "bugfix" will happen with the current do elaborator. But I'm working on rewriting do elaboration this Q, and will consider this as a feature request.

Do you know what is the overall timeline on this ? We (at Cryspen) are very interested in this feature (and corresponding mvcgen support) and might try to contribute to its developpement.

[Sebastian Graf]

is it correct to say that the match provides a join point, while having just a rhs let-binding does not ?

Yes, I think that't the gist of it.

Do you know what is the overall timeline on this ?

I should be finished with the rewrite by the end of the quarter. Could you live with a macro until then? I imagine that would be a viable workaround

[Sebastian Graf]

That is, something like

macro "let " x:ident " : " ty:term " ←* " rhs:doSeq : doElem =>
  `(doElem| let $x : $ty ← match () with | () => $rhs)

#check do
  let x : Nat ←*
    let y : Nat ←* pure 0  -- no longer fails here
    pure (y + 1)
  pure x

You could of course override the existing syntax as well.

[Clément Blaudeau]

Thank you for the macro! To override the existing syntax, I would need to produce a Parser.term.doLetArrow directly (without quotations) I suppose ? (just replacing ←* by ← in the macro is not enough)

[Sebastian Graf]

@Markus Himmel also reminded me that you could simply use a nested do block, which will be denested and force creation of a join point as well. Same expansion:

macro "let " x:ident " : " ty:term " ←* " rhs:doSeq : doElem =>
  `(doElem| let $x : $ty ← do $rhs)

#check do
  let x : Nat ←*
    let y : Nat ←* pure 0  -- no longer fails here
    pure (y + 1)
  pure x

---

Here is a macro that does what you want. Note that it emits join points when it doesn't need to, as in the second #check:

import Lean

open Lean Parser

def doIdDecl   := leading_parser
  atomic (ident >> Term.optType >> ppSpace >> Term.leftArrow) >>
  Term.doSeq
def doPatDecl  := leading_parser
  atomic (termParser >> ppSpace >> Term.leftArrow) >>
  Term.doSeq >> optional (checkColGt >> " | " >> Term.doSeq)
@[doElem_parser low] def doLetArrowSeq      := leading_parser
  withPosition ("let " >> optional "mut " >> (doIdDecl <|> doPatDecl))

macro_rules
  | `(doElem| let $[mut%$mutTk?]? $x:ident $[: $ty?]? ← $seq:doSeq) =>
    `(doElem| let $[mut%$mutTk?]? $x:ident $[: $ty?]? ← do $seq)

macro_rules
  | `(doElem| let $[mut%$mutTk?]? $p:term ← $doSeq:doSeq $[| $seq:doSeq]?) =>
    `(doElem| let $[mut%$mutTk?]? $p:term ← do $doSeq:doSeq $[| $seq:doSeq]?)

#check do
  let x : Nat ←
    let y : Nat ← pure 0  -- no longer fails here
    pure (y + 1)
  pure x

#check do
  let x : Nat ← pure (); pure 3
  let y : Nat ← pure (); pure 4
  let z : Nat ← pure (); pure 5
  return x + y + z

[Sebastian Graf]

Beware that the interpretation of semicolons is ambiguous with the macro above, which perhaps is one reason why the default syntax is more restricted. Concretely, do let x : Nat ← pure 13; return x + 3 will not type-check because pure 13; return x + 3 is parsed as one doSeq. This leaves me unconvinced that the above macro is actually a feature that we will support in the builtin syntax.

[Clément Blaudeau]

Thank you for the macro and the explanation !

[Clément Blaudeau]

Could another fix be to allow some delimiters in the do-statement syntax ? This would serve as a join point just like control flow ?

[Sebastian Graf]

Sorry, I didn't understand that. What kind of delimiters do you have in mind? To delimit what?

[Clément Blaudeau]

I was thinking some thing like :

let x <- ( --delimiter, starts a new do-statement
  let y <- ... ;
  y + 1 )
-- continue with top-level
let z <- ...

delimiters could serve as joint point ?

[Sebastian Graf]

Why can't you use do as a delimiter?

let x <- do
  let y <- ...
  y + 1
-- continue with top-level
let z <- ...