[Haskell-cafe] Clean proof -- correction

2010-05-23 Thread R J
Correction: the theorem is h . either (f, g) = either (h . f, h . g) (Thanks to Lennart for pointing out the typo.) From: rj248...@hotmail.com To: haskell-cafe@haskell.org Subject: Clean proof? Date: Sun, 23 May 2010 15:41:20 + Given the following definition of either, from the

Re: [Haskell-cafe] Clean proof -- correction

2010-05-23 Thread 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.

Re: [Haskell-cafe] Clean proof -- correction

2010-05-23 Thread 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

Re: [Haskell-cafe] Clean proof -- correction

2010-05-23 Thread 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 rj248...@hotmail.com: Correction:  the theorem is     h . either

Re: [Haskell-cafe] Clean proof -- correction

2010-05-23 Thread Derek Elkins
On Sun, May 23, 2010 at 11:38 AM, Daniel Fischer daniel.is.fisc...@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