{-# LANGUAGE RankNTypes #-}
module Nat where

import Prelude hiding (succ, pred)

class Nat a where
  zero :: a
  succ :: a -> a
  pred :: a -> a
  fold :: (b -> b) -> b -> a -> b
  
  toInt :: a -> Int
  toInt =  fold (+ 1) 0

  toNat :: Int -> a
  toNat 0 = zero
  toNat n = succ (toNat (n - 1))

-- Church Encoding
newtype CNat = CNat { unCNat :: forall a . (a -> a) -> a -> a }

instance Nat CNat where
  zero = CNat (\f x -> x)
  succ nat = CNat (\f x -> f (unCNat nat f x))
  pred nat = CNat (\f x -> unCNat nat (\g h -> h (g f)) (const x) id)
  fold s z nat = unCNat nat s z

-- Scott Encoding
newtype SNat = SNat { unSNat :: forall b . (SNat -> b) -> b -> b }

instance Nat SNat where
  zero = SNat (\f x -> x)
  succ nat = SNat (\f x -> f nat)
  fold s z nat = unSNat nat (\p -> s (fold s z p)) z
  pred nat = SNat (unSNat nat unSNat undefined)

-- Parigot Encoding
newtype PNat = PNat { unPNat :: forall b . (b -> PNat -> b) -> b -> b }

instance Nat PNat where
  zero = PNat (\f x -> x)
  succ nat = PNat (\f x -> f (unPNat nat f x) nat)
  fold s z nat = unPNat nat (\n p -> s n) z
  pred nat = unPNat nat (\n p -> p) undefined

-- Alternative Encoding
newtype ANat = ANat { unANat :: forall b . ((ANat -> b) -> ANat -> b) -> b -> b }

instance Nat ANat where
  zero = ANat (\f x -> x)
  succ nat = ANat (\f x -> f (\c -> unANat c f x) nat)
  fold s z nat = unANat nat (\cont p -> s (cont p)) z
  pred nat = unANat nat (\cont p -> p) undefined

-- Tests
testNat :: Nat a => a -> IO ()
testNat x = let printNat n = putStr (show . toInt $ n) >> putStr " " in
  do printNat x
     printNat $ pred x
     printNat $ succ x
     putStrLn []

test :: IO ()
test = do
  testNat (toNat 3 :: CNat)
  testNat (toNat 3 :: SNat)
  testNat (toNat 3 :: PNat)
  testNat (toNat 3 :: ANat)

main :: IO ()
main = test