Max Bolingbroke batterseapower at hotmail.com
Wed Nov 10 09:18:10 EST 2010

```On 10 November 2010 12:49, Patrick LeBoutillier
<patrick.leboutillier at gmail.com> wrote:
> I'm a total newbie with respect to the lambda calculus. I tried
> (naively) to port
> these examples to Haskell to play a bit with them:
>
> [snip]

You can give type signatures to your first definitions like this:

"""
{-# LANGUAGE RankNTypes #-}

type FBool = forall r. r -> r -> r

fTRUE, fFALSE :: FBool
fTRUE = \a -> \b -> a
fFALSE = \a -> \b -> b

fIF :: FBool -> a -> a -> a
fIF = \b -> \x -> \y -> b x y

type FPair a b = forall r. (a -> b -> r) -> r

fPAIR :: a -> b -> FPair a b
fPAIR   = \a -> \b -> \f -> f a b

fFIRST :: FPair a b -> a
fFIRST  = \p -> p (\a _ -> a) -- Original won't type check since I
gave fTRUE a restrictive type sig

fSECOND :: FPair a b -> b
fSECOND = \p -> p (\_ b -> b)
"""

has a different type to fZERO. What you want is a system where natural
numbers all have the same types.

One way to do this is to represent the natural number n by the
function that applies a functional argument n times. These are called
Church numerals (http://en.wikipedia.org/wiki/Church_encoding):

"""
type FNat = forall r. (r -> r) -> r -> r

fZERO :: FNat
fZERO = \_ -> id

fSUCC :: FNat -> FNat
fSUCC = \x f -> f . x f

fIS_ZERO :: FNat -> FBool
fIS_ZERO = \x -> x (\_ -> fFALSE) fTRUE

fADD :: FNat -> FNat -> FNat
fADD = \x y f -> x f . y f

fONE :: FNat
fONE = fSUCC fZERO
"""

Try it out:

"""
main = do
putStrLn \$ showFNat \$ fZERO
putStrLn \$ showFNat \$ fONE
putStrLn \$ showFBool \$ fIS_ZERO fZERO
putStrLn \$ showFBool \$ fIS_ZERO fONE
putStrLn \$ showFNat \$ fADD fONE fONE
"""

Exercise: define fPRED in this system :-)

Cheers,
Max
```