Actually, I didn't notice the typo. It's still not a true statement.
(h . either (f, g)) undefined /= (either (h . f, h . g)) undefined
Also, it's not exactly the function either from the Prelude.
-- Lennart
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