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:

some 10
 (
pure: {f : Type → Type} → [self : Pure f] → {α : Type} → α → f α
pure 
10: Nat
10 : 
Option: Type → Type
Option 
Nat: Type
Nat)  -- 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 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:

some 4 * some 5 : ?m.925
 
some 4 * some 5 : ?m.925
Warning: failed to synthesize
  HMul (Option Nat) (Option Nat) ?m.925
Additional diagnostic information may be available using the `set_option diagnostics true` command.
      -- failed to synthesize instance

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

some 20
 (
some: {α : Type} → α → Option α
some 
4: Nat
4).
map: {α β : Type} → (α → β) → Option α → Option β
map (fun 
x: Nat
x => 
x: Nat
x * 
5: Nat
5)  -- some 20


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


some 20
 
(· * 5): Nat → Nat
(· * 5) <$> (
some: {α : Type} → α → Option α
some 
4: Nat
4)   -- 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:

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


some 20
 
(.*.): Nat → Nat → Nat
(.*.) <$> 
some: {α : Type} → α → Option α
some 
4: Nat
4 <*> 
some: {α : Type} → α → Option α
some 
5: Nat
5 -- 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:

none
 
(.*.): Nat → Nat → Nat
(.*.) <$> 
none: {α : Type} → Option α
none <*> 
some: {α : Type} → α → Option α
some 
5: Nat
5  -- none

none
 
(.*.): Nat → Nat → Nat
(.*.) <$> 
some: {α : Type} → α → Option α
some 
4: Nat
4 <*> 
none: {α : Type} → Option α
none  -- none

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.singleton: {α : Type u_1} → α → List α
List.singleton
  seq 
f: List (α✝ → β✝)
f 
x: Unit → List α✝
x := 
List.flatMap: {α β : Type u_1} → List α → (α → List β) → List β
List.flatMap 
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:

[6, 8]
 [ 
(·+2): Nat → Nat
(·+2)] <*> [
4: Nat
4, 
6: Nat
6] -- [6, 8]

[6, 8]
 
(·+2): Nat → Nat
(·+2) <$> [
4: Nat
4,
6: Nat
6]    -- [6, 8]

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

[6, 8, 12, 18]
 [
(·+2): Nat → Nat
(·+2), 
(· *3): Nat → Nat
(· *3)] <*> [
4: Nat
4, 
6: Nat
6] -- [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?

[(1, 4), (1, 5), (1, 6), (2, 4), (2, 5), (2, 6), (3, 4), (3, 5), (3, 6)]
 
Prod.mk: {α β : Type} → α → β → α × β
Prod.mk <$> [
1: Nat
1, 
2: Nat
2, 
3: Nat
3] <*> [
4: Nat
4, 
5: Nat
5, 
6: Nat
6]
-- [(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?

[5, 6, 7, 6, 7, 8, 7, 8, 9]
 
(·+·): Nat → Nat → Nat
(·+·) <$> [
1: Nat
1, 
2: Nat
2, 
3: Nat
3] <*> [
4: Nat
4, 
5: Nat
5, 
6: Nat
6]
-- [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 (·,·,·):

[(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: Nat
1, 
2: Nat
2] <*> [
3: Nat
3, 
4: Nat
4] <*> [
5: Nat
5, 
6: Nat
6]
-- [(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 (·+·+·):

[9, 10, 10, 11, 10, 11, 11, 12]
 
(·+·+·): Nat → Nat → Nat → Nat
(·+·+·) <$> [
1: Nat
1, 
2: Nat
2] <*> [
3: Nat
3, 
4: Nat
4] <*> [
5: Nat
5, 
6: Nat
6]
-- [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:

[5, 7, 9]
 
List.zipWith: {α β γ : Type} → (α → β → γ) → List α → List β → List γ
List.zipWith 
(·+·): Nat → Nat → Nat
(·+·) [
1: Nat
1, 
2: Nat
2, 
3: Nat
3] [
4: Nat
4, 
5: Nat
5, 
6: Nat
6]
-- [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:

[(1, 4), (2, 5), (3, 6)]
 
List.zip: {α β : Type} → List α → List β → List (α × β)
List.zip [
1: Nat
1, 
2: Nat
2, 
3: Nat
3] [
4: Nat
4, 
5: Nat
5, 
6: Nat
6]
-- [(1, 4), (2, 5), (3, 6)]

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

([1, 2, 3], [4, 5, 6])
 
List.unzip: {α β : Type} → List (α × β) → List α × List β
List.unzip (
List.zip: {α β : Type} → List α → List β → List (α × β)
List.zip [
1: Nat
1, 
2: Nat
2, 
3: Nat
3] [
4: Nat
4, 
5: Nat
5, 
6: Nat
6])
-- ([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 → 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:

some 2
 (
some: {α : Type} → α → Option α
some 
1: Nat
1) *> (
some: {α : Type} → α → Option α
some 
2: Nat
2) -- Some 2

some 1
 (
some: {α : Type} → α → Option α
some 
1: Nat
1) <* (
some: {α : Type} → α → Option α
some 
2: Nat
2) -- 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 something interesting:

some 20
 
Seq.seq: {f : Type → Type} → [self : Seq f] → {α β : Type} → f (α → β) → (Unit → f α) → f β
Seq.seq (
(.*.): Nat → Nat → Nat
(.*.) <$> 
some: {α : Type} → α → Option α
some 
4: Nat
4) (fun (
_: Unit
_ : 
Unit: Type
Unit) => 
some: {α : Type} → α → Option α
some 
5: Nat
5) -- 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!