Church.hs

{-# LANGUAGE RankNTypes #-}

-- Church encoding of various data-types.
-- Very much inspired by Gabriel Gonzalez's talk "Internet of Code":
-- http://begriffs.com/posts/2015-10-16-internet-of-code.html
module Church where

import Prelude hiding (map, sum, foldr, and, not)

-- List

-- data List a = Cons a (List a) | Nil

type List a = forall list . (a -> list -> list) -> list -> list

list :: List Int
list = \cons nil -> cons 1 (cons 2 (cons 3 nil))

map :: (a -> b) -> List a -> List b
map f l = \cons nil -> l
  (\a as -> cons (f a) as)
  nil

toList :: List a -> [a]
toList l = l
  (\a as -> a : as)
  []

foldr :: (a -> b -> b) -> b -> List a -> b
foldr f x l = l f x

sum :: List Int -> Int
sum l = foldr (+) 0 l -- = l (+) 0

-- Natural numbers

-- data Nat = S Nat | Z

type Nat = forall nat . (nat -> nat) -> nat -> nat

zero, one, two :: Nat
zero = \s z -> z
one  = \s z -> s z
two  = \s z -> s (s z)

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

plus :: Nat -> Nat -> Nat
plus n m = \s z -> m s (n s z)

natList :: List Nat
natList = \cons nil -> cons zero (cons one (cons two nil))

intList :: List Int
-- intList = map toInt natList
intList = \cons nil -> natList (cons . toInt) nil

-- Booleans

-- data Boolean = True | False

type Boolean = forall bool . bool -> bool -> bool

false, true :: Boolean
true  = \t f -> t
false = \t f -> f

toBool :: Boolean -> Bool
toBool b = b True False

not :: Boolean -> Boolean
not x = \t f -> x f t

and :: Boolean -> Boolean -> Boolean
and x y = \t f -> x (y t f) f

-- Pairs

-- data Pair a b = Pair a b

type Pair a b = forall pair . (a -> b -> pair) -> pair

pair :: a -> b -> Pair a b
pair x y = \p -> p x y

first :: Pair a b -> a
first p = p (\x y -> x)

second :: Pair a b -> b
second p = p (\x y -> y)

-- IO

{-
data I_O a = GetLine (String -> I_O a)
           | PutLine String (I_O a)
           | Pure a

runIO :: I_O a -> IO a
runIO (GetLine f)     = do x <- getLine; runIO (f x)
runIO (PutLine str f) = do putStrLn str; runIO f
runIO (Pure x)        = return x
-}

type I_O a = forall io . ((String -> io) -> io) -> -- ^ GetLine
                         (String -> io -> io) ->   -- ^ PutLine
                         (a -> io) ->              -- ^ Pure
                         io

ioPure :: a -> I_O a
ioPure x = \_ _ pure -> pure x

ioGetLine :: (String -> I_O a) -> I_O a
ioGetLine f getLine putLine pure = getLine next
  where next s = f s getLine putLine pure

ioPutLine :: String -> I_O a -> I_O a
ioPutLine str f getLine putLine pure = putLine str next
  where next = f getLine putLine pure

runIO :: I_O a -> IO a
runIO io = io
  (\f     -> getLine >>= f)
  (\str f -> putStrLn str >> f)
  pure