MyNum.hs

newtype MyNum a r = MyNum { unNum :: ((MyNum a r -> r) -> r -> r) }

zero :: MyNum a r
zero = MyNum (\f x -> x)

mySucc :: MyNum a r -> MyNum a r
mySucc n = MyNum (\f x -> f n)

one :: MyNum a r
one = mySucc zero

two :: MyNum a r
two = mySucc one

myPlus :: MyNum t r -> MyNum a r -> MyNum a r
myPlus (MyNum n) m =
  MyNum $ \f x -> n (\n' -> unNum (mySucc (myPlus n' m)) f x) (unNum m f x)

myMult :: MyNum t r -> MyNum a r -> MyNum a r
myMult (MyNum n) m =
  MyNum $ \f x -> n (\n' -> unNum (myPlus (myMult n' m) m) f x) x

toInt :: MyNum t Int -> Int
toInt (MyNum n) = n (\n' -> (toInt n') + 1) 0

myPred :: MyNum a r -> MyNum a r
myPred (MyNum n) = MyNum $ \f x -> n (\(MyNum n') -> n' f x) x

myMinus :: MyNum a r -> MyNum t r -> MyNum a r
myMinus n (MyNum m) =
  MyNum $ \f x -> m (\m' -> unNum (myPred (myMinus n m')) f x) (unNum n f x)

myTrue :: t -> u -> t
myTrue x y = x

myFalse :: t -> u -> u
myFalse x y = y

myIsZero :: MyNum t a -> (a -> a -> a)
myIsZero (MyNum n) x y = n (\x -> y) x

myAnd :: (t2 -> t1 -> t3) -> (t -> t1 -> t2) -> t -> t1 -> t3
myAnd a b x y = a (b x y) y

myEquals :: MyNum t1 t2 -> MyNum t t2 -> t2 -> t2 -> t2
myEquals m n =
  myAnd (myIsZero (myMinus n m)) (myIsZero (myMinus m n))

myFact (MyNum n) =
  MyNum $ \f x -> n (\n' -> unNum (myMult (myFact n') (MyNum n)) f x) (unNum one f x)

test =
  [myEquals zero zero True False == True
  ,myEquals one zero True False == False
  ,myEquals one one True False == True
  ,myEquals (myPlus one one) two True False == True
  ,myEquals (myPlus one two) two True False == False
  ,myEquals (myMinus (myPlus two two) one) (myPlus one two) True False == True
  ,myEquals (myMinus (myPlus two two) one) (myPlus one one) True False == False
  ,toInt (myFact (myPlus two two)) == 24
  ]