[Haskell-cafe] Wrong Answer Computing Graph Dominators

Kim-Ee Yeoh a.biurvOir4 at asuhan.com
Sat Apr 19 14:11:31 EDT 2008

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.

More information about the Haskell-Cafe mailing list