Correction: the theorem is h . either (f, g) = either (h . f, h . g) (Thanks to Lennart for pointing out the typo.) From: rj248842@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. http://www.windowslive.com/campaign/thenewbusy?ocid=PID28326::T:WLMTAGL:ON:W...
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
Correction: the theorem is h . either (f, g) = either (h . f, h . g)
(Thanks to Lennart for pointing out the typo.) ________________________________ From: rj248842@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
On Sunday 23 May 2010 18:24:50, R J wrote:
Correction: the theorem is h . either (f, g) = either (h . f, h . g)
Still not entirely true, const True . either (undefined, undefined) $ undefined = True while either (const True . undefined, const True . undefined) undefined = undefined But if we ignore bottom, h . either (f, g) $ Left x = h (either (f,g) (Left x)) = h (f x) either (h . f, h . g) $ Left x = (h . f) x = h (f x) ---- h . either (f,g) $ Right y = h (either (f,g) (Right y)) = h (g y) either (h .f, h . g) $ Right y = (h . g) y = h (g y)
On Sun, May 23, 2010 at 11:38 AM, Daniel Fischer
On Sunday 23 May 2010 18:24:50, R J wrote:
Correction: the theorem is h . either (f, g) = either (h . f, h . g)
Still not entirely true,
const True . either (undefined, undefined) $ undefined = True
while
either (const True . undefined, const True . undefined) undefined = undefined
But if we ignore bottom,
If we ignore bottom we say "By parametricity." The theorem is a free theorem.
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
Correction: the theorem is h . either (f, g) = either (h . f, h . g)
(Thanks to Lennart for pointing out the typo.) ________________________________ From: rj248842@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
participants (5)
-
Daniel Fischer -
Derek Elkins -
Lennart Augustsson -
Per Vognsen -
R J