ADTs and μ-recursive types

import Prelude hiding (length, succ)


-- Product type (a × b)

data Prod a b = Prod a b

pair :: a -> b -> Prod a b
pair = Prod

prj1 :: Prod a b -> a
prj1 (Prod a _) = a

prj2 :: Prod a b -> b
prj2 (Prod _ b) = b


-- Sum type (a + b)

data Sum a b = Inl a | Inr b

inl :: a -> Sum a b
inl = Inl

inr :: b -> Sum a b
inr = Inr

sumCase :: Sum a b -> (a -> c) -> (b -> c) -> c
sumCase (Inl a) f _ = f a
sumCase (Inr b) _ g = g b


{-
data Bool = True | False
data Bool = True () | False ()

Bool = 1 + 1
-}

type Bool' = Sum () ()

true' :: Bool'
true' = inl ()

false' :: Bool'
false' = inr ()


data MaybeInt = Nothing | Just Int

{-
data MaybeInt = Nothing () | Just Int

MaybeInt = 1 + Int
-}

type MaybeInt' = Sum () Int

nothing' :: MaybeInt'
nothing' = inl ()

just' :: Int -> MaybeInt'
just' i = inr i


isJust :: MaybeInt' -> Bool'
isJust m = sumCase m (\_ -> true') (\_ -> false')


-----------------------------------------------------------


data Mu x = Fold (x (Mu x))

fold :: x (Mu x) -> Mu x
fold = Fold

unfold :: Mu x -> x (Mu x)
unfold (Fold a) = a


{-
data Nat = Zero | Succ Nat
data Nat = Zero () | Succ Nat

Nat = 1 + Nat
Nat = μ x . 1 + x
-}

newtype Nat' x = Nat (Sum () x)
type Nat = Mu Nat'

zero :: Nat
zero = fold . Nat $ inl ()

succ :: Nat -> Nat
succ n = fold . Nat $ inr n


{-
data NatList = Nil | Cons Nat NatList
data NatList = Nil () | Cons (Nat, NatList)

NatList = 1 + (Nat * NatList)
NatList = μ x . 1 + (Nat * x)
-}

newtype NatList' x = NatList' { unNatList :: Sum () (Prod Nat x) }
type NatList = Mu NatList'

nil :: NatList
nil = fold . NatList' $ inl ()

cons :: Nat -> NatList -> NatList
cons x xs = fold . NatList' $ inr (pair x xs)

length :: NatList -> Nat
length xs = sumCase (unNatList . unfold $ xs) (\() -> zero) (\p -> succ (length (prj2 p)))

sum :: NatList -> Nat
sum = undefined  -- Ex.


-- Exercise: type NatTree


-------------------------------------------------------


-- bad

{-
type Bad = Bad -> Bad
-}

data Bad' x = BadF (x -> x)
type Bad = Mu Bad'

apply :: Bad -> Bad -> Bad
apply f x = let (BadF f') = unfold f in f' x

foo :: Bad
foo = fold . BadF $ \b -> apply b b

zoo :: Bad
zoo = apply foo foo

-- Exercise: fixpoint combinator