[Haskell-cafe] Clean proof -- correction

R J rj248842 at hotmail.com
Sun May 23 12:24:50 EDT 2010

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.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://www.haskell.org/pipermail/haskell-cafe/attachments/20100523/e834f1b1/attachment-0001.html

More information about the Haskell-Cafe mailing list