[Haskell-cafe] Clean proof -- correction

Daniel Fischer daniel.is.fischer at web.de
Sun May 23 12:38:55 EDT 2010


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)


More information about the Haskell-Cafe mailing list