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.
f x = b is equivalent to f = \x -> b
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 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