7. Functors, Monads and do-Notation🔗

The type classes Functor, Applicative, and Monad provide fundamental tools for functional programming.An introduction to programming with these abstractions is available in Functional Programming in Lean. While they are inspired by the concepts of functors and monads in category theory, the versions used for programming are more limited. The type classes in Lean's standard library represent the concepts as used for programming, rather than the general mathematical definition.

Instances of Functor allow an operation to be applied consistently throughout some polymorphic context. Examples include transforming each element of a list by applying a function and creating new IO actions by arranging for a pure function to be applied to the result of an existing IO action. Instances of Monad allow side effects with data dependencies to be encoded; examples include using a tuple to simulate mutable state, a sum type to simulate exceptions, and representing actual side effects with IO. Applicative functors occupy a middle ground: like monads, they allow functions computed with effects to be applied to arguments that are computed with effects, but they do not allow sequential data dependencies where the output of an effect forms an input into another effectful operation.

The additional type classes Pure, Bind, SeqLeft, SeqRight, and Seq capture individual operations from Applicative and Monad, allowing them to be overloaded and used with types that are not necessarily Applicative functors or Monads. The Alternative type class describes applicative functors that additionally have some notion of failure and recovery.

🔗type class
Functor.{u, v} (f : Type u → Type v)
    : Type (max (u + 1) v)

In functional programming, a "functor" is a function on types F : Type u → Type v equipped with an operator called map or <$> such that if f : α → β then map f : F α → F β, so f <$> x : F β if x : F α. This corresponds to the category-theory notion of functor in the special case where the category is the category of types and functions between them, except that this class supplies only the operations and not the laws (see LawfulFunctor).

Instance Constructor

Functor.mk.{u, v}

Methods

map : {α β : Type u} → (α → β) → f α → f β

If f : α → β and x : F α then f <$> x : F β.

mapConst : {α β : Type u} → α → f β → f α

The special case const a <$> x, which can sometimes be implemented more efficiently.

🔗type class
Pure.{u, v} (f : Type u → Type v)
    : Type (max (u + 1) v)

The typeclass which supplies the pure function. See Monad.

Instance Constructor

Pure.mk.{u, v}

Methods

pure : {α : Type u} → α → f α

If a : α, then pure a : f α represents a monadic action that does nothing and returns a.

🔗type class
Seq.{u, v} (f : Type u → Type v)
    : Type (max (u + 1) v)

The typeclass which supplies the <*> "seq" function. See Applicative.

Instance Constructor

Seq.mk.{u, v}

Methods

seq : {α β : Type u} → f (α → β) → (Unit → f α) → f β

If mf : F (α → β) and mx : F α, then mf <*> mx : F β. In a monad this is the same as do let f ← mf; x ← mx; pure (f x): it evaluates first the function, then the argument, and applies one to the other.

To avoid surprising evaluation semantics, mx is taken "lazily", using a Unit → f α function.

🔗type class
SeqLeft.{u, v} (f : Type u → Type v)
    : Type (max (u + 1) v)

The typeclass which supplies the <* "seqLeft" function. See Applicative.

Instance Constructor

SeqLeft.mk.{u, v}

Methods

seqLeft : {α β : Type u} → f α → (Unit → f β) → f α

If x : F α and y : F β, then x <* y evaluates x, then y, and returns the result of x.

To avoid surprising evaluation semantics, y is taken "lazily", using a Unit → f β function.

🔗type class
SeqRight.{u, v} (f : Type u → Type v)
    : Type (max (u + 1) v)

The typeclass which supplies the *> "seqRight" function. See Applicative.

Instance Constructor

SeqRight.mk.{u, v}

Methods

seqRight : {α β : Type u} → f α → (Unit → f β) → f β

If x : F α and y : F β, then x *> y evaluates x, then y, and returns the result of y.

To avoid surprising evaluation semantics, y is taken "lazily", using a Unit → f β function.

🔗type class
Applicative.{u, v} (f : Type u → Type v)
    : Type (max (u + 1) v)

An applicative functor is an intermediate structure between Functor and Monad. It mainly consists of two operations:

  • pure : α → F α

  • seq : F (α → β) → F α → F β (written as <*>)

The seq operator gives a notion of evaluation order to the effects, where the first argument is executed before the second, but unlike a monad the results of earlier computations cannot be used to define later actions.

Instance Constructor

Applicative.mk.{u, v}

Extends

Methods

map : {α β : Type u} → (α → β) → f α → f β
Inherited from
  1. Functor f
  2. Pure f
  3. Seq f
  4. SeqLeft f
  5. SeqRight f
mapConst : {α β : Type u} → α → f β → f α
Inherited from
  1. Functor f
  2. Pure f
  3. Seq f
  4. SeqLeft f
  5. SeqRight f
pure : {α : Type u} → α → f α
Inherited from
  1. Functor f
  2. Pure f
  3. Seq f
  4. SeqLeft f
  5. SeqRight f
seq : {α β : Type u} → f (α → β) → (Unit → f α) → f β
Inherited from
  1. Functor f
  2. Pure f
  3. Seq f
  4. SeqLeft f
  5. SeqRight f
seqLeft : {α β : Type u} → f α → (Unit → f β) → f α
Inherited from
  1. Functor f
  2. Pure f
  3. Seq f
  4. SeqLeft f
  5. SeqRight f
seqRight : {α β : Type u} → f α → (Unit → f β) → f β
Inherited from
  1. Functor f
  2. Pure f
  3. Seq f
  4. SeqLeft f
  5. SeqRight f
Lists with Lengths as Applicative Functors

The structure LenList pairs a list with a proof that it has the desired length. As a consequence, its zipWith operator doesn't require a fallback in case the lengths of its inputs differ.

structure LenList (length : Nat) (α : Type u) where list : List α lengthOk : list.length = length def LenList.head (xs : LenList (n + 1) α) : α := xs.list.head <| α:Type uβ:Type un:Natxs:LenList (n + 1) α⊢ xs.list ≠ [] α:Type uβ:Type un:Natxs:LenList (n + 1) αh:xs.list = []⊢ False α:Type uβ:Type un:Natlist✝:List αlengthOk✝:list✝.length = n + 1h:{ list := list✝, lengthOk := lengthOk✝ }.list = []⊢ False α:Type uβ:Type un:Natlist✝:List αlengthOk✝:list✝.length = n + 1h:list✝ = []⊢ False All goals completed! 🐙 def LenList.tail (xs : LenList (n + 1) α) : LenList n α := match xs with | ⟨_ :: xs', _⟩ => ⟨xs', α:Type uβ:Type un:Natxs:LenList (n + 1) αhead✝:αxs':List αlengthOk✝:(head✝ :: xs').length = n + 1⊢ xs'.length = n All goals completed! 🐙⟩ def LenList.map (f : α → β) (xs : LenList n α) : LenList n β where list := xs.list.map f lengthOk := α:Type uβ:Type un:Natf:α → βxs:LenList n α⊢ (List.map f xs.list).length = n α:Type uβ:Type un:Natf:α → βlist✝:List αlengthOk✝:list✝.length = n⊢ (List.map f { list := list✝, lengthOk := lengthOk✝ }.list).length = n All goals completed! 🐙 def LenList.zipWith (f : α → β → γ) (xs : LenList n α) (ys : LenList n β) : LenList n γ where list := xs.list.zipWith f ys.list lengthOk := α:Type uβ:Type un:Natf:α → β → γxs:LenList n αys:LenList n β⊢ (List.zipWith f xs.list ys.list).length = n α:Type uβ:Type un:Natf:α → β → γys:LenList n βlist✝:List αlengthOk✝:list✝.length = n⊢ (List.zipWith f { list := list✝, lengthOk := lengthOk✝ }.list ys.list).length = n; α:Type uβ:Type un:Natf:α → β → γlist✝¹:List αlengthOk✝¹:list✝¹.length = nlist✝:List βlengthOk✝:list✝.length = n⊢ (List.zipWith f { list := list✝¹, lengthOk := lengthOk✝¹ }.list { list := list✝, lengthOk := lengthOk✝ }.list).length = n All goals completed! 🐙

The well-behaved Applicative instance applies functions to arguments element-wise. Because Applicative extends Functor, a separate Functor instance is not necessary, and map can be defined as part of the Applicative instance.

instance : Applicative (LenList n) where map := LenList.map pure x := { list := List.replicate n x lengthOk := List.length_replicate _ _ } seq fs xs := type mismatch LenList.zipWith (fun x1 x2 => ?m.118) fs (xs ()) has type LenList n γ : Type ?u.101 but is expected to have type LenList n β✝ : Type ?u.10fs.zipWith (type mismatch x1✝ x2✝ has type β✝ : Type ?u.10 but is expected to have type γ : Type ?u.101· ·) (xs ())

The well-behaved Monad instance takes the diagonal of the results of applying the function:

@[simp] theorem LenList.list_length_eq (xs : LenList n α) : xs.list.length = n := α:Type un:Natxs:LenList n α⊢ xs.list.length = n α:Type un:Natlist✝:List αlengthOk✝:list✝.length = n⊢ { list := list✝, lengthOk := lengthOk✝ }.list.length = n All goals completed! 🐙 def fail to show termination for LenList.diagonal with errors failed to infer structural recursion: Not considering parameter α of LenList.diagonal: it is unchanged in the recursive calls Not considering parameter n of LenList.diagonal: it is unchanged in the recursive calls Cannot use parameter square: the type LenList n (LenList n α) does not have a `.brecOn` recursor failed to prove termination, possible solutions: - Use `have`-expressions to prove the remaining goals - Use `termination_by` to specify a different well-founded relation - Use `decreasing_by` to specify your own tactic for discharging this kind of goal α : Type u n n' : Nat square : LenList (n' + 1) (LenList (n' + 1) α) ⊢ sizeOf (sorry ()) < sizeOf squareLenList.diagonal (square : LenList n (LenList n α)) : LenList n α := match n with | 0 => ⟨[], rfl⟩ | n' + 1 => { list := square.head.head :: application type mismatch diagonal (map (fun x => ?m.284) square.tail) argument map (fun x => ?m.284) square.tail has type LenList n' ?m.279 : Type u but is expected to have type LenList n (LenList n α) : Type u(square.tail.map (·.tail)).diagonal.list, lengthOk := α:Type uβ:Type un:Natn':Natsquare:LenList (n' + 1) (LenList (n' + 1) α)⊢ (square.head.head :: (diagonal sorry).list).length = n' + 1 α:Type uβ:Type un:Natn':Natsquare:LenList (n' + 1) (LenList (n' + 1) α)⊢ n = n' }
🔗type class
Alternative.{u, v} (f : Type u → Type v)
    : Type (max (u + 1) v)

An Alternative functor is an Applicative functor that can "fail" or be "empty" and a binary operation <|> that “collects values” or finds the “left-most success”.

Important instances include

  • Option, where failure := none and <|> returns the left-most some.

  • Parser combinators typically provide an Applicative instance for error-handling and backtracking.

Error recovery and state can interact subtly. For example, the implementation of Alternative for OptionT (StateT σ Id) keeps modifications made to the state while recovering from failure, while StateT σ (OptionT Id) discards them.

Instance Constructor

Alternative.mk.{u, v}

Extends

Methods

map : {α β : Type u} → (α → β) → f α → f β
Inherited from
  1. Applicative f
mapConst : {α β : Type u} → α → f β → f α
Inherited from
  1. Applicative f
pure : {α : Type u} → α → f α
Inherited from
  1. Applicative f
seq : {α β : Type u} → f (α → β) → (Unit → f α) → f β
Inherited from
  1. Applicative f
seqLeft : {α β : Type u} → f α → (Unit → f β) → f α
Inherited from
  1. Applicative f
seqRight : {α β : Type u} → f α → (Unit → f β) → f β
Inherited from
  1. Applicative f
failure : {α : Type u} → f α

Produces an empty collection or recoverable failure. The <|> operator collects values or recovers from failures. See Alternative for more details.

orElse : {α : Type u} → f α → (Unit → f α) → f α

Depending on the Alternative instance, collects values or recovers from failures by returning the leftmost success. Can be written using the <|> operator syntax.

🔗type class
Bind.{u, v} (m : Type u → Type v)
    : Type (max (u + 1) v)

The typeclass which supplies the >>= "bind" function. See Monad.

Instance Constructor

Bind.mk.{u, v}

Methods

bind : {α β : Type u} → m α → (α → m β) → m β

If x : m α and f : α → m β, then x >>= f : m β represents the result of executing x to get a value of type α and then passing it to f.

🔗type class
Monad.{u, v} (m : Type u → Type v)
    : Type (max (u + 1) v)

A monad is a structure which abstracts the concept of sequential control flow. It mainly consists of two operations:

  • pure : α → F α

  • bind : F α → (α → F β) → F β (written as >>=)

Like many functional programming languages, Lean makes extensive use of monads for structuring programs. In particular, the do notation is a very powerful syntax over monad operations, and it depends on a Monad instance.

See the do notation chapter of the manual for details.

Instance Constructor

Monad.mk.{u, v}

Extends

Methods

map : {α β : Type u} → (α → β) → m α → m β
Inherited from
  1. Applicative m
  2. Bind m
mapConst : {α β : Type u} → α → m β → m α
Inherited from
  1. Applicative m
  2. Bind m
pure : {α : Type u} → α → m α
Inherited from
  1. Applicative m
  2. Bind m
seq : {α β : Type u} → m (α → β) → (Unit → m α) → m β
Inherited from
  1. Applicative m
  2. Bind m
seqLeft : {α β : Type u} → m α → (Unit → m β) → m α
Inherited from
  1. Applicative m
  2. Bind m
seqRight : {α β : Type u} → m α → (Unit → m β) → m β
Inherited from
  1. Applicative m
  2. Bind m
bind : {α β : Type u} → m α → (α → m β) → m β
Inherited from
  1. Applicative m
  2. Bind m
  1. 7.1. Laws
  2. 7.2. Lifting Monads
    1. 7.2.1. Reversing Lifts
      1. 7.2.1.1. Monad Functors
      2. 7.2.1.2. Reversible Lifting with MonadControl
  3. 7.3. Syntax
    1. 7.3.1. Infix Operators
      1. 7.3.1.1. Functors
      2. 7.3.1.2. Applicative Functors
      3. 7.3.1.3. Monads
    2. 7.3.2. do-Notation
      1. 7.3.2.1. Sequential Computations
      2. 7.3.2.2. Early Return
      3. 7.3.2.3. Local Mutable State
      4. 7.3.2.4. Control Structures
      5. 7.3.2.5. Iteration
      6. 7.3.2.6. Identifying do Blocks
      7. 7.3.2.7. Type Classes for Iteration
  4. 7.4. API Reference
    1. 7.4.1. Discarding Results
    2. 7.4.2. Control Flow
    3. 7.4.3. Lifting Boolean Operations
    4. 7.4.4. Kleisli Composition
    5. 7.4.5. Re-Ordered Operations
  5. 7.5. Varieties of Monads
    1. 7.5.1. Monad Type Classes
    2. 7.5.2. Monad Transformers
    3. 7.5.3. Identity
    4. 7.5.4. State
      1. 7.5.4.1. General State API
      2. 7.5.4.2. Tuple-Based State Monads
      3. 7.5.4.3. State Monads in Continuation Passing Style
      4. 7.5.4.4. State Monads from Mutable References
    5. 7.5.5. Reader
    6. 7.5.6. Option
    7. 7.5.7. Exceptions
      1. 7.5.7.1. Exceptions
      2. 7.5.7.2. Type Class
      3. 7.5.7.3. “Finally” Computations
      4. 7.5.7.4. Transformer
      5. 7.5.7.5. Exception Monads in Continuation Passing Style
    8. 7.5.8. Combined Error and State Monads
      1. 7.5.8.1. State Rollback
      2. 7.5.8.2. Implementations