Parigot/Church-Scott encoding of naturals in CoC (by way of Idris)

Para2.idr

Fix : (Type -> Type) -> Type
Fix f = {x : Type} -> (f x -> x) -> x

fold : Functor f => {x : Type} -> (f x -> x) -> Fix f -> x
fold k t = t k

embed : Functor f => f (Fix f) -> Fix f
embed s k = k (map (fold k) s)

project : Functor f => Fix f -> f (Fix f)
project = fold (map embed)

data PNatF : Type -> Type where
    PNF : {a : Type} -> ({b : Type} -> (Maybe (Unit -> b, a) -> b) -> b) -> PNatF a

unPNF : {a : Type} -> PNatF a -> ({b : Type} -> (Maybe (Unit -> b, a) -> b) -> b)
unPNF (PNF x) = x

{- instance -} Functor PNatF where
    map f (PNF x) = PNF (\g => x ((g Nothing) `maybe` (\(y, z) => g (Just (y, f z)))))

PNat : Type
PNat = Fix PNatF

pzero : PNat
pzero = embed (PNF (\f => f Nothing))

psucc : PNat -> PNat
psucc n = embed (PNF (\f => f (Just (\_ => unPNF (project n) f, n))))

pone : PNat
pone = psucc pzero

ptwo : PNat
ptwo = psucc pone

pthree : PNat
pthree = psucc ptwo

elimPNat : {a : Type} -> (Maybe PNat -> a) -> PNat -> a
elimPNat f n = let n' = unPNF (project n) in n' ((\_ => f Nothing) `maybe` (\(_, g), _ => f (Just g))) ()

piszero : PNat -> Bool
piszero = elimPNat (True `maybe` const False)

ppred : PNat -> Maybe PNat
ppred = elimPNat (Nothing `maybe` Just)

ptpred : PNat -> PNat
ptpred = elimPNat (pzero `maybe` id)

toPNat : Nat -> PNat
toPNat Z = pzero
toPNat (S n) = psucc (toPNat n)

fromPNat : PNat -> Nat
fromPNat n = unPNF (project n) (Z `maybe` (\(m, _) => S (m ())))

data PLstF : Type -> Type -> Type where
    PLF : {a : Type} -> {b : Type} -> ({c : Type} -> (Maybe (a, Unit -> c, b) -> c) -> c) -> PLstF a b

unPLF : {a : Type} -> {b : Type} -> PLstF a b -> ({c : Type} -> (Maybe (a, Unit -> c, b) -> c) -> c)
unPLF (PLF x) = x

{- instance -} Functor (PLstF a) where
    map f (PLF x) = PLF (\g => x ((g Nothing) `maybe` (\(y, z, t) => g (Just (y, z, f t)))))

PLst : Type -> Type
PLst a = Fix (PLstF a)

pnil : {a : Type} -> PLst a
pnil = embed (PLF (\f => f Nothing))

pcons : {a : Type} -> a -> PLst a -> PLst a
pcons x xs = embed (PLF (\f => f (Just (x, (\_ => let (PLF xs') = project xs in xs' f), xs))))

elimPLst : {a : Type} -> {b : Type} -> (Maybe (b, PLst b) -> a) -> PLst b -> a
elimPLst f xs = let (PLF xs') = project xs in xs' ((\_ => f Nothing) `maybe` (\(z, _, zs), _ => f (Just (z, zs)))) ()

pisnil : {a : Type} -> PLst a -> Bool
pisnil = elimPLst (True `maybe` const False)