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.
f x = b is equivalent to f = \x -> b
In our case, the relevant syntactic sugar is that 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@haskell.org http://www.haskell.org/mailman/listinfo/beginners