[Haskell-cafe] Wrong Answer Computing Graph Dominators

[Kim-Ee Yeoh]

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.