On 10 November 2010 12:49, Patrick LeBoutillier <patrick.leboutill...@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 _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe