14. 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)

A functor in the sense used in functional programming, which means a function f : Type u → Type v has a way of mapping a function over its contents. This map operator is written <$>, and overloaded via Functor instances.

This map function should respect identity and function composition. In other words, for all terms v : f α, it should be the case that:

id <$> v = v
For all functions h : β → γ and g : α → β, (h ∘ g) <$> v = h <$> g <$> v

While all Functor instances should live up to these requirements, they are not required to prove that they do. Proofs may be required or provided via the LawfulFunctor class.

Assuming that instances are lawful, this definition corresponds to the category-theoretic notion of functor in the special case where the category is the category of types and functions between them.

Instance Constructor

Functor.mk.{u, v}

Methods

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

Applies a function inside a functor. This is used to overload the <$> operator.

When mapping a constant function, use Functor.mapConst instead, because it may be more efficient.

Conventions for notations in identifiers:

The recommended spelling of <$> in identifiers is map.

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

Mapping a constant function.

Given a : α and v : f α, mapConst a v is equivalent to Function.const _ a <$> v. For some functors, this can be implemented more efficiently; for all other functors, the default implementation may be used.

type class

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

The pure function is overloaded via Pure instances.

Pure is typically accessed via Monad or Applicative instances.

Instance Constructor

Pure.mk.{u, v}

Methods

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

Given a : α, then pure a : f α represents an action that does nothing and returns a.

Examples:

(pure "hello" : Option String) = some "hello"
(pure "hello" : Except (Array String) String) = Except.ok "hello"
(pure "hello" : StateM Nat String).run 105 = ("hello", 105)

type class

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

The <*> operator is overloaded using the function Seq.seq.

While <$> from the class Functor allows an ordinary function to be mapped over its contents, <*> allows a function that's “inside” the functor to be applied. When thinking about f as possible side effects, this captures evaluation order: seq arranges for the effects that produce the function to occur prior to those that produce the argument value.

For most applications, Applicative or Monad should be used rather than Seq itself.

Instance Constructor

Seq.mk.{u, v}

Methods

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

The implementation of the <*> operator.

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

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

Conventions for notations in identifiers:

The recommended spelling of <*> in identifiers is seq.

type class

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

The <* operator is overloaded using seqLeft.

When thinking about f as potential side effects, <* evaluates first the left and then the right argument for their side effects, discarding the value of the right argument and returning the value of the left argument.

For most applications, Applicative or Monad should be used rather than SeqLeft itself.

Instance Constructor

SeqLeft.mk.{u, v}

Methods

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

Sequences the effects of two terms, discarding the value of the second. This function is usually invoked via the <* operator.

Given x : f α and y : f β, x <* y runs x, then runs y, and finally returns the result of x.

The evaluation of the second argument is delayed by wrapping it in a function, enabling “short-circuiting” behavior from f.

Conventions for notations in identifiers:

The recommended spelling of <* in identifiers is seqLeft.

type class

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

The *> operator is overloaded using seqRight.

When thinking about f as potential side effects, *> evaluates first the left and then the right argument for their side effects, discarding the value of the left argument and returning the value of the right argument.

For most applications, Applicative or Monad should be used rather than SeqLeft itself.

Instance Constructor

SeqRight.mk.{u, v}

Methods

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

Sequences the effects of two terms, discarding the value of the first. This function is usually invoked via the *> operator.

Given x : f α and y : f β, x *> y runs x, then runs y, and finally returns the result of y.

The evaluation of the second argument is delayed by wrapping it in a function, enabling “short-circuiting” behavior from f.

Conventions for notations in identifiers:

The recommended spelling of *> in identifiers is seqRight.

type class

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

An applicative functor is more powerful than a Functor, but less powerful than a Monad.

Applicative functors capture sequencing of effects with the <*> operator, overloaded as seq, but not data-dependent effects. The results of earlier computations cannot be used to control later effects.

Applicative functors should satisfy four laws. Instances of Applicative are not required to prove that they satisfy these laws, which are part of the LawfulApplicative class.

Instance Constructor

Applicative.mk.{u, v}

Extends

Functor f
Pure f
Seq f
SeqLeft f
SeqRight f

Methods

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

Inherited from

Functor f
Pure f
Seq f
SeqLeft f
SeqRight f

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

Inherited from

Functor f
Pure f
Seq f
SeqLeft f
SeqRight f

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

Inherited from

Functor f
Pure f
Seq f
SeqLeft f
SeqRight f

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

Inherited from

Functor f
Pure f
Seq f
SeqLeft f
SeqRight f

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

Inherited from

Functor f
Pure f
Seq f
SeqLeft f
SeqRight f

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

Inherited from

Functor f
Pure f
Seq f
SeqLeft f
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 <| byα:Type uβ:Type un:Natxs:LenList (n + 1) α⊢ xs.list ≠ []
    intro hα:Type uβ:Type un:Natxs:LenList (n + 1) αh:xs.list = []⊢ False
    cases xsmkα:Type uβ:Type un:Natlist✝:List αlengthOk✝:list✝.length = n + 1h:{ list := list✝, lengthOk := lengthOk✝ }.list = []⊢ False
    simp_all [List.length]mkα:Type uβ:Type un:Natlist✝:List αlengthOk✝:list✝.length = n + 1h:list✝ = []⊢ False
    subst_eqsAll goals completed! 🐙

def LenList.tail (xs : LenList (n + 1) α) : LenList n α :=
  match xs with
  | ⟨_ :: xs', _⟩ => ⟨xs', byα:Type uβ:Type un:Natxs:LenList (n + 1) αhead✝:αxs':List αlengthOk✝:(head✝ :: xs').length = n + 1⊢ xs'.length = n simp_allAll goals completed! 🐙⟩

def LenList.map (f : α → β) (xs : LenList n α) : LenList n β where
  list := xs.list.map f
  lengthOk := byα:Type uβ:Type un:Natf:α → βxs:LenList n α⊢ (List.map f xs.list).length = n
    cases xsmkα:Type uβ:Type un:Natf:α → βlist✝:List αlengthOk✝:list✝.length = n⊢ (List.map f { list := list✝, lengthOk := lengthOk✝ }.list).length = n
    simp [List.length_map, *]All goals completed! 🐙

def LenList.zipWith (f : α → β → γ)
    (xs : LenList n α) (ys : LenList n β) :
    LenList n γ where
  list := xs.list.zipWith f ys.list
  lengthOk := byα:Type uβ:Type uγ:Type ?u.3289n:Natf:α → β → γxs:LenList n αys:LenList n β⊢ (List.zipWith f xs.list ys.list).length = n
    cases xsmkα:Type uβ:Type uγ:Type ?u.3289n:Natf:α → β → γys:LenList n βlist✝:List αlengthOk✝:list✝.length = n⊢ (List.zipWith f { list := list✝, lengthOk := lengthOk✝ }.list ys.list).length = n; cases ysmk.mkα:Type uβ:Type uγ:Type ?u.3289n: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
    simp [List.length_zipWith, *]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 := fs.zipWith (· ·) (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 := byα:Type un:Natxs:LenList n α⊢ xs.list.length = n
  cases xsmkα:Type un:Natlist✝:List αlengthOk✝:list✝.length = n⊢ { list := list✝, lengthOk := lengthOk✝ }.list.length = n
  simp [*]All goals completed! 🐙

def LenList.diagonal (square : LenList n (LenList n α)) : LenList n α :=
  match n with
  | 0 => ⟨[], rfl⟩
  | n' + 1 => {
    list :=
      square.head.head :: (square.tail.map (·.tail)).diagonal.list
    lengthOk := byα:Type uβ:Type un:Natn':Natsquare:LenList (n' + 1) (LenList (n' + 1) α)⊢ (square.head.head :: (diagonal (map (fun x => x.tail) square.tail)).list).length = n' + 1 simpAll goals completed! 🐙
  }

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

Applicative f

Methods

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

Inherited from

Applicative f

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

Inherited from

Applicative f

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

Inherited from

Applicative f

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

Inherited from

Applicative f

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

Inherited from

Applicative f

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

Inherited from

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 >>= operator is overloaded via instances of bind.

Bind is typically used via Monad, which extends it.

Instance Constructor

Bind.mk.{u, v}

Methods

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

Sequences two computations, allowing the second to depend on the value computed by the first.

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.

Conventions for notations in identifiers:

The recommended spelling of >>= in identifiers is bind.

type class

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

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.

The Monad API may be used directly. However, it is most commonly accessed through do-notation.

Most Monad instances provide implementations of pure and bind, and use default implementations for the other methods inherited from Applicative. Monads should satisfy certain laws, but instances are not required to prove this. An instance of LawfulMonad expresses that a given monad's operations are lawful.

Instance Constructor

Monad.mk.{u, v}

Extends

Applicative m
Bind m

Methods

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

Inherited from

Applicative m
Bind m

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

Inherited from

Applicative m
Bind m

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

Inherited from

Applicative m
Bind m

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

Inherited from

Applicative m
Bind m

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

Inherited from

Applicative m
Bind m

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

Inherited from

Applicative m
Bind m

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

Inherited from

Applicative m
Bind m

14. Functors, Monads and do-Notation🔗

Instance Constructor

Methods

Instance Constructor

Methods

Instance Constructor

Methods

Instance Constructor

Methods

Instance Constructor

Methods

Instance Constructor

Extends

Methods

Instance Constructor

Extends

Methods

Instance Constructor

Methods

Instance Constructor

Extends

Methods

14. Functors, Monads and `do`-Notation🔗