I’ve been experimenting with a few things that would benefit from do notation – mostly to organize how type annotations work. I’ve also been working through a rough implementation on the haskell backend and things don’t seem to be too breaking 
The main idea is this – introduce “do notation” syntax that comprises, syntactically, of three parts:
do_block = do <functor> <bind> <result type>
<do_lines>
<final_line>
do_lines = <ident> : <type> <- <expr>
| <expr>
final_line = expr
In general, we’d have:
do M bind A
x : B <- q
r
z : D <- s
k
turn into:
bind B A q (\(x : B) ->
bind {} A r (\(_ : {}) ->
bind D A s (\(z : D) ->
k
)
)
)
M (in do M bind A) would have to be an expression of type Type -> Type.
bind (in do M bind A) would have to be an expression of type
forall (a : Type)
-> forall (b : Type)
-> M a
-> (a -> M b)
-> M b
And the type of the entire expression would be M A, and k would also have type M A.
Specifically, the rules for within do M bind A would be:
do M bind A
x : B <- q
rest
=>
bind B A q (\(x : B) -> desugar-rest)
and
do M bind A
r
rest
=>
bind {} A r (\(_ : {}) -> desugar-rest)
where any “non-binding” line is required to have type M {}.
So for example, for Optional, if we had ./bind:
\(a : Type)
-> \(b : Type)
-> \(x : Optional a)
-> \(f : a -> Optional b)
-> Optional/fold a x (Optional b) f (None b)
and ./subtractMaybe
\(x : Natural) ->
if Natural/isZero x
then None Natural
else Some (Natural/subtract 1 x)
Then we could do:
\(x : Natural) -> do Optional ./bind Natural
y : Natural <- ./subtractMaybe x
z : Natural <- ./subtractMaybe y
./subtractMaybe z
This would be desugared as:
\(x : Natural) -> ./bind Natural Natural (./subtractMaybe x) (\(y : Natural) ->
./bind Natural Natural (./subtractMaybe y) (\(z : Natural) ->
./subtractMaybe z
)
)
The requirements for type annotations for all bindings, and also that any “non-binding” line has to have type M {}, requires no extra logic for type inference: the types are all present as they are.
The advantages of being able to write
bind B A q (\(x : B) ->
bind {} A r (\(_ : {}) ->
bind D A s (\(z : D) ->
k
)
)
)
as
do M bind A
x : B <- q
r
z : D <- s
k
are:
-
The type applications are not duplicated, and closer to their main meaningful binding.
In the case of
qandx, for instance,Bwould normally appear twice: as an argument forbind, and again as the lambda annotation. In the do-notation,Bwould only appear once, and next tox, which is arguably where it is the most important to visually see.Most egregiously, in the normal case,
Aappears three times – O(n) on the number of lines. That’s because it is the type of the “final binds” for all of the lines. Now here,Aonly appears once: at the head of the block, to indicate the type of the entire expression as beingM A. -
Formatting is clearer: we don’t need the nested indentation creep of the nested lambdas. Automatic formatting also fails to show the intended structure that the original represents. For do notation, automatic formatting could be made to be more clear.
-
Dataflow is visually clearer.
The “need” for a do notation arose from my experiments with using dhall as a cross-platform safe scripting language, and in the end I’d like to be able to write things like
do ./IO ./bindIO {}
x : Text <- ./getLine
y : Text <- ./readFile "myfile.txt"
./putStrLn x
./writeFile "destination.txt" y
and have them be interpretable by an interpreter.
This works at the moment with explicit binds, but is made very unweildy by the formatting and, probably most significantly, the duplication of necessary type annotations and type arguments for things to work out properly.
I…don’t really have a plan as for how indentation/layouting would work. Right now my examples are a bit ad-hoc with how layouting, newlines, etc. work and I’m open to suggestions.
Let me know if you think this would be something that would fit into the overall vision of dhall, or any tweaks (if possible) that would bring it more in line! If it’s way too out-there to warrant being a part of the standard language, I’d understand too.