Create a gist now

Instantly share code, notes, and snippets.

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)
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment