Applicative Functors
Building on Functors is the Applicative Functor. For simplicity, you can refer to these simply as "Applicatives". These are a little tricker than functors, but still simpler than monads. Let's see how they work!
What is an Applicative Functor?
An applicative functor defines a default or "base" construction for an object and allows function application to be chained across multiple instances of the structure. All applicative functors are functors, meaning they must also support the "map" operation.
How are Applicatives represented in Lean?
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 pure
operator specifies how you can wrap a normal object α
into an instance of this structure F α
.
This is the "default" mechanism mentioned above.
The seq
operator allows you to chain operations by wrapping a function in a structure. The name
"applicative" comes from the fact that you "apply" functions from within the structure, rather than
simply from outside the structure, as was the case with Functor.map
.
Applicative in Lean is built on some helper type classes, Functor
, Pure
and Seq
:
namespace hidden -- hidden
class Applicative: (Type u → Type v) → Type (max (u + 1) v)
Applicative (f: Type u → Type v
f : Type u: Type (u + 1)
Type u → Type v: Type (v + 1)
Type v) extends Functor: (Type u → Type v) → Type (max (u + 1) v)
Functor f: Type u → Type v
f, Pure: (Type u → Type v) → Type (max (u + 1) v)
Pure f: Type u → Type v
f, Seq: (Type u → Type v) → Type (max (u + 1) v)
Seq f: Type u → Type v
f, SeqLeft: (Type u → Type v) → Type (max (u + 1) v)
SeqLeft f: Type u → Type v
f, SeqRight: (Type u → Type v) → Type (max (u + 1) v)
SeqRight f: Type u → Type v
f where
map := fun x: α✝ → β✝
x y: f α✝
y => Seq.seq: {f : Type u → Type v} → [self : Seq f] → {α β : Type u} → f (α → β) → (Unit → f α) → f β
Seq.seq (pure: {α : Type u} → α → f α
pure x: α✝ → β✝
x) fun _: Unit
_ => y: f α✝
y
seqLeft := fun a: f α✝
a b: Unit → f β✝
b => Seq.seq: {f : Type u → Type v} → [self : Seq f] → {α β : Type u} → f (α → β) → (Unit → f α) → f β
Seq.seq (Functor.map: {f : Type u → Type v} → [self : Functor f] → {α β : Type u} → (α → β) → f α → f β
Functor.map (Function.const: {α : Type u} → (β : Type u) → α → β → α
Function.const _: Type u
_) a: f α✝
a) b: Unit → f β✝
b
seqRight := fun a: f α✝
a b: Unit → f β✝
b => Seq.seq: {f : Type u → Type v} → [self : Seq f] → {α β : Type u} → f (α → β) → (Unit → f α) → f β
Seq.seq (Functor.map: {f : Type u → Type v} → [self : Functor f] → {α β : Type u} → (α → β) → f α → f β
Functor.map (Function.const: {α : Type u} → (β : Type u) → α → β → α
Function.const _: Type u
_ id: {α : Type u} → α → α
id) a: f α✝
a) b: Unit → f β✝
b
end hidden -- hidden
Notice that as with Functor
it is also a type transformer (f : Type u → Type v)
and notice the
extends Functor f
is ensuring the base Functor
also performs that same type transformation.
As stated above, all applicatives are then functors. This means you can assume that map
already
exists for all these types.
The Pure
base type class is a very simple type class that supplies the pure
function.
namespace hidden -- hidden
class Pure: (Type u → Type v) → Type (max (u + 1) v)
Pure (f: Type u → Type v
f : Type u: Type (u + 1)
Type u → Type v: Type (v + 1)
Type v) where
pure: {f : Type u → Type v} → [self : Pure f] → {α : Type u} → α → f α
pure {α: Type u
α : Type u: Type (u + 1)
Type u} : α: Type u
α → f: Type u → Type v
f α: Type u
α
end hidden -- hidden
You can think of it as lifting the result of a pure value to some monadic type. The simplest example
of pure
is the Option
type:
(purepure: {f : Type → Type} → [self : Pure f] → {α : Type} → α → f α10 :10: NatOptionOption: Type → TypeNat) -- some 10Nat: Type
Here we used the Option
implementation of pure
to wrap the Nat 10
value in an Option Nat
type resulting in the value some 10
, and in fact if you look at the Monad instance of Option
, you
will see that pure
is indeed implemented using Option.some
:
instance: Monad Option
instance : Monad: (Type u_1 → Type u_1) → Type (u_1 + 1)
Monad Option: Type u_1 → Type u_1
Option where
pure := Option.some: {α : Type u_1} → α → Option α
Option.some
The Seq
type class is also a simple type class that provides the seq
operator which can
also be written using the special syntax <*>
.
namespace hidden -- hidden
class Seq: (Type u → Type v) → Type (max (u + 1) v)
Seq (f: Type u → Type v
f : Type u: Type (u + 1)
Type u → Type v: Type (v + 1)
Type v) : Type (max (u+1) v): Type ((max (u + 1) v) + 1)
Type (max (u+1) v) where
seq: {f : Type u → Type v} → [self : Seq f] → {α β : Type u} → f (α → β) → (Unit → f α) → f β
seq : {α: Type u
α β: Type u
β : Type u: Type (u + 1)
Type u} → f: Type u → Type v
f (α: Type u
α → β: Type u
β) → (Unit: Type
Unit → f: Type u → Type v
f α: Type u
α) → f: Type u → Type v
f β: Type u
β
end hidden -- hidden
Basic Applicative Examples
Many of the basic functors also have instances of Applicative
.
For example, Option
is also Applicative
.
So let's take a look and what the seq
operator can do. Suppose you want to multiply two Option Nat
objects. Your first attempt might be this:
-- failed to synthesize instance
You then might wonder how to use the Functor.map
to solve this since you could do these before:
(somesome: {α : Type} → α → Option α4).4: Natmap (funmap: {α β : Type} → (α → β) → Option α → Option βx =>x: Natx *x: Nat5) -- some 205: Nat(somesome: {α : Type} → α → Option α4).4: Natmapmap: {α β : Type} → (α → β) → Option α → Option β(· * 5) -- some 20(· * 5): Nat → Nat(· * 5) <$> ((· * 5): Nat → Natsomesome: {α : Type} → α → Option α4) -- some 204: Nat
Remember that <$>
is the infix notation for Functor.map
.
The functor map
operation can apply a multiplication to the value in the Option
and then lift the
result back up to become a new Option
, but this isn't what you need here.
The Seq.seq
operator <*>
can help since it can apply a function to the items inside a
container and then lift the result back up to the desired type, namely Option
.
There are two ways to do this:
purepure: {f : Type → Type} → [self : Pure f] → {α : Type} → α → f α(.*.) <*>(.*.): Nat → Nat → Natsomesome: {α : Type} → α → Option α4 <*>4: Natsomesome: {α : Type} → α → Option α5 -- some 205: Nat(.*.) <$>(.*.): Nat → Nat → Natsomesome: {α : Type} → α → Option α4 <*>4: Natsomesome: {α : Type} → α → Option α5 -- some 205: Nat
In the first way, we start off by wrapping the function in an applicative using pure. Then we apply
this to the first Option
, and again to the second Option
in a chain of operations. So you can see
how Seq.seq
can be chained in fact, Seq.seq
is really all about chaining of operations.
But in this case there is a simpler way. In the second way, you can see that "applying" a single
function to a container is the same as using Functor.map
. So you use <$>
to "transform" the first
option into an Option
containing a function, and then apply this function over the second value.
Now if either side is none
, the result is none
, as expected, and in this case the
seq
operator was able to eliminate the multiplication:
(.*.) <$>(.*.): Nat → Nat → Natnone <*>none: {α : Type} → Option αsomesome: {α : Type} → α → Option α5 -- none5: Nat(.*.) <$>(.*.): Nat → Nat → Natsomesome: {α : Type} → α → Option α4 <*>4: Natnone -- nonenone: {α : Type} → Option α
For a more interesting example, let's make List
an applicative by adding the following
definition:
instance: Applicative List
instance : Applicative: (Type u_1 → Type u_1) → Type (u_1 + 1)
Applicative List: Type u_1 → Type u_1
List where
pure := List.pure: {α : Type u_1} → α → List α
List.pure
seq f: List (α✝ → β✝)
f x: Unit → List α✝
x := List.bind: {α β : Type u_1} → List α → (α → List β) → List β
List.bind f: List (α✝ → β✝)
f fun y: α✝ → β✝
y => Functor.map: {f : Type u_1 → Type u_1} → [self : Functor f] → {α β : Type u_1} → (α → β) → f α → f β
Functor.map y: α✝ → β✝
y (x: Unit → List α✝
x (): Unit
())
Notice you can now sequence a list of functions and a list of items.
The trivial case of sequencing a singleton list is in fact the same as map
, as you saw
earlier with the Option
examples:
[(·+2)] <*> [(·+2): Nat → Nat4,4: Nat6] -- [6, 8]6: Nat(·+2) <$> [(·+2): Nat → Nat4,4: Nat6] -- [6, 8]6: Nat
But now with list it is easier to show the difference when you do this:
[(·+2),(·+2): Nat → Nat(· *3)] <*> [(· *3): Nat → Nat4,4: Nat6] -- [6, 8, 12, 18]6: Nat
Why did this produce 4 values? The reason is because <*>
applies every function to every
value in a pairwise manner. This makes sequence really convenient for solving certain problems. For
example, how do you get the pairwise combinations of all values from two lists?
Prod.mk <$> [Prod.mk: {α β : Type} → α → β → α × β1,1: Nat2,2: Nat3] <*> [3: Nat4,4: Nat5,5: Nat6] -- [(1, 4), (1, 5), (1, 6), (2, 4), (2, 5), (2, 6), (3, 4), (3, 5), (3, 6)]6: Nat
How do you get the sum of these pairwise values?
(·+·) <$> [(·+·): Nat → Nat → Nat1,1: Nat2,2: Nat3] <*> [3: Nat4,4: Nat5,5: Nat6] -- [5, 6, 7, 6, 7, 8, 7, 8, 9]6: Nat
Here you can use <$>
to "transform" each element of the first list into a function, and then apply
these functions over the second list.
If you have 3 lists, and want to find all combinations of 3 values across those lists you
would need helper function that can create a tuple out of 3 values, and Lean provides a
very convenient syntax for that (·,·,·)
:
(·,·,·) <$> [(·,·,·): Nat → Nat → Nat → Nat × Nat × Nat1,1: Nat2] <*> [2: Nat3,3: Nat4] <*> [4: Nat5,5: Nat6] -- [(1, 3, 5), (1, 3, 6), (1, 4, 5), (1, 4, 6), (2, 3, 5), (2, 3, 6), (2, 4, 5), (2, 4, 6)]6: Nat
And you could sum these combinations if you first define a sum function that takes three inputs and
then you could chain apply this over the three lists. Again lean can create such a function
with the expression (·+·+·)
:
(·+·+·) <$> [(·+·+·): Nat → Nat → Nat → Nat1,1: Nat2] <*> [2: Nat3,3: Nat4] <*> [4: Nat5,5: Nat6] -- [9, 10, 10, 11, 10, 11, 11, 12]6: Nat
And indeed each sum here matches the expected values if you manually sum the triples we show above.
Side note: there is another way to combine lists with a function that does not do the pairwise
combinatorics, it is called List.zipWith
:
List.zipWithList.zipWith: {α β γ : Type} → (α → β → γ) → List α → List β → List γ(·+·) [(·+·): Nat → Nat → Nat1,1: Nat2,2: Nat3] [3: Nat4,4: Nat5,5: Nat6] -- [5, 7, 9]6: Nat
And there is a helper function named List.zip
that calls zipWith
using the function Prod.mk
so you get a nice zipped list like this:
List.zip [List.zip: {α β : Type} → List α → List β → List (α × β)1,1: Nat2,2: Nat3] [3: Nat4,4: Nat5,5: Nat6] -- [(1, 4), (2, 5), (3, 6)]6: Nat
And of course, as you would expect, there is an unzip
also:
List.unzip (List.unzip: {α β : Type} → List (α × β) → List α × List βList.zip [List.zip: {α β : Type} → List α → List β → List (α × β)1,1: Nat2,2: Nat3] [3: Nat4,4: Nat5,5: Nat6]) -- ([1, 2, 3], [4, 5, 6])6: Nat
Example: A Functor that is not Applicative
From the chapter on functors you might remember this example of LivingSpace
that had a Functor
instance:
structure LivingSpace: Type → Type
LivingSpace (α: Type
α : Type: Type 1
Type) where
totalSize: {α : Type} → LivingSpace α → α
totalSize : α: Type
α
numBedrooms: {α : Type} → LivingSpace α → Nat
numBedrooms : Nat: Type
Nat
masterBedroomSize: {α : Type} → LivingSpace α → α
masterBedroomSize : α: Type
α
livingRoomSize: {α : Type} → LivingSpace α → α
livingRoomSize : α: Type
α
kitchenSize: {α : Type} → LivingSpace α → α
kitchenSize : α: Type
α
deriving Repr: Type u → Type u
Repr, BEq: Type u → Type u
BEq
def LivingSpace.map: {α β : Type} → (α → β) → LivingSpace α → LivingSpace β
LivingSpace.map (f: α → β
f : α: Type
α → β: Type
β) (s: LivingSpace α
s : LivingSpace: Type → Type
LivingSpace α: Type
α) : LivingSpace: Type → Type
LivingSpace β: Type
β :=
{ totalSize := f: α → β
f s: LivingSpace α
s.totalSize: {α : Type} → LivingSpace α → α
totalSize
numBedrooms := s: LivingSpace α
s.numBedrooms: {α : Type} → LivingSpace α → Nat
numBedrooms
masterBedroomSize := f: α → β
f s: LivingSpace α
s.masterBedroomSize: {α : Type} → LivingSpace α → α
masterBedroomSize
livingRoomSize := f: α → β
f s: LivingSpace α
s.livingRoomSize: {α : Type} → LivingSpace α → α
livingRoomSize
kitchenSize := f: α → β
f s: LivingSpace α
s.kitchenSize: {α : Type} → LivingSpace α → α
kitchenSize }
instance: Functor LivingSpace
instance : Functor: (Type → Type) → Type 1
Functor LivingSpace: Type → Type
LivingSpace where
map := LivingSpace.map: {α β : Type} → (α → β) → LivingSpace α → LivingSpace β
LivingSpace.map
It wouldn't really make sense to make an Applicative
instance here. How would you write pure
in
the Applicative
instance? By taking a single value and plugging it in for total size and the
master bedroom size and the living room size? That wouldn't really make sense. And what would the
numBedrooms value be for the default? What would it mean to "chain" two of these objects together?
If you can't answer these questions very well, then it suggests this type isn't really an Applicative functor.
SeqLeft and SeqRight
You may remember seeing the SeqLeft
and SeqRight
base types on class Applicative
earlier.
These provide the seqLeft
and seqRight
operations which also have some handy notation
shorthands <*
and *>
respectively. Where: x <* y
evaluates x
, then y
, and returns the
result of x
and x *> y
evaluates x
, then y
, and returns the result of y
.
To make it easier to remember, notice that it returns that value that the <*
or *>
notation is
pointing at. For example:
(somesome: {α : Type} → α → Option α1) *> (1: Natsomesome: {α : Type} → α → Option α2) -- Some 22: Nat(somesome: {α : Type} → α → Option α1) <* (1: Natsomesome: {α : Type} → α → Option α2) -- Some 12: Nat
So these are a kind of "discard" operation. Run all the actions, but only return the values that you
care about. It will be easier to see these in action when you get to full Monads, but they are used
heavily in the Lean Parsec
parser combinator library where you will find parsing functions like
this one which parses the XML declaration <?xml version="1.0" encoding='utf-8' standalone="yes">
:
def XMLdecl : Parsec Unit := do
skipString "<?xml"
VersionInfo
optional EncodingDecl *> optional SDDecl *> optional S *> skipString "?>"
But you will need to understand full Monads before this will make sense.
Lazy Evaluation
Diving a bit deeper, (you can skip this and jump to the Applicative
Laws if don't want to dive into this implementation detail right
now). But, if you write a simple Option
example (.*.) <$> some 4 <*> some 5
that produces some 20
using Seq.seq
you will see something interesting:
Seq.seq (Seq.seq: {f : Type → Type} → [self : Seq f] → {α β : Type} → f (α → β) → (Unit → f α) → f β(.*.) <$>(.*.): Nat → Nat → Natsomesome: {α : Type} → α → Option α4) (fun (4: Nat_ :_: UnitUnit) =>Unit: Typesomesome: {α : Type} → α → Option α5) -- some 205: Nat
This may look a bit cumbersome, specifically, why did we need to invent this funny looking function
fun (_ : Unit) => (some 5)
?
Well if you take a close look at the type class definition:
class Seq (f : Type u → Type v) where
seq : {α β : Type u} → f (α → β) → (Unit → f α) → f β
You will see this function defined here: (Unit → f α)
, this is a function that takes Unit
as input
and produces the output of type f α
where f
is the container type Type u -> Type v
, in this example Option
and α
is the element type Nat
, so fun (_ : Unit) => some 5
matches this definition because
it is taking an input of type Unit and producing some 5
which is type Option Nat
.
The that seq
is defined this way is because Lean is an eagerly evaluated language
(call-by-value), you have to use this kind of Unit function whenever you want to explicitly delay
evaluation and seq
wants that so it can eliminate unnecessary function evaluations whenever
possible.
Fortunately the <*>
infix notation hides this from you by creating this wrapper function for you.
If you look up the notation using F12 in VS Code you will find it contains (fun _ : Unit => b)
.
Now to complete this picture you will find the default implementation of seq
on the Lean Monad
type class:
class Monad (m : Type u → Type v) extends Applicative m, Bind m where
seq f x := bind f fun y => Functor.map y (x ())
Notice here that x
is the (Unit → f α)
function, and it is calling that function by passing the
Unit value ()
, which is the Unit value (Unit.unit). All this just to ensure delayed evaluation.
How do Applicatives help with Monads?
Applicatives are helpful for the same reasons as functors. They're a relatively simple abstract structure that has practical applications in your code. Now that you understand how chaining operations can fit into a structure definition, you're in a good position to start learning about Monads!