There are plenty of descriptions of Haskell's do notation as syntactic sugar for stringing together sequences of operators such as >>=.
There are also "laws" that define the semantics of the do notation.
But I haven't found any decent description of how to use do notation as if it was a first class language construct. That would be especially useful for beginners.
"""
Let m be a monad, and a be a type. The do keyword allows you to define a value of type m a in an imperative style: it starts a context where you can write code as a sequence of statements.
In this imperative mini-language, you can bind names to constants (no variables allowed!) in two ways:
If the value you are binding can be deduced from constants already in scope, just use the let keyword.
If the value you are binding is the result of a monadic action, use <- to perform the action and get the resulting value. If the statement is of type m b, the type associated with the name is now b.
Any name bound in this way can be used in the statements that follow it.
You can also perform a monadic action without assigning its result to anything (just write the monadic action as a separate statement).
Finally, the last statement must be the result of your monadic action, i.e. a value of type m a. Just write the action as your last statement.
"""
I feel like it's a pretty simple thing to write, and that most Haskell texts/courses feature that explanation, so I probably misunderstood your request 😅
@glocq That's very good and just what I was looking for, thank you. I don't think that kind of description appears in "Learn You a Haskell for Great Good!", Graham Hutton's "Programming in Haskell", or the Haskell wiki, unless I missed it.
I suppose you can then go on and describe Monad instances in terms of what their do-notation does. Here is what would be called the "equational theory" on do-notation at Maybe:
@underlap I am not sure you can get very far with that approach? The semantics of do notation is defined in terms of return / pure and (>>=). So in order to understand what a do block means for a concrete monad, you have to look up the definition of the Monad and superclass instances, and be able to relate that to what the do-block says. So you basically have to be able to do the desugaring in your head.
Treating do-notation as first-class could still be useful if you limit yourself to one fixed type, say IO where the definitions are built-in anyway. But while I agree in principle that introducing IO before talking about monads (at all or in general) is the correct order, even for IO I am not sure that introducing do without talking about its desugaring helps much.
@kosmikus You may be right. But I wonder if the type constraints of >>= etc. in the IO monad case could be used to infer acceptable types for the parts of the do notation.
Add comment