[Haskell-cafe] Fwd: Questions about lambda calculus
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)
"""
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
More information about the Haskell-Cafe
mailing list