Scott encoding of naturals with reduction

scottencoding.hs

{-# LANGUAGE RankNTypes #-}

-- You can safely ignore the types. They're necessary for the
-- program to compile, but they don't change the behaviour of
-- the program in any way.
newtype Nat = Nat (forall a. a -> (Nat -> a) -> a)

-- zero = \x y -> x
zeroN :: Nat
zeroN = Nat (\x y -> x)

-- succ = \n -> \x y -> y n
succN :: Nat -> Nat
succN n = Nat (\x y -> y n)

-- reduce = \s z -> \n -> n z (s . reduce s z)
reduceN :: (a -> a) -> a -> Nat -> a
reduceN s z (Nat n) = n z (s . reduceN s z)

-- toInt = reduce (+ 1) 0
toInt :: Nat -> Int
toInt = reduceN (+ 1) 0

{-
  In pure, untyped lambda calculus (untested)
  
  zero = \x y -> x
  succ = \n -> \x y -> y n
  
  (f . g) = \a -> f (g a)
  
  reduce = \s z -> \n -> n z (s . reduce s z)
  
  Or using fix
  
  fix = \f -> (\a -> f (a a)) (\a -> f (a a))
  reduce = \s z -> fix (\f n -> n z (s . f))
  
  toInt = reduce (+ 1) 0
-}