Re: [Haskell-cafe] Fwd: Questions about lambda calculus

Thanks a lot Ryan. That's exactly what I was looking for. Patrick On Wed, Nov 10, 2010 at 12:36 PM, Ryan Ingram wrote:

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

-- ===================== Patrick LeBoutillier Rosemère, Québec, Canada