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-tp16714477p16786100.html Sent from the Haskell - Haskell-Cafe mailing list archive at Nabble.com. _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe