# 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 vf : 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 vf, Pure: (Type u → Type v) → Type (max (u + 1) v)Pure f: Type u → Type vf, Seq: (Type u → Type v) → Type (max (u + 1) v)Seq f: Type u → Type vf, SeqLeft: (Type u → Type v) → Type (max (u + 1) v)SeqLeft f: Type u → Type vf, SeqRight: (Type u → Type v) → Type (max (u + 1) v)SeqRight f: Type u → Type vf 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 fPure (f: Type u → Type vf : 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 vf α: 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:

```#evalsome 10
(pure: {f : Type → Type} → [self : Pure f] → {α : Type} → α → f αpure 10: Nat10 : Option: Type → TypeOption Nat: TypeNat)  -- some 10```

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 Optioninstance : Monad: (Type u_1 → Type u_1) → Type (u_1 + 1)Monad Option: Type u_1 → Type u_1Option 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 fSeq (f: Type u → Type vf : 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 vf (α: Type uα → β: Type uβ) → (Unit: TypeUnit → f: Type u → Type vf α: Type uα) → f: Type u → Type vf β: 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:

```#check_failuresome 4 * some 5 : ?m.4196 (some: {α : Type} → α → Option αsome 4: Nat4) * (some: {α : Type} → α → Option αsome 5: Nat5)some 4 * some 5 : ?m.4196Warning: failed to synthesize instance
HMul (Option Nat) (Option Nat) ?m.4196      -- failed to synthesize instance```

You then might wonder how to use the `Functor.map` to solve this since you could do these before:

```#evalsome 20
(some: {α : Type} → α → Option αsome 4: Nat4).map: {α β : Type} → (α → β) → Option α → Option βmap (fun x: Natx => x: Natx * 5: Nat5)  -- some 20

#evalsome 20
(some: {α : Type} → α → Option αsome 4: Nat4).map: {α β : Type} → (α → β) → Option α → Option βmap (· * 5): Nat → Nat(· * 5)  -- some 20

#evalsome 20
(· * 5): Nat → Nat(· * 5) <\$> (some: {α : Type} → α → Option αsome 4: Nat4)   -- some 20```

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:

```#evalsome 20
pure: {f : Type → Type} → [self : Pure f] → {α : Type} → α → f αpure (.*.): Nat → Nat → Nat(.*.) <*> some: {α : Type} → α → Option αsome 4: Nat4 <*> some: {α : Type} → α → Option αsome 5: Nat5 -- some 20

#evalsome 20
(.*.): Nat → Nat → Nat(.*.) <\$> some: {α : Type} → α → Option αsome 4: Nat4 <*> some: {α : Type} → α → Option αsome 5: Nat5 -- some 20```

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:

```#evalnone
(.*.): Nat → Nat → Nat(.*.) <\$> none: {α : Type} → Option αnone <*> some: {α : Type} → α → Option αsome 5: Nat5  -- none
#evalnone
(.*.): Nat → Nat → Nat(.*.) <\$> some: {α : Type} → α → Option αsome 4: Nat4 <*> none: {α : Type} → Option αnone  -- none```

For a more interesting example, let's make `List` an applicative by adding the following definition:

```instance: Applicative Listinstance : Applicative: (Type u_1 → Type u_1) → Type (u_1 + 1)Applicative List: Type u_1 → Type u_1List 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:

```#eval[6, 8]
[ (·+2): Nat → Nat(·+2)] <*> [4: Nat4, 6: Nat6] -- [6, 8]
#eval[6, 8]
(·+2): Nat → Nat(·+2) <\$> [4: Nat4,6: Nat6]    -- [6, 8]```

But now with list it is easier to show the difference when you do this:

```#eval[6, 8, 12, 18]
[(·+2): Nat → Nat(·+2), (· *3): Nat → Nat(· *3)] <*> [4: Nat4, 6: Nat6] -- [6, 8, 12, 18]```

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?

```#eval[(1, 4), (1, 5), (1, 6), (2, 4), (2, 5), (2, 6), (3, 4), (3, 5), (3, 6)]
Prod.mk: {α β : Type} → α → β → α × βProd.mk <\$> [1: Nat1, 2: Nat2, 3: Nat3] <*> [4: Nat4, 5: Nat5, 6: Nat6]
-- [(1, 4), (1, 5), (1, 6), (2, 4), (2, 5), (2, 6), (3, 4), (3, 5), (3, 6)]```

How do you get the sum of these pairwise values?

```#eval[5, 6, 7, 6, 7, 8, 7, 8, 9]
(·+·): Nat → Nat → Nat(·+·) <\$> [1: Nat1, 2: Nat2, 3: Nat3] <*> [4: Nat4, 5: Nat5, 6: Nat6]
-- [5, 6, 7, 6, 7, 8, 7, 8, 9]```

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 `(·,·,·)`:

```#eval[(1, 3, 5), (1, 3, 6), (1, 4, 5), (1, 4, 6), (2, 3, 5), (2, 3, 6), (2, 4, 5), (2, 4, 6)]
(·,·,·): Nat → Nat → Nat → Nat × Nat × Nat(·,·,·) <\$> [1: Nat1, 2: Nat2] <*> [3: Nat3, 4: Nat4] <*> [5: Nat5, 6: 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)]```

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 `(·+·+·)`:

```#eval[9, 10, 10, 11, 10, 11, 11, 12]
(·+·+·): Nat → Nat → Nat → Nat(·+·+·) <\$> [1: Nat1, 2: Nat2] <*> [3: Nat3, 4: Nat4] <*> [5: Nat5, 6: Nat6]
-- [9, 10, 10, 11, 10, 11, 11, 12]```

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`:

```#eval[5, 7, 9]
List.zipWith: {α β γ : Type} → (α → β → γ) → List α → List β → List γList.zipWith (·+·): Nat → Nat → Nat(·+·) [1: Nat1, 2: Nat2, 3: Nat3] [4: Nat4, 5: Nat5, 6: Nat6]
-- [5, 7, 9]```

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:

```#eval[(1, 4), (2, 5), (3, 6)]
List.zip: {α β : Type} → List α → List β → List (α × β)List.zip [1: Nat1, 2: Nat2, 3: Nat3] [4: Nat4, 5: Nat5, 6: Nat6]
-- [(1, 4), (2, 5), (3, 6)]```

And of couse, as you would expect, there is an `unzip` also:

```#eval([1, 2, 3], [4, 5, 6])
List.unzip: {α β : Type} → List (α × β) → List α × List βList.unzip (List.zip: {α β : Type} → List α → List β → List (α × β)List.zip [1: Nat1, 2: Nat2, 3: Nat3] [4: Nat4, 5: Nat5, 6: Nat6])
-- ([1, 2, 3], [4, 5, 6])```

## 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 → TypeLivingSpace (α: Typeα : Type: Type 1Type) where
totalSize: {α : Type} → LivingSpace α → αtotalSize : α: Typeα
numBedrooms: {α : Type} → LivingSpace α → NatnumBedrooms : Nat: TypeNat
masterBedroomSize: {α : Type} → LivingSpace α → αmasterBedroomSize : α: Typeα
livingRoomSize: {α : Type} → LivingSpace α → αlivingRoomSize : α: Typeα
kitchenSize: {α : Type} → LivingSpace α → αkitchenSize : α: Typeα
deriving Repr: Type u → Type uRepr, BEq: Type u → Type uBEq

def LivingSpace.map: {α β : Type} → (α → β) → LivingSpace α → LivingSpace βLivingSpace.map (f: α → βf : α: Typeα → β: Typeβ) (s: LivingSpace αs : LivingSpace: Type → TypeLivingSpace α: Typeα) : LivingSpace: Type → TypeLivingSpace β: Typeβ :=
{ totalSize := f: α → βf s: LivingSpace αs.totalSize: {α : Type} → LivingSpace α → αtotalSize
numBedrooms := s: LivingSpace αs.numBedrooms: {α : Type} → LivingSpace α → NatnumBedrooms
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 LivingSpaceinstance : Functor: (Type → Type) → Type 1Functor LivingSpace: Type → TypeLivingSpace 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:

```#evalsome 2
(some: {α : Type} → α → Option αsome 1: Nat1) *> (some: {α : Type} → α → Option αsome 2: Nat2) -- Some 2
#evalsome 1
(some: {α : Type} → α → Option αsome 1: Nat1) <* (some: {α : Type} → α → Option αsome 2: Nat2) -- Some 1```

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 somthing interesting:

```#evalsome 20
Seq.seq: {f : Type → Type} → [self : Seq f] → {α β : Type} → f (α → β) → (Unit → f α) → f βSeq.seq ((.*.): Nat → Nat → Nat(.*.) <\$> some: {α : Type} → α → Option αsome 4: Nat4) (fun (_: Unit_ : Unit: TypeUnit) => some: {α : Type} → α → Option αsome 5: Nat5) -- some 20```

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!