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 <rj248...@hotmail.com>:
> Correction: the theorem is
> h . either (f, g) = either (h . f, h . g)
>
> (Thanks to Lennart for pointing out the typo.)
> ________________________________
> From: rj248...@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
>
>
_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
