Is learning monads essential for coding in Lean?

Stream: new members

[Dan Abramov]

I’ve gotten more interested in the “Lean as a programming language” side of things and have scanned through FPIL. I’ve never programmed in a completely pure language before so I’m not familiar with idioms around that.

I’ve noticed a bulk of FPIL seems dedicated to monads, functors, and monad transformers. I’m familiar with the general idea of pure functional programming (and treating IO as part of return value). I’m also familiar with the idea that monadic interfaces let you create sequential-like syntax a la async/await which makes pure IO feel close in usability to imperative programming languages.

However, to my non-fully-functional brain, the idea of learning about “monad transformers” and such feels like an immediate turn-off. At least compared to things like Koka where, if I understands it right, typed effects propagate upwards without the explicit machinery associated with monads.

Do I need to bite the bullet and just learn these concepts? And does Lean consider them SOTA in terms of usability, i.e. does the Lean team consider that everyone who wants to write programs that do IO need to learn what a “monad transformer” is? Or are there ideas on how to avoid that?

[Aaron Liu]

I don't think about how monad transformers work I just use them

[Arthur Paulino]

My way of thinking about monads is that there are essentially 3 orthogonal operations we want to perform more ergonomically in a purely functional language:

1. We want to have access to some read-only data. This is similar to passing shared references to functions in Rust
2. We want to mutate some state. This is similar to passing (exclusive) mutable references to functions in Rust
3. We want to return errors, and have the ability to early return them sometimes. This is similar to using the Result type in Rust and the ? operator

For (1), there's ReaderT. For (2) there's StateT and for (3) there's ExceptT.

[Niels Voss]

When I read #fpil a few years ago, I seem to remember that Chapter 2 basically teaches you how monads work without actually telling you that that's what you're learning. The info in Chapter 2 should be enough to let you write lots of nontrivial programs without actually needing a deeper understanding of what's going on.

I guess whether you need to learn monads depends on what kinds of programs you plan to write. But I think if you get used to how IO works, you'll find that learning monads isn't actually very hard. I wouldn't worry about monad transformers unless you get to the point where you understand monads well enough that you start wanting to combine different monads.

[Niels Voss]

(Also, maybe the linkifier should link to the new website of FPIL rather than the old one)

[Aaron Liu]

Here's how I think about monad transformers, let's use StateT as an example.

• StateM σ is a monad that gives you access to a box containing one mutable value of type σ. A value of type StateM σ α is a computation that produces an α using a box containing a mutable value of σ. You can interact with this box using the get, set, and modifyGet functions that StateM provides. If you have f : StateM σ α and init : σ then f.run init : α × σ will set up a box, put init inside, and then run f using this box. The return value is α × σ, which is the value of α produced, and also the final state of the box.
• If m is a monad, then StateT σ m is a monad that extends m with a box containing one mutable value of type σ. A value of type StateT σ m α is a computation in m that produces an α using a box containing a mutable value of type σ. You can interact with this box using the get, set, and modifyGet functions that StateT provides, and you can also do all the things that are possible in m. If you have f : StateT σ m α and init : σ then f.run init : m (α × σ) will set up a box, put init inside, and then run f using this box. The return value is m (α × σ), which is the computation in m that will return the value of α produced by f, and also the final state of the box.

[Rado Kirov]

Slightly off topic and not sure about monad transformers but on monads Waller’s original paper https://homepages.inf.ed.ac.uk/wadler/papers/marktoberdorf/baastad.pdf IMHO still remains the best practical introduction to monads. It doesn’t go into the category theory at all, it has a lot of examples of writing mini parser with monads, etc. The myriad of analogy driven blog posts muddled the waters.

[eyelash]

I remember monads being scary when I first learned functional programming. Nowadays I think of monads as a powerful abstraction over control flow. Other languages have features such as methods, exceptions, or async/await. In a purely functional language all of these features can be built on top of monads and do notation.

I recommend learning how to use specific monads such as IO, Option, Except, or StateM. You don't need to know what a monad is to use those. In fact, some of these also exist in other languages, they just aren't called monads. Once you have a good understanding of these specific monads you might want to dive deeper and learn how to write your own monads or combine monads using monad transformers.

[eyelash]

One other way to think about monads that might be useful to programmers is to think of monads as operator overloading, but instead of overloading the usual operators, you overload control flow. In a language with operator overloading the meaning of a + b depends on the types of a and b and the definition of the overloaded plus operator. Similarly, in a language with monads and do notation, the meaning of do { a; b } depends on the definition of the monad. In Lean, to overload the plus operator, you create an instance of HAdd and to overload the do notation you create an instance of Monad.

[Dan Abramov]

These are good explanations, thanks. To answer this directly:

Other languages have features such as methods, exceptions, or async/await. In a purely functional language all of these features can be built on top of monads and do notation.

What I’m asking about is whether dealing with monads directly actually is state of the art in pure functional language. As I mention in the OP post, I’ve heard of other approaches to this, for example effects in Koka:

Effect handlers can be composed freely. This is unlike general monads which need monad transformers to compose in particular ways.

Lean seems to be state of the art in multiple ways so what I’m expressing is some doubt whether this particular approach is also state of the art. I guess I’m asking if we really have nothing “better” by this point. I’m obviously biased towards effects (they “feel” “obvious” to me in a way monadic ceremony isn’t) but maybe there’s something else that’s promising.

[Dan Abramov]

So more concretely I’m wondering whether

1. Lean team doesn’t consider algebraic effects to be an improvement over dealing with monad transformers

2. Lean team does consider it to be an improvement but there’s still not enough research into effects to build upon them

3. It’s an improvement but also too much work and can’t possibly be prioritized so will likely have to wait for years

4. It’s an improvement but fundamentally can’t fit into the Lean typesystem so it isn’t considered

I searched this board for discussions about algebraic effects and found surprisingly little. I don’t understand if it’s because the folks here don’t find value in them, or because of insurmountable difficulties, or because they’re somehow not well-known (that would be difficult to believe in the PL crowd though).

[Mauricio Collares]

Did you look at https://leanprover.zulipchat.com/#narrow/channel/270676-lean4/topic/algebraic.20effects.20and.20handlers.3F ?

[Dan Abramov]

Yea that seems to be closest to the official word on the matter. I was hoping maybe there's a bit more on how Lean plans to solve similar problems (or maybe Lean just considers them non-problems, which would be helpful to hear explicitly too).