Dan Weston westondan at imageworks.com
Fri Apr 18 15:24:59 EDT 2008

```Matthew Brecknell wrote:
> Dan Weston wrote:
>> Here, "any path" means all paths, a logical conjunction:
>>
>> and [True, True] = True
>> and [True      ] = True
>> and [          ] = True
>
> Kim-Ee Yeoh wrote:
>> Hate to nitpick, but what appears to be some kind of a
>> limit in the opposite direction is a curious way of arguing
>> that: and [] = True.
>>
>> Surely one can also write
>>
>> and [False, False] = False
>> and [False      ] = False
>> and [          ] = False ???
>
> No. I think what Dan meant was that for all non-null
> xs :: [Bool], it is clearly true that:
>
> and (True:xs) == and xs  -- (1)
>
> It therefore makes sense to define (1) to hold also
> for empty lists, and since it is also true that:
>
> and (True:[]) == True
>
> We obtain:
>
> and [] == True
>
> Since we can't make any similar claim about the
> conjuctions of lists beginning with False, there
> is no reasonable argument to the contrary.

Also, (and I know none of this is original, but it's worth repeating...)

It is not just the definition of "and" at stake here. Logical
propositions that extend painlessly to [] if (and [] == True) become
inconsistent for [] if (and [] == False) and would have to be checked in
program calculation.

For instance, in propositional logic, you can prove (using Composition,
Distribution[2], Material Implication) that for nonnull ys =
[y0,y1,..,yn], implying everthing implies each thing:

x -> (y0 && y1 && ... yn)
<-->
(x -> y0) && (x -> y1) && ... && (x -> yn)

Writing this in Haskell and using the fact that x -> y means (not x ||
y), this says that

not x || and ys == and (map (not x ||) ys)

or in pointfree notation:

f . and == and . map f
where f = (not x ||)

This should look familiar to origamists everywhere. "and" can be defined
in terms of foldr iff (and [] == True) [Try it!].

Why is this important?

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:

LHS:  not x || (and []) == not x || False == not x
RHS:  and (map (not x ||) []) == and [] == False
Since not x == False, then x == True
Therefore, True |- x ==> -| x (everything is derivable)

so we would have to exclude the null case for this law (and many
others). Uck! Better stick with (and [] == True)

Naturally, similar reasoning justifies (or [] == False).
```