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 <rj248842@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@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 <daniel.is.fischer@web.de> wrote:
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 <rj248842@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@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