Recently I found this blog post about representable functors in Haskell. The example section lacks on detailed explanation on the infinite list functor. Thus, I decided to prove that infinite lists are representable by the type of natural numbers.

# Basic definitions

We begin with basic definitions of natural numbers

```
> data Nat = Zero | Succ Nat
```

and infinite lists (also called streams)

```
> data Stream a = Cons { head :: a , tail :: Stream a }
```

The instance for `Functor`

is now straightforward:

```
> instance Functor Stream where
> fmap f (Cons x xs) = f x `Cons` fmap f xs
```

The stream of all natural numbers is defined as follows.

```
> nats :: Stream Nat
> nats = Zero `Cons` fmap Succ nats
```

# The isomorphism between `Stream a`

and `Nat -> a`

To prove that the stream functor is representable by natural numbers we need to establish an isomorphism between `Nat -> a`

and `Stream a`

, which is defined by `alpha`

and `beta`

as follows.

```
> alpha :: (Nat -> a) -> Stream a
> alpha f = fmap f nats
>
> beta :: Stream a -> (Nat -> a)
> beta xs = \n -> xs!!n
```

The function `beta`

uses the usual index-based accessor:

```
> (!!) :: Stream a -> Nat -> a
> stream !! Zero = head stream
> stream !! (Succ m) = tail stream !! m
```

We need to show the isomorphism law for `alpha`

and `beta`

:

`beta . alpha = id = alpha . beta`

## beta . alpha = id

```
(beta . alpha) f
= beta $ fmap f nats
= \x -> fmap f nats !! x
```

Two functions are semantically equal if their behaviour on every input equals. Thus we prove by induction that

`(\x -> fmap f nats !! x) n `

equals `f n`

for every natural number n and an arbitrary function `f :: Nat -> a`

.

### Base case: n = Zero

```
(\x -> fmap f nats !! x) Zero
= fmap f nats !! Zero
= fmap f (Zero `Cons` fmap Succ nats) !! Zero
= (f Zero `Cons` fmap f (fmap Succ) nats) !! Zero
= f Zero
```

### Induction step: n = Succ m

```
(\x -> fmap f nats !! x) (Succ m)
= fmap f nats !! Succ m
= tail (fmap f nats) !! m
= tail (fmap f (Zero `Cons` fmap Succ nats)) !! m
= tail (h Zero `Cons` fmap f (fmap Succ nats)) !! m
= fmap f (fmap Succ nats) !! m
= fmap (f . Succ) nats !! m -- induction hypothesis
= (f . Succ) m
= f (Succ m)
```

## alpha . beta = id

```
(alpha . beta) xs
= alpha $ \n -> xs !! n
= fmap (\n -> xs !! n) nats
```

Two streams are equal if their values on every position equal. Hence, we show that

`xs!!i = (fmap (\n -> xs !! n) nats) !! i`

holds for every natural number i.

### Base case: i = Zero

```
fmap (\n -> xs !! n) nats !! Zero
= fmap (\n -> xs !! n) (Zero `Cons` fmap Succ nats) !! Zero
= ((\n -> xs !! n) Zero `Cons` fmap (\n -> xs !! n) (fmap Succ Nats)) !! Zero
= (\n -> xs !! n) Zero
= xs !! Zero
```

### Induction step: i = Succ j

```
fmap (\n -> xs !! n) nats !! Succ j
= fmap (\n -> xs !! n) (Zero `Cons` fmap Succ nats) !! Succ j
= ((\n -> xs !! n) Zero `Cons` fmap (\n -> xs !! n) (fmap Succ nats)) !! Succ j
= fmap (\n -> xs !! n) (fmap Succ nats) !! j
= fmap ((\n -> xs !! n) . Succ) nats !! j
= fmap (\n -> xs !! Succ n) nats !! j
= fmap (\n -> tail xs !! n) nats !! j -- induction hypothesis
= tail xs !! j
= xs !! (Succ j)
```