[Haskell-cafe] Clean proof?

[Lennart Augustsson]

There is no clean proof of that statement because it is false.
(Consider the argument 'undefined'.)

2010/5/23 R J <rj248842 at hotmail.com>:
> 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.
> _______________________________________________
> Haskell-Cafe mailing list
> Haskell-Cafe at haskell.org
> http://www.haskell.org/mailman/listinfo/haskell-cafe
>
>