linusyang · November 26, 2015 08:59 · Nov 26, 2015
diff --git a/Nat.hs b/Nat.hs
@@ -0,0 +1,71 @@
+{-# 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
No results found