[Haskell-cafe] Fwd: Questions about lambda calculus

[Ryan Ingram]

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
>