# 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`**: **{f : Type u → Type v} → ({α : Type u} → α → f α) → Pure f

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`**: **{f : Type u → Type v} → ({α β : Type u} → f (α → β) → (Unit → f α) → f β) → Seq f

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!