[Haskell-cafe] Fwd: Questions about lambda calculus

[Max Bolingbroke]

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)
"""

Your fADD doesn't type check because with those definitions e.g. fONE
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