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.
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).
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.
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.
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.
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(LenListn)wheremap:=LenList.mappurex:={list:=List.replicatenxlengthOk:=List.length_replicate__}seqfsxs:=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]theoremLenList.list_length_eq(xs:LenListnα):xs.list.length=n:=α:Type un:Natxs:LenListnα⊢ xs.list.length = nα:Type un:Natlist✝:ListαlengthOk✝:list✝.length = n⊢ { list := list✝, lengthOk := lengthOk✝ }.list.length = nAll goals completed! 🐙deffail 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:LenListn(LenListnα)):LenListnα:=matchnwith|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'}
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.
Depending on the Alternative instance, collects values or recovers from failures by
returning the leftmost success. Can be written using the <|> operator syntax.
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.