# Proof of functor laws for Maybe

*Posted on April 17, 2020 by Thomas Mahler*

In this post I want to give a short example of how equational reasoning can be used to proof certain properties of a given piece of code in Haskell.

So without further ado let’s begin:

## Known facts

The `Functor`

instance declaration of the type `Maybe`

is defined as:

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

The composition operator `(.)`

is defined as:

```
(.) :: (b -> c) -> (a -> b) -> a -> c
. g x = f (g x) -- (3) f
```

The Identity function `id`

is defined as:

```
id :: a -> a
id x = x -- (4)
```

## Claim

The claim is that `Maybe`

fulfils the two functor laws:

```
1.: fmap id = id
2.: fmap (f . g) = (fmap f . fmap g)
```

## Proof of the first law

**Claim:** `fmap id m = id m`

, for any `m`

of type `Maybe a`

.

**Proof.** On cases of `m`

.

*Case 1:* `m = Nothing`

.

```
fmap id m = fmap id Nothing -- by expansion of m
= Nothing -- by applying equation (1)
= id m -- by definition m, by applying equation (4)
```

*Case 2:* `m = Just a`

.

```
fmap id m = fmap id (Just a) -- by expansion of m
= Just (id a) -- by applying equation (2)
= Just a -- by expansion of id (equation (4))
= m -- by definition of m
= id m -- by applying equation (4)
```

Therefore, `fmap id m = id m`

in all cases.∎

## Proof of the second law

**Claim:** `fmap (f . g) m = (fmap f . fmap g) m`

, for any `m`

of type `Maybe a`

.

**Proof.** On cases of `m`

.

*Case 1:* `m = Nothing`

.

```
fmap (f . g) m = fmap (f . g) Nothing -- by expansion of m
= Nothing -- by applying equation (1)
fmap f . fmap g) m = fmap f (fmap g Nothing) -- by applying equation (4) and expanding m
(= fmap f Nothing -- by applying equation (1)
= Nothing -- by applying equation (1)
```

*Case 2:* `m = Just a`

.

```
fmap (f . g) m = fmap (f . g) (Just a) -- by expansion of m
= Just ((f . g) a) -- by applying equation (2)
fmap f . fmap g) m = fmap f (fmap g (Just a)) -- by applying equation (4) and expanding m
(= fmap f (Just (g a)) -- by applying equation (2)
= Just (f (g a) -- by applying equation (2)
= Just ((f . g) a) -- by applying equation (3)
```

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

in all cases. ∎

## Conclusion

You’ll see this kind of reasoning quite a lot in Haskell documentation and online discussions. The simple reason is: if you can prove something you don’t have to test it.