What These Notes Are For
Lean is a functional programming language, and although it lets the user type imperative looking code using do blocks, under the hood it transforms the same block of code into functional blocks using machinery called monads.
But what the feck is a monad?
I cannot for the life of me seem to find a clean definition1.
After about 48 hours of reading and scouring through different blogs and lecture notes2, here's my opinionated3 take on what a monad is.
When I say functions from here on -- I don't mean a method or a function in a programming language, but a function as introduced in an introductory textbook for mathematics.
Given some computation $C$ that cannot be expressed as a composition of functions, a monad is a type that comes with the "machinery" needed to write $C$ as a composition of functions. It's a circular way of saying: when a function's domain or co-domain involves monadic types, we can always compose these functions.
More precisely: a monad is an inductive type m together with two functions — pure : α → m α (which wraps a term of type α into m α) and bind : m α → (α → m β) → m β (which takes a term of type m α and a function α → m β, extracts the α, and feeds it to the function, thereby enabling composition).
I am aware this precise definition could be more confusing — but a concrete example might help. Say we have two functions in Rust:
fn f(x: i32) -> Option<i32> { if x > 0 { Some(x + 1) } else { None } }
fn g(x: i32) -> Option<i32> { if x < 100 { Some(x * 2) } else { None } }Now normally we can't compose them as g(f(5)) because f returns Option<i32>, not i32. Non-composeable computation. But Option is a monad.
Why? Because Option comes with and_then (which we refer to as bind) and Some (which we refer to as pure).
So we can now compose the above function anyway, using this extended machinery.
f(5).and_then(|x| g(x)) // Some(12)
f(-1).and_then(|x| g(x)) // None — f returned None, so and_then short-circuits without calling g and_then extracts the i32 from Some and feeds it to the next function:
pure is Some — it wraps a plain i32 into Option<i32>.
I've come to the conclusion that there is no easy 3 sentence definition.
Now chances are that this definition is even more confusing, and conveys about as much information as the definition I criticised4. I apologise if this is the case, and refer the reader to this starter post Monads: What Is?, which tells the story in longer form. We'll start with a simple computation that is composable, and then change it so it becomes non-composable. Then we will make it composable again -- and everything that we did to make it composable will be a monad.
If that does not convince you, we will take the monad starter pack from the Lean documentation and re-write it in terms of the same composition notation from the above post.
At this point, we've either convinced ourselves that the above definition somewhat makes sense, or I still don't understand what the feck a monad is, and in that case you should stop reading. Were we to have understood monads, we go into some Lean4 specific machinery that makes writing monadic code easier here and here.
With this monad crash course done, hopefully we have the background to understand what is going on in Markus' post.
Such as these: You Could Have Invented Monads (Dan Piponi), Monads for Functional Programming (Philip Wadler), Monads: Programmer's Definition (Bartosz Milewski), and FP in Lean Ch. 4.
Functions here are mathematical functions in that it's a list of tuples mapping a domain to a co-domain.
Possibly wrong opinion.
By clean definition, I mean how we have a nice definition say for an injective function.This excerpt in italics is from hovering over Monads in the Functional programming book. Perhaps, to functional programming experts, this is a much better definition, but I was no cleverer about what Monads do from this. Monads are an abstraction of sequential control flow and side effects used in functional programming. Monads allow both sequencing of effects and data-dependent effects: the values that result from an early step may influence the effects carried out in a later step.