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 <rj248842@hotmail.com>:
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