[Haskell-cafe] Clean proof -- correction

[Per Vognsen]

Lennart wasn't pointing out a typo. He was pointing out a fundamental
issue with such identities in a partial call-by-name language. If

    h = const 42

then

    (h . either (f, g)) undefined

evaluates to 42. But the evaluation of

    (either (h . f, h . g)) undefined

is non-terminating.

This is a canonical example of an equation that holds in a partial
call-by-value language but not in a partial call-by-name language:

CBV has more sum equations; CBN has more product equations.

-Per

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
>
>