Functor

A Functor is any type that can act as a generic container that allows you to transform the underlying values inside the container using a function, so that the values are all updated, but the structure of the container is the same. This is called "mapping".

A List is one of the most basic examples of a Functor.

A list contains zero or more elements of the same, underlying type. When you map a function over a list, you create a new list with the same number of elements, where each has been transformed by the function:

#eval["1", "2", "3"]
 List.map: {α β : Type} → (α → β) → List α → List β
List.map (λ x: Nat
x => toString: {α : Type} → [self : ToString α] → α → String
toString x: Nat
x) [1: Nat
1,2: Nat
2,3: Nat
3] -- ["1", "2", "3"]

-- you can also write this using dot notation on the List object
#eval["1", "2", "3"]
 [1: Nat
1,2: Nat
2,3: Nat
3].map: {α β : Type} → (α → β) → List α → List β
map (λ x: Nat
x => toString: {α : Type} → [self : ToString α] → α → String
toString x: Nat
x)  -- ["1", "2", "3"]

Here we converted a list of natural numbers (Nat) to a list of strings where the lambda function here used toString to do the transformation of each element. Notice that when you apply map the "structure" of the object remains the same, in this case the result is always a List of the same size.

Note that in Lean a lambda function can be written using fun keyword or the unicode symbol λ which you can type in VS code using \la .

List has a specialized version of map defined as follows:

def map: {α : Type u_1} → {β : Type u_2} → (α → β) → List α → List β
map (f: α → β
f : α: Type u_1
α → β: Type u_2
β) : List: Type u_1 → Type u_1
List α: Type u_1
α → List: Type u_2 → Type u_2
List β: Type u_2
β
  | []    => []: List β
[]
  | a: α
a::as: List α
as => f: α → β
f a: α
a :: map: {α : Type u_1} → {β : Type u_2} → (α → β) → List α → List β
map f: α → β
f as: List α
as

This is a very generic map function that can take any function that converts (α → β) and use it to convert List α → List β. Notice the function call f a above, this application of f is producing the converted items for the new list.

Let's look at some more examples:

-- List String → List Nat
#eval[8, 5, 7]
 ["elephant": String
"elephant", "tiger": String
"tiger", "giraffe": String
"giraffe"].map: {α β : Type} → (α → β) → List α → List β
map (fun s: String
s => s: String
s.length: String → Nat
length)
-- [8, 5, 7]

-- List Nat → List Float
#eval[1.000000, 8.000000, 27.000000, 64.000000, 125.000000]
 [1: Nat
1,2: Nat
2,3: Nat
3,4: Nat
4,5: Nat
5].map: {α β : Type} → (α → β) → List α → List β
map (fun s: Nat
s => (s: Nat
s.toFloat: Nat → Float
toFloat) ^ 3.0: Float
3.0)
-- [1.000000, 8.000000, 27.000000, 64.000000, 125.000000]

--- List String → List String
#eval["Chris", "David", "Mark"]
 ["chris": String
"chris", "david": String
"david", "mark": String
"mark"].map: {α β : Type} → (α → β) → List α → List β
map (fun s: String
s => s: String
s.capitalize: String → String
capitalize)
-- ["Chris", "David", "Mark"]

Another example of a functor is the Option type. Option contains a value or nothing and is handy for code that has to deal with optional values, like optional command line arguments.

Remember you can construct an Option using the type constructors some or none:

#checksome 5 : Option Nat some: {α : Type} → α → Option α
some 5: Nat
5 -- Option Nat
#evalsome 5
 some: {α : Type} → α → Option α
some 5: Nat
5  -- some 5
#evalsome 6
 (some: {α : Type} → α → Option α
some 5: Nat
5).map: {α β : Type} → (α → β) → Option α → Option β
map (fun x: Nat
x => x: Nat
x + 1: Nat
1) -- some 6
#evalsome "5"
 (some: {α : Type} → α → Option α
some 5: Nat
5).map: {α β : Type} → (α → β) → Option α → Option β
map (fun x: Nat
x => toString: {α : Type} → [self : ToString α] → α → String
toString x: Nat
x) -- some "5"

Lean also provides a convenient short hand syntax for (fun x => x + 1), namely (· + 1) using the middle dot unicode character which you can type in VS code using \. .

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

The map function preserves the none state of the Option, so again map preserves the structure of the object.

def x: Option Nat
x : Option: Type → Type
Option Nat: Type
Nat := none: {α : Type} → Option α
none
#evalnone
 x: Option Nat
x.map: {α β : Type} → (α → β) → Option α → Option β
map (fun x: Nat
x => toString: {α : Type} → [self : ToString α] → α → String
toString x: Nat
x) -- none
#checkOption.map (fun x => toString x) x : Option String x: Option Nat
x.map: {α β : Type} → (α → β) → Option α → Option β
map (fun x: Nat
x => toString: {α : Type} → [self : ToString α] → α → String
toString x: Nat
x) -- Option String

Notice that even in the none case it has transformed Option Nat into Option String as you see in the #check command.

How to make a Functor Instance?

The List type is made an official Functor by the following type class instance:

instance: Functor List
instance : Functor: (Type u_1 → Type u_1) → Type (u_1 + 1)
Functor List: Type u_1 → Type u_1
List where
  map := List.map: {α β : Type u_1} → (α → β) → List α → List β
List.map

Notice all you need to do is provide the map function implementation. For a quick example, let's supposed you create a new type describing the measurements of a home or apartment:

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

Now you can construct a LivingSpace in square feet using floating point values:

abbrev SquareFeet: Type
SquareFeet := Float: Type
Float

def mySpace: LivingSpace SquareFeet
mySpace : LivingSpace: Type → Type
LivingSpace SquareFeet: Type
SquareFeet :=
  { totalSize := 1800: SquareFeet
1800, numBedrooms := 4: Nat
4, masterBedroomSize := 500: SquareFeet
500,
    livingRoomSize := 900: SquareFeet
900, kitchenSize := 400: SquareFeet
400 }

Now, suppose you want anyone to be able to map a LivingSpace from one type of measurement unit to another. Then you would provide a Functor instance as follows:

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

Notice this functor instance takes LivingSpace and not the fully qualified type LivingSpace SquareFeet. Notice below that LivingSpace is a function from Type to Type. For example, if you give it type SquareFeet it gives you back the fully qualified type LivingSpace SquareFeet.

#checkLivingSpace (α : Type) : Type LivingSpace: Type → Type
LivingSpace -- Type → Type

So the instance : Functor then is operating on the more abstract, or generic LivingSpace saying for the whole family of types LivingSpace α you can map to LivingSpace β using the generic LivingSpace.map map function by simply providing a function that does the more primitive mapping from (f : α → β). So LivingSpace.map is a sort of function applicator. This is called a "higher order function" because it takes a function as input (α → β) and returns another function as output F α → F β.

Notice that LivingSpace.map applies a function f to convert the units of all the LivingSpace fields, except for numBedrooms which is a count (and therefore is not a measurement that needs converting).

So now you can define a simple conversion function, let's say you want square meters instead:

abbrev SquareMeters: Type
SquareMeters := Float: Type
Float
def squareFeetToMeters: SquareFeet → SquareMeters
squareFeetToMeters (ft: SquareFeet
ft : SquareFeet: Type
SquareFeet ) : SquareMeters: Type
SquareMeters := (ft: SquareFeet
ft / 10.7639104: SquareMeters
10.7639104)

and now bringing it all together you can use the simple function squareFeetToMeters to map mySpace to square meters:

#eval{ totalSize := 167.225472,
  numBedrooms := 4,
  masterBedroomSize := 46.451520,
  livingRoomSize := 83.612736,
  kitchenSize := 37.161216 }
 mySpace: LivingSpace SquareFeet
mySpace.map: {α β : Type} → (α → β) → LivingSpace α → LivingSpace β
map squareFeetToMeters: SquareFeet → SquareMeters
squareFeetToMeters
/-
{ totalSize := 167.225472,
  numBedrooms := 4,
  masterBedroomSize := 46.451520,
  livingRoomSize := 83.612736,
  kitchenSize := 37.161216 }
  -/

Lean also defines custom infix operator <$> for Functor.map which allows you to write this:

#eval[8, 5, 7]
 (fun s: String
s => s: String
s.length: String → Nat
length) <$> ["elephant": String
"elephant", "tiger": String
"tiger", "giraffe": String
"giraffe"] -- [8, 5, 7]
#evalsome 6
 (fun x: Nat
x => x: Nat
x + 1: Nat
1) <$> (some: {α : Type} → α → Option α
some 5: Nat
5) -- some 6

Note that the infix operator is left associative which means it binds more tightly to the function on the left than to the expression on the right, this means you can often drop the parentheses on the right like this:

#evalsome 6
 (fun x: Nat
x => x: Nat
x + 1: Nat
1) <$> some: {α : Type} → α → Option α
some 5: Nat
5 -- some 6

Note that Lean lets you define your own syntax, so <$> is nothing special. You can define your own infix operator like this:

infixr:100 " doodle " => Functor.map: {f : Type u → Type v} → [self : Functor f] → {α β : Type u} → (α → β) → f α → f β
Functor.map

#eval[5, 10, 15]
 (· * 5): Nat → Nat
(· * 5) doodle [1: Nat
1, 2: Nat
2, 3: Nat
3]  -- [5, 10, 15]

Wow, this is pretty powerful. By providing a functor instance on LivingSpace with an implementation of the map function it is now super easy for anyone to come along and transform the units of a LivingSpace using very simple functions like squareFeetToMeters. Notice that squareFeetToMeters knows nothing about LivingSpace.

How do Functors help with Monads ?

Functors are an abstract mathematical structure that is represented in Lean with a type class. The Lean functor defines both map and a special case for working on constants more efficiently called mapConst:

class Functor (f : Type u → Type v) : Type (max (u+1) v) where
  map : {α β : Type u} → (α → β) → f α → f β
  mapConst : {α β : Type u} → α → f β → f α

Note that mapConst has a default implementation, namely: mapConst : {α β : Type u} → α → f β → f α := Function.comp map (Function.const _) in the Functor type class. So you can use this default implementation and you only need to replace it if your functor has a more specialized variant than this (usually the custom version is more performant).

In general then, a functor is a function on types F : Type u → Type v equipped with an operator called map such that if you have a function f of type α → β then map f will convert your container type from F α → 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.

Understanding abstract mathematical structures is a little tricky for most people. So it helps to start with a simpler idea like functors before you try to understand monads. Building on functors is the next abstraction called Applicatives.

Lean Manual

Functor

How to make a Functor Instance?

How do Functors help with Monads ?