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:
List.map (λList.map: {α β : Type} → (α → β) → List α → List βx =>x: NattoStringtoString: {α : Type} → [self : ToString α] → α → Stringx) [x: Nat1,1: Nat2,2: Nat3] -- ["1", "2", "3"] -- you can also write this using dot notation on the List object3: Nat[1,1: Nat2,2: Nat3].3: Natmap (λmap: {α β : Type} → (α → β) → List α → List βx =>x: NattoStringtoString: {α : Type} → [self : ToString α] → α → Stringx) -- ["1", "2", "3"]x: Nat
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["elephant","elephant": String"tiger","tiger": String"giraffe"]."giraffe": Stringmap (funmap: {α β : Type} → (α → β) → List α → List βs =>s: Strings.s: Stringlength) -- [8, 5, 7] -- List Nat → List Floatlength: String → Nat[1,1: Nat2,2: Nat3,3: Nat4,4: Nat5].5: Natmap (funmap: {α β : Type} → (α → β) → List α → List βs => (s: Nats.s: NattoFloat) ^toFloat: Nat → Float3.0) -- [1.000000, 8.000000, 27.000000, 64.000000, 125.000000] --- List String → List String3.0: Float["chris","chris": String"david","david": String"mark"]."mark": Stringmap (funmap: {α β : Type} → (α → β) → List α → List βs =>s: Strings.s: Stringcapitalize) -- ["Chris", "David", "Mark"]capitalize: String → String
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
:
somesome: {α : Type} → α → Option α5 -- Option Nat5: Natsomesome: {α : Type} → α → Option α5 -- some 55: Nat(somesome: {α : Type} → α → Option α5).5: Natmap (funmap: {α β : Type} → (α → β) → Option α → Option βx =>x: Natx +x: Nat1) -- some 61: Nat(somesome: {α : Type} → α → Option α5).5: Natmap (funmap: {α β : Type} → (α → β) → Option α → Option βx =>x: NattoStringtoString: {α : Type} → [self : ToString α] → α → Stringx) -- some "5"x: Nat
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 \.
.
(somesome: {α : Type} → α → Option α4).4: Natmapmap: {α β : Type} → (α → β) → Option α → Option β(· * 5) -- some 20(· * 5): Nat → Nat
The map
function preserves the none
state of the Option, so again
map preserves the structure of the object.
defx :x: Option NatOptionOption: Type → TypeNat :=Nat: Typenonenone: {α : Type} → Option αx.x: Option Natmap (funmap: {α β : Type} → (α → β) → Option α → Option βx =>x: NattoStringtoString: {α : Type} → [self : ToString α] → α → Stringx) -- nonex: Natx.x: Option Natmap (funmap: {α β : Type} → (α → β) → Option α → Option βx =>x: NattoStringtoString: {α : Type} → [self : ToString α] → α → Stringx) -- Option Stringx: Nat
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
.
LivingSpace -- Type → TypeLivingSpace: 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:
mySpace.mySpace: LivingSpace SquareFeetmapmap: {α β : Type} → (α → β) → LivingSpace α → LivingSpace βsquareFeetToMeters /- { totalSize := 167.225472, numBedrooms := 4, masterBedroomSize := 46.451520, livingRoomSize := 83.612736, kitchenSize := 37.161216 } -/squareFeetToMeters: SquareFeet → SquareMeters
Lean also defines custom infix operator <$>
for Functor.map
which allows you to write this:
(funs =>s: Strings.s: Stringlength) <$> [length: String → Nat"elephant","elephant": String"tiger","tiger": String"giraffe"] -- [8, 5, 7]"giraffe": String(funx =>x: Natx +x: Nat1) <$> (1: Natsomesome: {α : Type} → α → Option α5) -- some 65: Nat
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:
(funx =>x: Natx +x: Nat1) <$>1: Natsomesome: {α : Type} → α → Option α5 -- some 65: Nat
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.mapFunctor.map: {f : Type u → Type v} → [self : Functor f] → {α β : Type u} → (α → β) → f α → f β(· * 5) doodle [(· * 5): Nat → Nat1,1: Nat2,2: Nat3] -- [5, 10, 15]3: Nat
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.