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)
> 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)
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
ListL has to be explicitly built, so there is no infinite
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)
> type ListG a = GFix (F a)
ListG can be constructed out of
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
force witnesses the isomorphism between
> force :: Functor f => GFix f -> LFix f > force = inL . fmap force . outG -- recursion!
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]
force has to be defined using general recursion. The price is that it is now possible to write programs that do not terminate.