UPs and F-Algebras.hs

{-# LANGUAGE DeriveFunctor #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE TypeOperators #-}








--
--  Universal Properties
--




-- The initial type

data Zero  -- Void


-- One part of its universal property

initialUP :: forall r.  Zero  ->  r
initialUP _ = undefined



-- Zero -> r  ~==  A subset of Zero x r




-- The final type

data One = Trivial  -- ()


-- One part of its universal property

finalUP :: forall r.  r  ->  One
finalUP _ = Trivial



-- r -> One  ~==   A subset of r x One




-- The product type (remember: projects are part of the product!)

data a :* b = Pair a b

proj1 :: forall a b.  a :* b  ->  a
proj1 (Pair x y) = x

proj2 :: forall a b.  a :* b  ->  b
proj2 (Pair x y) = y


-- One part of its universal property

productUP :: forall a b p.  (p -> a)  ->  (p -> b)  ->  (p -> a :* b)
productUP f g x = Pair (f x) (g x)




-- The coproduct type (injects are part of the corproduct => the constructors)

data a :+ b = InLeft a | InRight b

-- InLeft :: a -> a :+ b
-- InRight :: b -> a :+ b


-- One part of its universal property

coproductUP :: forall a b d.  (a -> d)  ->  (b -> d)  ->  (a :+ b -> d)
coproductUP f g (InLeft x)  = f x
coproductUP f g (InRight y) = g y









--
--  Functor Algebras
--




-- The initial algebra gadget @Mu@

newtype Mu f = In (f (Mu f))

-- In :: f (Mu f) -> Mu f




-- One part of its universal property

fold :: forall f a. Functor f =>  (f a -> a)  ->  (Mu f -> a)
fold alg (In x) = alg (fmap (fold alg) x)

-- fold alg . In  =  alg . fmap (fold alg)




-- The natural number type for reference

{-
  
  data Nat = Zero | Suc Nat
  
-}


-- The natural number functor, as a native Haskell type

data NatF r = ZeroS | SucS r
  deriving (Functor)


type Nat = Mu NatF


zero :: Nat
zero = In ZeroS


suc :: Nat -> Nat
suc n = In (SucS n)





-- The natural number functor, via One, (:*), and (:+)

newtype NatF2 r = NatS2 (One  :+  r)

instance Functor NatF2 where
  fmap f (NatS2 (InLeft x)) = NatS2 (InLeft x)
  fmap f (NatS2 (InRight y)) = NatS2 (InRight (f y))

type Nat2 = Mu NatF2


zero2 :: Nat2
zero2 = In (NatS2 (InLeft Trivial))


suc2 :: Nat2 -> Nat2
suc2 n = In (NatS2 (InRight n))








-- The list type for reference

{-
  
  data List a = Nil | Cons a (List a)
  
-}


-- The list functor, as a native Haskell type

data ListF a r = NilS | ConsS a r
  deriving (Functor)


type List a = Mu (ListF a)


nil :: List a
nil = In NilS


cons :: a -> List a -> List a
cons x xs = In (ConsS x xs)


-- The list functor, via One, (:*), and (:+)

newtype ListF2 a r = ListF2 (One  :+  (a :* r))

instance Functor (ListF2 a) where
  fmap f (ListF2 (InLeft Trivial)) = ListF2 (InLeft Trivial)
  fmap f (ListF2 (InRight (Pair a x))) = ListF2 (InRight (Pair a (f x)))


type List2 a = Mu (ListF2 a)


nil2 :: List2 a
nil2 = In (ListF2 (InLeft Trivial))


cons2 :: a -> List2 a -> List2 a
cons2 x xs = In (ListF2 (InRight (Pair x xs)))





-- The binary tree type for reference

{-
  
  data Tree a = Leaf a | Branch a (Tree a) (Tree a)
  
-}


-- The binary tree functor, as a native Haskell type

data TreeF a r = LeafS a | BranchS a r r
  deriving (Functor)


type Tree a = Mu (TreeF a)


leaf :: a -> Tree a
leaf x = In (LeafS x)


branch :: a -> Tree a -> Tree a -> Tree a
branch x l r = In (BranchS x l r)


-- The binary tree functor, via (:*) and (:+)

newtype TreeF2 a r = TreeF2 (a  :+  (a :* (r :* r)))

instance Functor (TreeF2 a) where
  fmap f (TreeF2 (InLeft x)) = TreeF2 (InLeft x)
  fmap f (TreeF2 (InRight (Pair x (Pair l r)))) =
    TreeF2 (InRight (Pair x (Pair (f l) (f r))))


type Tree2 a = Mu (TreeF2 a)


leaf2 :: a -> Tree2 a
leaf2 x = In (TreeF2 (InLeft x))


branch2 :: a -> Tree2 a -> Tree2 a -> Tree2 a
branch2 x l r = In (TreeF2 (InRight (Pair x (Pair l r))))