Trying to Understand an Example in FPIL

Stream: general

[David Ledvinka]

I am trying to understand the following excerpt from 6.2.1.1. of FPIL:

---

The problem here is that Lean is selecting the wrong Monad instance for the surrounding use of pure. Similar errors occur for the definition of bind. One solution is to use type annotations to guide Lean to the correct Monad instance:

instance [Monad m] : Monad (OptionT m) where
  pure x := (pure (some x) : m (Option _))
  bind action next := (do
    match (← action) with
    | none => pure none
    | some v => next v : m (Option _))

While this solution works, it is inelegant and the code becomes a bit noisy.

An alternative solution is to define functions whose type signatures guide Lean to the correct instances. In fact, OptionT could have been defined as a structure:

structure OptionT (m : Type u → Type v) (α : Type u) : Type v where
  run : m (Option α)

This would solve the problem, because the constructor OptionT.mk and the field accessor OptionT.run would guide type class inference to the correct instances. The downside to doing this is that the resulting code is more complicated, and these structures can make it more difficult to read proofs. The best of both worlds can be achieved by defining functions that serve the same role as the constructor OptionT.mk and the field OptionT.run, but that work with the direct definition:

def OptionT.mk (x : m (Option α)) : OptionT m α := x

def OptionT.run (x : OptionT m α) : m (Option α) := x

Both functions return their inputs unchanged, but they indicate the boundary between code that is intended to present the interface of OptionT and code that is intended to present the interface of the underlying monad m. Using these helpers, the Monad instance becomes more readable:

instance [Monad m] : Monad (OptionT m) where
  pure x := OptionT.mk (pure (some x))
  bind action next := OptionT.mk do
    match ← action with
    | none => pure none
    | some v => next v

Here, the use of OptionT.mk indicates that its arguments should be considered as code that uses the interface of m, which allows Lean to select the correct Monad instances.

---

In particular given the first solution I would have "expected" that you want to use run. Why does mk allow lean to make the right choice of pure here?

[David Ledvinka]

Oh I think I figured it out myself. The input to mk is interpreted as m (Option α) so pure is interpreted as the pure instance for m. The first solution forces lean to interpret the output first as m (Option α) so it can use pure and then realizes the output is definitionally equal to the required OptionT m α?