Encoding Inductive and Coinductive Types in Polymorphic Lambda Calculus

This was written about two years ago. Mostly inspired by Philip Wadler‘s note Recursive types for free.

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.

Leave a Comment

Your email address will not be published. Required fields are marked *