[Haskell-cafe] Fwd: Questions about lambda calculus

[Patrick LeBoutillier]

Thanks a lot Ryan. That's exactly what I was looking for.

Patrick


On Wed, Nov 10, 2010 at 12:36 PM, Ryan Ingram <ryani.spam at gmail.com> 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
> <patrick.leboutillier at gmail.com> 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 <patrick.leboutillier at gmail.com>
>> Date: Thu, Nov 4, 2010 at 2:02 PM
>> Subject: Questions about lambda calculus
>> To: beginners <beginners at haskell.org>
>>
>>
>> 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 at haskell.org
>> http://www.haskell.org/mailman/listinfo/haskell-cafe
>>
>



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