# Encoding Inductive and Coinductive Types in Polymorphic Lambda Calculus

### Inductive types

Inductive types are least fixed-points. An indcutive type μF is simulated by

`` forall x . (F x -> x) -> x``

In Haskell, we need a constructor to wrap a “forall” quantifier.

``````> newtype LFix f = LF (forall x. (f x -> x) -> x)
> instance Show (LFix f) where
>   show _ = ""

> foldL :: Functor f => (f x -> x) -> LFix f -> x
> foldL f (LF x) = x f

> inL :: Functor f => f (LFix f) -> LFix f
> inL fx = LF (\\f -> f . fmap (foldL f) \$ fx)

> outL :: Functor f => LFix f -> f (LFix f)
> outL = foldL (fmap inL)
``````

Example: lists.

``````> data F a x = L | R a x deriving Show
> instance Functor (F a) where
>   fmap f L = L
>   fmap f (R a x) = R a (f x)

> type ListL a = LFix (F a)
``````

A `ListL` can only be constructed out of nil and cons.

``````    Main> consL 1 (consL 2 (consL 3 nilL))

``````
``````> nilL = inL L
> consL a x = inL (R a x)
``````

We can convert a ListL to a ‘real’ Haskell list.

``````
Main> lList \$ consL 1 (consL 2 (consL 3 nilL))
[1,2,3]
``````
``````> lList :: LFix (F a) -> [a]
> lList = foldL ll
>   where ll L = []
>         ll (R a x) = a : x
``````

However, a `ListL` has to be explicitly built, so there is no infinite `ListL`.

### Coinductive types

A coinductive type νF is simulatd by

`````` exists x . (x -> F x, x)
``````

We represent it in Haskell using the property `exists x . F x == forall y . (forall x . F x -> y) -> y`:

``````> data GFix f = forall x . GF (x -> f x, x)
> instance Show (GFix f) where
>   show _ = ""

> unfoldG :: Functor f => (x -> f x) -> x -> GFix f
> unfoldG g x = GF (g,x)

> outG :: Functor f => GFix f -> f (GFix f)
> outG (GF (g,x)) = fmap (unfoldG g) . g \$ x

> inG :: Functor f => f (GFix f) -> GFix f
> inG = unfoldG (fmap outG)
``````

Example:

``````> type ListG a = GFix (F a)
``````

`ListG` can be constructed out of `nil` and `cons`, as well as an unfold.

``````> nilG = inG L
> consG a x = inG (R a x)

> fromG :: Int -> ListG Int
> fromG m = unfoldG ft m
>    where ft m = R m (m+1)
``````

However, one can perform only a finite number of outG.

``````  Main> fmap outG . outG . fromG \$ 1
R 1 (R 2 )
``````

### Isomorphism

The function `force` witnesses the isomorphism between `LFix` and `GFix`.

``````> force :: Functor f => GFix f -> LFix f
> force = inL . fmap force . outG     -- recursion!
``````

If `LFix` and `GFix` are isomorphic, we are allowed to build hylomorphisms:

``````> fromTo :: Int -> Int -> LFix (F Int)
> fromTo m n = takeLessThan n . force . fromG \$ m

> takeLessThan :: Int -> LFix (F Int) -> LFix (F Int)
> takeLessThan n = foldL (tlt n)
>   where tlt n L = nilL
>         tlt n (R m x) | n <= m = nilL
>                       | otherwise = consL m x

Main> lList (fromTo 1 10)
[1,2,3,4,5,6,7,8,9]
``````

However, `force` has to be defined using general recursion. The price is that it is now possible to write programs that do not terminate.