Lennart wasn't pointing out a typo. He was pointing out a fundamental
issue with such identities in a partial call-by-name language. If
h = const 42
then
(h . either (f, g)) undefined
evaluates to 42. But the evaluation of
(either (h . f, h . g)) undefined
is non-terminating.
This is a canonical example of an equation that holds in a partial
call-by-value language but not in a partial call-by-name language:
CBV has more sum equations; CBN has more product equations.
-Per
2010/5/23 R J
Correction: the theorem is h . either (f, g) = either (h . f, h . g)
(Thanks to Lennart for pointing out the typo.) ________________________________ From: rj248842@hotmail.com To: haskell-cafe@haskell.org Subject: Clean proof? Date: Sun, 23 May 2010 15:41:20 +0000
Given the following definition of "either", from the prelude: either :: (a -> c, b -> c) -> Either a b -> c either (f, g) (Left x) = f x either (f, g) (Right x) = g x what's a clean proof that: h . either (f, g) = either (h . f, g . h)? The only proof I can think of requires the introduction of an anonymous function of z, with case analysis on z (Case 1: z = Left x, Case 2: z = Right y), but the use of anonymous functions and case analysis is ugly, and I'm not sure how to tie up the two cases neatly at the end. For example here's the "Left" case: h . either (f, g) = {definition of "\"} \z -> (h . either (f, g)) z = {definition of "."} \z -> (h (either (f, g) z) = {definition of "either" in case z = Left x} \z -> (h (f x)) = {definition of "."} \z -> (h . f) x = {definition of "."} h . f
Thanks. ________________________________ The New Busy is not the too busy. Combine all your e-mail accounts with Hotmail. Get busy. ________________________________ The New Busy is not the old busy. Search, chat and e-mail from your inbox. Get started. _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe