On 10 November 2010 12:49, Patrick LeBoutillier 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

Max has a good solution, but another solution is to embed an untyped lambda calculus into Haskell -- "atom" is just used for output during testing data U = Atom Int | F (U -> U) instance Show U where show (Atom s) = s show (F _) = "<function>" -- function application F f $$ x = f x infixl 9 $$ fTrue = F $ \x -> F $ \y -> x fFalse = F $ \x -> F $ \y -> y fIf = F $ \b -> F $ \x -> F $ \y -> b $$ x $$ y etc. getAtom (Atom x) = x fNat :: U -> U fNat n = fIf $$ (fIsZero $$ n) $$ Atom 0 $$ Atom (getAtom (fNat $$ (fPred $$ n)) + 1) -- getAtom (fNat $$ (fAdd $$ fOne $$ fTwo)) == 3 An even better encoding is this: data UAtom a = Atom a | F (UAtom a -> UAtom a) newtype U = U { unU :: forall a. UAtom a } Notice that there are no objects of type U with any non-bottom Atoms. So you can be more sure there's nothing tricky going on inside, but then when you want to go back to Haskell-land and actually extract information, you can switch to UAtom at whatever type you like. It is still possible to do tricksy stuff like case analyze and do different things to functions and atoms. I'll leave fixing that as an exercise :) ($$) :: U -> U -> U (U (F f)) $$ (U x) = U (f x) lam :: (forall a. UAtom a -> UAtom a) -> U lam f = U (F f) fTrue = lam $ \x -> lam $ \y -> x .. etc. On Wed, Nov 10, 2010 at 4:49 AM, Patrick LeBoutillier wrote:

Hi all,

Sorry for cross-posting this, but I didn't get anything on the beginners list so I thought I'd give it a try here.

Thanks,

Patrick

---------- Forwarded message ---------- From: Patrick LeBoutillier Date: Thu, Nov 4, 2010 at 2:02 PM Subject: Questions about lambda calculus To: beginners

Hi all,

I've been reading this article: http://perl.plover.com/lambda/tpj.html in which the author talks about the lambda calculus and uses examples in Perl (here's a link directly to the code: http://perl.plover.com/lambda/lambda-brief.pl)

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:

fTRUE = \a -> \b -> a fFALSE = \a -> \b -> b

fIF = \b -> \x -> \y -> b x y

fPAIR   = \a -> \b -> \f -> f a b fFIRST  = \p -> p fTRUE fSECOND = \p -> p fFALSE

fZERO    = fPAIR fTRUE fTRUE fSUCC    = \x -> fPAIR fFALSE x fIS_ZERO = \x -> fFIRST x fPRED    = \x -> fSECOND x fONE     = fSUCC fZERO fTWO     = fSUCC fONE

fADD = \m -> (\n -> fIF (fIS_ZERO m) n (fADD (fPRED m) (fSUCC n)))

but I couldn't get fADD to compile:

  Occurs check: cannot construct the infinite type:      t = (t1 -> t1 -> t1) -> t    Probable cause: `fADD' is applied to too many arguments    In the third argument of `fIF', namely `(fADD (fPRED m) (fSUCC n))'    In the expression: fIF (fIS_ZERO m) n (fADD (fPRED m) (fSUCC n))

I think its because in these Perl examples all functions are treated as being of the same type (number or type of args doesn't matter), but this is not the case in Haskell.

Is there any way to create code similar to this in Haskell?

Thanks,

Patrick

-- ===================== Patrick LeBoutillier Rosemère, Québec, Canada _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe