-- G54FOP
-- Inductive and CoInductive Types

-- In Haskell there is no difference between inductive and coinductive types
-- So (Mu f) and (Nu f) have the same definition
-- But we implement differently the introduction/elimination rules

-- Mu and Nu can be defined for any type operator f
-- But they are useful only when f is a (strictly positive) functor

-- INDUCTIVE TYPES

data Mu f = In (f (Mu f))

cata :: Functor f => (f x -> x) -> Mu f -> x
cata alg (In t) = alg (fmap (cata alg) t)

-- When using (Mu f) we restrict ourselves only to In and cata

-- Natural numbers

type Nat = Mu Maybe

zero :: Nat
zero = In Nothing

sux :: Nat -> Nat
sux n = In (Just n)

-- To be able to print them, we map them to Integers
natToInt :: Nat -> Integer
natToInt = cata alg
  where alg Nothing = 0
        alg (Just n) = n+1

-- Try: natToInt (sux $ sux $ sux zero)

-- COINDUCTIVE TYPES

data Nu f = InNu (f (Nu f))

ana :: Functor f => (x -> f x) -> x -> Nu f
ana coalg x = InNu (fmap (ana coalg) (coalg x))

out :: Nu f -> f (Nu f)
out (InNu t) = t

-- When using (Mu f) we restrict ourselves only to ana and out

-- Streams

type Stream a = Nu ((,) a)

(<:) :: a -> Stream a -> Stream a
(<:) a = ana (\s -> (a,s))
-- we could define it as (a <: s) = InNu (a,s)
-- but we want to use just the rules for Nu: ana and out

hd :: Stream a -> a
hd s = fst (out s)

tl :: Stream a -> Stream a
tl s = snd (out s)

natsFrom :: Integer -> Stream Integer
natsFrom = ana (\n -> (n,n+1))

nats :: Stream Integer
nats = natsFrom 0

-- To be able to print them, we map them to lists
strToList :: Stream a -> [a]
strToList s = hd s : strToList (tl s)

-- Try: take 10 (strToList nats)

-- Infinite Binary Trees

data FTree a x = Node  a x x

instance Functor (FTree a) where
  fmap f (Node a x1 x2) = Node a (f x1) (f x2)

type CoTree a = Nu (FTree a)

label :: CoTree a -> a
label t = let (Node a _ _) = out t in a

left :: CoTree a -> CoTree a
left t = let (Node _ l _) = out t in l

right :: CoTree a -> CoTree a
right t = let (Node _ _ r) = out t in r

mkTree :: a -> CoTree a -> CoTree a -> CoTree a
mkTree = tcurry $ ana (\(a,l,r) -> Node a (outFT l) (outFT r))
   where tcurry g = \a l r -> g (a,l,r)
         outFT t = (label t, left t, right t)
-- we could define it as (mkTree a l r) = InNu (Node a l r)
-- but we want to use just the rules for Nu: ana and out


-- Tree of Depths

depthTree :: Int -> CoTree Int
depthTree = ana (\n -> Node n (n+1) (n+1))

-- Pretty printer for trees
showT :: Show a => CoTree a -> String
showT t = showTree 4 t 0 -- prints to depth 4

showTree :: Show a => Int -> CoTree a -> Int -> String
showTree 0 _ m = spaces m ++ "...\n"
showTree n t m = (showTree (n-1) (left t) (m+5))
                 ++ spaces m ++ (show (label t))++"\n"
                 ++ (showTree (n-1) (right t) (m+5))

spaces :: Int -> String
spaces n = take n (repeat ' ')

-- Try: putStr $ showT (depthTree 0)