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