# Proofs of functor laws in Haskell

Haskell defines a typeclass `Functor`

containing a function `fmap`

which allows developers to apply a function over the contents of an instance without changing the actual structure of the data (note that this is roughly equivalent to the formal definition of a functor). To achieve this guarantee, instances of `Functor`

must obey the following two laws where `fmap :: (a -> b) -> f a -> f b`

, `id :: a -> a`

, `f :: b -> c`

, and `g :: a -> b`

:

`fmap id == id`

`fmap (f . g) == (fmap f . fmap g)`

Proving these laws on different instances is a useful exercise, especially when you come up with your own instance for an arbitrary data structure and you need to verify that it is correct, so let’s prove them on two instances of `Functor`

: `Maybe a`

and `[a]`

. For all the non-Haskellers out there, the former is a data structure that implements nullable values of `a`

, and the latter is a list of `a`

’s.

## Nullable values: The `Maybe a`

functor

A value of `Maybe a`

is either `Just a`

or `Nothing`

; the instance should allow us to apply a function on either `a`

in `Just a`

or fail silently on `Nothing`

without changing anything else. Therefore, `fmap`

is defined as the following.

```
instance Functor Maybe where
fmap _ Nothing = Nothing (1)
fmap f (Just a) = Just (f a) (2)
```

These proofs are fairly straightforward and follow the common theme of considering either case of `Maybe a`

.

### Proof of the first law

**Claim**: *On* `m`

*of* `Maybe a`

, `fmap id m == id m`

.

*Proof*. On cases of `m`

.

* Case 1*:

`m == Nothing`

.```
fmap id m == fmap id Nothing {- by expansion of m -}
== Nothing {- by fmap (1) -}
== id m {- by definition of id, m -}
```

* Case 2*:

`m == Just a`

.```
fmap id m == fmap id (Just a) {- by expansion of m -}
== Just (id a) {- by fmap (2) -}
== Just a {- by expansion of id -}
== m {- by definition of m -}
== id m {- by definition of id -} ∎
```

### Proof of the second law

**Claim**: *On* `m`

*of* `Maybe a`

, `fmap (f . g) m == (fmap f . fmap g) m`

.

*Proof*. On cases of `m`

.

* Case 1*:

`m == Nothing`

.```
fmap (f . g) m == fmap (f . g) Nothing
{- by expansion of m -}
== Nothing
{- by fmap (1) -}
```

```
(fmap f . fmap g) m == fmap f (fmap g Nothing)
{- by expansion of (.) and m -}
== fmap f Nothing
{- by fmap (1) -}
== Nothing
{- by fmap (1) -}
```

* Case 2*:

`m == Just a`

.```
fmap (f . g) m == fmap (f . g) (Just a)
{- by expansion of m -}
== Just ((f . g) a)
{- by fmap (2) -}
```

```
(fmap f . fmap g) m == fmap f (fmap g (Just a))
{- by expansion of (.), m -}
== fmap f (Just (g a))
{- by fmap (2) -}
== Just (f (g a))
{- by fmap (2) -}
== Just ((f . g) a)
{- by definition of (.) -}
```

Therefore, `fmap (f . g) m == (fmap f . fmap g) m`

in all cases. ∎

## Lists: The `[a]`

functor

The `[a]`

functor should allow us to apply a function to every element of a list without changing anything else. Thus, `fmap = map`

, which is defined as the following.

```
map :: (a -> b) -> [a] -> [b]
map _ [] = [] (1)
map f (x:xs) = f x : map f xs (2)
```

The proofs here are a bit harder since lists have infinitely many cases to consider, so we must turn to induction.

### Proof of the first law

**Claim**: *On a list* `l`

, `fmap id l == id l`

.

*Proof*. By induction on the length of `l`

.

* Base case*: On a list where

`length l == 0`

, i.e. `l = []`

.```
fmap id l == map id [] {- by expansion of fmap, l -}
== [] {- by map (1) -}
== id [] {- by definition of id -}
```

* Inductive hypothesis*: Assume that

`fmap id l’ == id l’`

where `length l’ < length l`

. Since `l = x:xs`

where `x`

and `xs`

are the head and tail of `l`

, respectively, `fmap id xs == id xs`

as `length xs < length l`

.* Inductive step*:

```
fmap id l == map id (x:xs) {- by expansion of fmap, l -}
== id x : fmap id xs {- by map (2), defn. of fmap -}
== id x : id xs {- by inductive hypothesis -}
== x:xs {- by expansion of id -}
== id l {- by definition of id, l -} ∎
```

### Proof of the second law

**Claim**: *On a list* `l`

, `fmap (f . g) l == (fmap f . fmap g) l`

.

*Proof*. By induction on the length of `l`

.

* Base case*: On a list where

`length l == 0`

i.e. `l = []`

.```
fmap (f . g) l == map (f . g) []
{- by expansion of fmap, l -}
== []
{- by map (1) -}
```

```
(fmap f . fmap g) l == map f (map g [])
{- by expansion of (.), fmap, l -}
== map f []
{- by map (1) -}
== []
{- by map (1) -}
```

* Inductive hypothesis*: Assume that

`fmap (f . g) l’ == (fmap f . fmap g) l’`

where `length l’ < length l`

. Since `l = x:xs`

where `x`

and `xs`

are the head and tail of `l`

, respectively, `fmap (f . g) xs == (fmap f . fmap g) xs`

as `length xs < length l`

.* Inductive step*:

```
fmap (f . g) l == map (f . g) (x:xs)
{- by expansion of fmap, l -}
== (f . g) x : fmap (f . g) xs
{- by map (2), definition of fmap -}
```

```
(fmap f . fmap g) l == map f (map g (x:xs))
{- by expansion of (.), fmap, l -}
== map f (g x : map g xs)
{- by map (2) -}
== f (g x) : map f (map g xs)
{- by map (2) -}
== (f . g) x : fmap f (fmap g xs)
{- by definition of (.), fmap -}
== (f . g) x : (fmap f . fmap g) xs
{- by definition of (.) -}
== (f . g) x : fmap (f . g) xs
{- by inductive hypothesis -}
```

Therefore, `fmap (f . g) l == (fmap f . fmap g) l`

in all cases. ∎

### Was it all for naught?

Turns out these instances of `Functor`

implement `fmap`

correctly. However, turns out proving the second law in any case is redundant due to the free theorem of `fmap`

, but it was fun anyways.