Skip to content
{{ message }}

Instantly share code, notes, and snippets.

# CarstenKoenig/Church.hs

Created Nov 5, 2014
Some fun with churchs lambda calculus in haskell
 {-# LANGUAGE RankNTypes #-} module Church where import Prelude hiding (succ, pred, and, or, not, fst, snd, head, tail) newtype Boolean = Bo (forall a . a -> a -> a) true :: Boolean true = Bo (\ t _ -> t) false :: Boolean false = Bo (\ _ f -> f) instance Show Boolean where show (Bo f) = f "true" "false" and :: Boolean -> Boolean -> Boolean and (Bo b) c = b c false or :: Boolean -> Boolean -> Boolean or (Bo b) c = b true c not :: Boolean -> Boolean not (Bo b) = b false true newtype Pair a b = Pr (forall c . (a -> b -> c) -> c) instance (Show a, Show b) => Show (Pair a b) where show (Pr p) = p (\ a b -> "(" ++ show a ++ "," ++ show b ++ ")") pair :: a -> b -> Pair a b pair f s = Pr (\ b -> b f s) fst :: Pair a b -> a fst (Pr p) = p (\ a _ -> a) snd :: Pair a b -> b snd (Pr p) = p (\ _ b -> b) newtype Number = Nr (forall a. (a -> a) -> a -> a) instance Show Number where show (Nr a) = a ("1+" ++) "0" instance Num Number where fromInteger n | n < 0 = error "cannot convert negative numbers" | n == 0 = zero | otherwise = succ (fromInteger \$ n-1) a + b = add a b a - b = subt a b a * b = mult a b abs _ = error "not implemented" signum _ = error "not implemented" eval :: Number -> Integer eval (Nr a) = a (+1) 0 zero :: Number zero = Nr (\ _ z -> z) succ :: Number -> Number succ (Nr a) = Nr (\ s z -> s (a s z)) add :: Number -> Number -> Number add (Nr a) = a succ mult :: Number -> Number -> Number mult (Nr a) b = a (add b) zero one :: Number one = succ zero two :: Number two = succ one three :: Number three = succ two four :: Number four = succ three five :: Number five = succ four pow :: Number -> Number -> Number pow x (Nr n) = n (mult x) one isZero :: Number -> Boolean isZero (Nr n) = n (\ _ -> false) true -- | the most impressive implementation of the predecessor function pred :: Number -> Number pred (Nr n) = fst (n ss zz) where zz = pair zero zero ss p = pair (snd p) (succ \$ snd p) subt :: Number -> Number -> Number subt a (Nr b) = b pred a isEqual :: Number -> Number -> Boolean isEqual a b = isZero (subt a b) `and` isZero (subt b a) -- * Lists newtype List a = L (forall s . (a -> s -> s) -> s -> s) instance Show a => Show (List a) where show (L l) = show \$ l (:) [] nil :: List a nil = L (\ _ n -> n) cons :: a -> List a -> List a cons h (L tl) = L (\ c n -> c h (tl c n)) infixr 3 +: (+:) :: a -> List a -> List a (+:) = cons isNil :: List a -> Boolean isNil (L l) = l (\ _ _ -> false) true -- I have to cheat a bit here with undefined head :: List a -> a head (L l) = l (\ a _ -> a) undefined tail :: List a -> List a tail (L l) = fst (l ss nn) where nn = pair nil nil ss a p = pair (snd p) (a +: snd p)
to join this conversation on GitHub. Already have an account? Sign in to comment