Dan Weston wrote:
f . and == and . map f where f = (not x ||)
If and is defined with foldr, then the above can be proven for all well-typed f, and for f = (not x ||) in particular, even if ys is null. The law is painlessly extended to cover the null case automatically (and is therefore consistent):
LHS: not x || (and []) == not x || True == True RHS: and (map (not x ||) []) == and [] == True Therefore True |- True, an instance of x |- x
If (and [] == False), then the law becomes inconsistent:
-- snipped -- Yes, the natural way of defining and [] is, well, natural in more than one sense of the word. I initially had a hard time grasping what you meant with the 3 equations that started this discussion. I was sure you meant something other than what I thought, but I couldn't work it out. I'm glad Matt Brecknell came to the rescue. Before I would've merely relied on a monoidal identity argument like the one Chris had presented. Appealing to uniformity (a la parametric polymorphism) definitely looks sexier. All the cool kids seem to be doing it. -- View this message in context: http://www.nabble.com/Wrong-Answer-Computing-Graph-Dominators-tp16714477p167... Sent from the Haskell - Haskell-Cafe mailing list archive at Nabble.com.