The functor of infinite lists is representable by natural numbers

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)							 
Advertisements