module Main where

  import Prelude

  data Id = Id forall a. a -> a

  runId = \id a -> case id of
    Id f -> f a

  data Nat = Nat forall r. r -> (r -> r) -> r

  runNat = \nat -> case nat of
    Nat f -> f 0 (\n -> n + 1)

  zero' = Nat (\zero' _ -> zero')

  succ = \n -> case n of
    Nat f -> Nat (\zero' succ -> succ (f zero' succ))

  add = \n m -> case n of
    Nat f -> case m of
      Nat g -> Nat (\zero' succ -> g (f zero' succ) succ)

  one' = succ zero'
  two = succ zero'
  four = add two two
  fourNumber = runNat four

  main = Debug.Trace.trace "Done'"