postfix monad arrow

Stream: lean4

[James Gallicchio]

have we discussed adding a way to monad-bind as a postfix operation? something like (x : m a).← would work for me. can this be implemented as a macro on expressions, or would it require modifying core do notation?

[Mario Carneiro]

macros are expanded before expandLiftMethod, so it should be possible to implement outside core

[James Gallicchio]

oh huge, let me see if the braindead macro implementation works

[James Gallicchio]

:thinking:

syntax term ".←" : term

macro_rules
| `($t.←) => `(← $t)

#eval show IO _ from do
  IO.getStdin.←.flush -- invalid use of `(<- ...)`, must be nested inside a 'do' expression
  return 0

[James Gallicchio]

from trace.Elab.do:

with_annotate_term(Term.paren "(" (Term.proj (Term.paren "(" («term_.←» `IO.getStdin ".←") ")") "." `flush) ")")
      Bind.bind✝ (((IO.getStdin.←).flush) : ?m✝ PUnit✝)
        (fun (_ : PUnit✝) => with_annotate_term(Term.doReturn "return" [(num "0")]) Pure.pure✝ 0)

I'm not entirely sure how to parse this trace

[Mario Carneiro]

you can ignore the with_annotate_term(...) parts, that is just for error messages

[Mario Carneiro]

it appears to have macro expanded the do block without expanding the IO.getStdin.← part first

[Mario Carneiro]

the invalid use of `(<- ...)`, must be nested inside a 'do' expression error is what happens when you try to directly elaborate the expression <- e

[Mario Carneiro]

it is supposed to be eliminated as part of the macro expansion for the do, which finds and replaces them

[James Gallicchio]

Right. so it seems like the do elaborator doesn't fully elaborate the inner expressions before eliminating arrows.

[Mario Carneiro]

I see this:

      match (← liftMacroM <| expandMacro? doElem) with
      | some doElem => doSeqToCode (doElem::doElems)
      | none =>
      match (← liftMacroM <| expandDoIf? doElem) with
      | some doElem => doSeqToCode (doElem::doElems)
      | none =>
        let (liftedDoElems, doElem) ← expandLiftMethod doElem
        ...

but now I'm thinking that the first expandMacro? line is only expanding doElems that are directly macro terms

[James Gallicchio]

I assume in the above example the (macroful) term is wrapped in a seq doElem or whatever?

[Mario Carneiro]

a doExpr (which embeds term in doElem)

[Mario Carneiro]

the case that would be handled here is something like repeat or assert, which are actually doElems that expand to other doElems

[Mario Carneiro]

expansion of <- terms is done by expandLiftMethod which is not at all user-extensible:

private def liftMethodDelimiter (k : SyntaxNodeKind) : Bool :=
  k == ``Parser.Term.do ||
  k == ``Parser.Term.doSeqIndent ||
  k == ``Parser.Term.doSeqBracketed ||
  k == ``Parser.Term.termReturn ||
  k == ``Parser.Term.termUnless ||
  k == ``Parser.Term.termTry ||
  k == ``Parser.Term.termFor

private partial def hasLiftMethod : Syntax → Bool
  | Syntax.node _ k args =>
    if liftMethodDelimiter k then false
    else if k == ``Parser.Term.liftMethod then true
    else args.any hasLiftMethod
  | _ => false

[James Gallicchio]

can we elaborate the term while it's still contained in a doExprand before expandLiftMethod?

[James Gallicchio]

oh, but we'd have to explicitly elaborate in every term place in the do notation

[Mario Carneiro]

no, macro expansion happens from the outside in

[Mario Carneiro]

you could do it if you replaced do (which you can do in this case without actually rewriting that whole file)

[Mario Carneiro]

(implementation aside, I think e.← looks really silly so I hope you keep it to your personal projects :stuck_out_tongue: .)

[James Gallicchio]

hey, the syntax is up for debate, I just frequently want a way to do it in a pipe chain, and I'd be surprised if you don't feel the same urge to not have to make intermediary let binds just to monad bind :)

[James Gallicchio]

and directly calling bind isn't ergonomic there either

[James Gallicchio]

x |> bind (.|>.foo) looks so much worse than x.←.foo

[James Gallicchio]

This is a much spicier proposal: .!. Then we can have e.g. (e : Except String Int).! + 5 in monadic contexts (a treat for the rustaceans)

[Mario Carneiro]

import Lean
open Lean

macro (name := postfixLift) x:term noWs "." noWs "←" : term => `(← $x)
macro (name := pipeLift) x:term:min "|>." noWs "←" : term => `(← $x)

syntax:arg (name := do') (priority := high) ppAllowUngrouped "do " doSeq : term

@[macro do'] def expandDo' : Macro := fun stx =>
  stx.setKind ``Parser.Term.do |>.replaceM fun stx =>
    if stx.getKind == ``postfixLift || stx.getKind == ``pipeLift then
      Macro.expandMacro? stx
    else
      pure none

#eval show IO _ from do
  IO.getStdin.←.flush
  return 0

[James Gallicchio]

super cool. i'm assuming you still don't want it in Std?

[Alex Keizer]

James Gallicchio said:

x |> bind (.|>.foo) looks so much worse than x.←.foo

There's also (←x) foo, right? A bit more parenthesis than the postfix version, but still better than explicit bind or let-bindings.

[James Gallicchio]

Yeah, the parentheses are what I don't like

[James Gallicchio]

let me find the snippets from my code

[James Gallicchio]

I just grepped and found this in Aesop, it's this sort of thing where I'd rather have postfix ←:
(← (← getRootGoal).get).traceTree .tree

[James Gallicchio]

let _ ← (← bdRef.get).1.markAllSols is also a fun one :joy:

[James Gallicchio]

(from LeanSAT)

[James Gallicchio]

the arrows just get in the way for me when I'm reading this kind of code, since i have to jump back and forth from left to right instead of reading left to right continuously

[James Gallicchio]

it's obviously different when you're using normal (i.e. backwards to any good category theorist) function application and are reading right to left anyways