Nat Para + Cata

Nat.hs

module Nat (
       -- types
       Algebra
     , Coalgebra
     , NatF
     -- data
     , Fix
     , N
     , Nat
       -- methods
     , ncata
     , npara
     , successor
     , zero
     , cata
     , toInt
     , toIntF
     , nadd
     , nmult
     , mult
     , plus
   ) where

data Nat = Zero | Succ Nat

ncata :: a -> (a -> a) -> Nat -> a
ncata z f Zero     = z
ncata z f (Succ n) = f (ncata z f n)


npara :: a -> (Nat -> a -> a) -> Nat -> a
npara z f Zero       = z
npara z f n@(Succ m) = f n (npara z f m)

-- lol nadd
nadd :: Nat -> Nat -> Nat
nadd n = ncata n (Succ)

nmult :: Nat -> Nat -> Nat
nmult n = error "not implemented" -- Implement in terms of para + cata

toInt :: Nat -> Int
toInt = npara 0 (\a b -> 1 + b)

-- Nat pattern functor
data N a = Z | S a

instance Functor N where
  fmap f Z = Z
  fmap f (S n) = S (f n)

newtype Fix f = Fix { unfix :: f (Fix f) }

type NatF = Fix N
type Algebra f a  = f a -> a 
type Coalgebra f a = (a -> f a)

successor :: NatF -> NatF 
successor = Fix . S

zero :: NatF
zero = Fix Z

cata :: Functor f => Algebra f a -> Fix f -> a
cata φ = φ . fmap (cata φ) . unfix

plus :: NatF -> NatF -> NatF
plus n = cata alg where
  alg Z = n
  alg (S m) = successor m

mult :: NatF -> NatF -> NatF
mult n = cata alg where
  alg Z = zero
  alg (S m) = plus n m

toIntF :: NatF -> Int
toIntF = cata alg where
  alg Z = 0
  alg (S n) = 1 + n