A minimalistic proposal for do-notation

[winitzki]

There was already a discussion about do-notation here #1017 and here https://discourse.dhall-lang.org/t/proposal-do-notation-syntax/99/7

I would like to propose another syntax for the do-notation.
This is super easy to implement because there are no changes anywhere except for adding one more top-level rule to the parser.

Example syntax

as M T in bind
    with x : A in p
    with y : B in q
    with z : C in r
    then s

This is desugared at parsing time to:

bind A T p ( λ(x : A) →
  bind B T q ( λ(y : B) →
    bind C T r ( λ(z : B) →
      s
)))

Here M is a type constructor and bind is a monad-like method.

The types of variables must be:

M : Type → Type
bind : ∀(a : Type) → ∀(b : Type) → M a → (a → M b) → M b
p : M A
q : M B
r : M C
s : M T

The type of the entire expression is M T and is made more clear by as M T. The M T must be a literal type application.

(Perhaps this could be simplified to just as T in bind because the desugaring uses only T and does not need M?)

The expressions p, q, r, etc., may use variables x : A, y : B, etc., defined at any line above the line where they are used. This is ensured automatically after desugaring.

Some advantages of my proposal over what was discussed before:

• The do-notation is desugared at parsing time into standard Dhall.
• No new keywords or reserved symbols needed for the parser.
• No indentation sensitivity, code can be reformatted arbitrarily.
• No new data structures needed in Syntax.hs.
• One more top-level parsing rule starting with a keyword, which is not in conflict with any other parsing rules.
• The do-notation is not a breaking change because it only introduces a new expression that starts with as. In today's Dhall, no expression may start with as. So, all today's programs will run correctly in the presence of the new parsing rule.

Working example code is shown here.

Parsing rules

The do-notation contains the first block: as M T in b, then zero or more with ... in ... bindings, and finally a closing block then ....

; "as (M T) in bind *(with x : A in p) then r"
expression-do-notation = "as" whsp1 application-expression whsp "in" whsp1 expression whsp *with-binding "then" whsp1 expression

; "with x : A in p"
with-binding = "with" whsp1 nonreserved-label whsp ":" whsp1 expression whsp "in" whsp1 expression whsp

The new rule expression-do-notation goes into the main expression rule, for example, here: https://github.com/dhall-lang/dhall-lang/blob/master/standard/dhall.abnf#L832

Desugaring rules

Desugaring is done at parse time.

  desugar_do_notation(as M T in bind then x) = x

 desugar_do_notation(as M T in bind with x : A in p <rest of the code>)
   = bind A T p (λ(x : A) -> desugar_do_notation(as M T in bind <rest of the code>))`