[Haskell-cafe] Clean proof -- correction

[Lennart Augustsson]

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 <rj248842 at 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 at hotmail.com
> To: haskell-cafe at 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 at haskell.org
> http://www.haskell.org/mailman/listinfo/haskell-cafe
>
>