[Haskell-beginners] understanding curried function calls

[Dimitri DeFigueiredo]

Fantastic Gesh! That's much more clear now. These are the rules I 
wanted. I will try to apply them everywhere to practice now. I think the 
rule

\x y -> b
is equivalent to
\x -> \y -> b

is what I was missing to avoid the confusion when trying to evaluate
expressions with multi-parameter functions.

Thanks,

Dimitri



Em 20/08/14 18:14, Gesh escreveu:
> On 2014-08-20 11:19, Dimitri DeFigueiredo wrote:
>> What is the systematic way to evaluate these expressions?
> The canonical evaluation of Haskell is given by the Report[0].
> Among other things, it gives, in chapter 3, the semantics of Haskell
> constructs.
>
> However, since Haskell's semantics resemble those of lambda calculus[1]
> so much, we (or at least I) usually use lambda calculus semantics to
> reason about Haskell code, keeping in mind the how Haskell expressions
> desugar.
>
> In our case, the relevant syntactic sugar is that
> > f x = b
> is equivalent to
> > f = \x -> b
> that
> > \x y -> b
> is equivalent to
> > \x -> \y -> b
> and that function application is left-associative. That means that
> > f x y
> is equivalent to
> > (f x) y
>
> Returning to your examples, they give us:
> > ex1 = doTwice doTwice -- inlining the definition of doTwice
> >     = (\f x -> f (f x)) doTwice -- beta reduction
> >     = \x -> doTwice (doTwice x) -- inline doTwice
> >     = \x -> doTwice ((\f y -> f (f y)) x) -- beta
> >     = \x -> doTwice (\y -> x (x y)) -- inline doTwice
> >     = \x -> (\f z -> f (f z)) (\y -> x (x y)) -- beta
> >     = \x -> (\z -> (\y -> x (x y)) ((\w -> x (x w)) z)) -- beta
> >     = \x -> (\z -> (\y -> x (x y)) (x (x z))) -- beta
> >     = \x -> (\z -> x (x (x (x z)))) -- combining lambdas
> >     = \x z -> x (x (x z)) -- irreducible
> And similarly, combining steps for brevity:
> > -- Proposition:
> > foldl f a xs = foldr (\e g b -> g (f b e)) id bs a
> >
> > -- Proof: By decomposition into constructor cases
> >
> > -- Case []
> > foldl f a [] = a
> > foldr (\e g b -> g (f b e)) id [] a
> >     = (foldr (\e g b -> g (f b e)) id []) a
> >     = id a
> >     = a
> >
> > -- Case (:)
> > -- Induction hypothesis:
> > -- foldl f a xs = foldr (\e g b -> g (f b e)) id xs a
> > -- for all f, a
> > foldl f a (x:xs) = foldl f (f a x) xs
> > foldr (\e g b -> g (f b e)) id (x:xs) a
> >     = (foldr (\e g b -> g (f b e)) id (x:xs)) a
> >     = ((\e g b -> g (f b e)) x (foldr (\e g b -> g (f b e)) id xs)) a
> >     = (\b -> foldr (\e g b -> g (f b e)) id xs (f b x)) a
> >     = foldr (\e g b -> g (f b e)) id xs (f a x)
> >     = foldl f (f a x) xs
>
> Hope this helps,
> Gesh
>
> [0] - https://www.haskell.org/onlinereport/haskell2010/
> [1] - https://en.wikipedia.org/wiki/Lambda_calculus#Reduction
> _______________________________________________
> Beginners mailing list
> Beginners at haskell.org
> http://www.haskell.org/mailman/listinfo/beginners