Why “and []” is True and “or []” is False

问题:

Why "and" on an empty list returns true, does it imply that an empty list holds True? Sorry but I cannot read and comprehend this correctly, so please correct me. Thanks.

Prelude> and []
True
Prelude> or []
False

回答1:

In mathematics, it's often useful to talk about a binary operation, such as &&, ||, +, *, etc as having an identity. The identity is a value e such that the following property holds for some generic binary operation <>

e <> x = x
x <> e = x

For the operators I listed above, they are commutative, meaning that x <> y = y <> x for all x and y, so we only have to check one of the above properties. For and, the binary operator in question is &&, and for or the binary operator is ||. If we make a Cayley table for these operations, it would look like

&&    | False | True
------+-------+------
False | False | False
True  | False | True


||    | False | True
------+-------+------
False | False | True
True  | True  | True

So as you can see, for && if you have True && False and True && True, the answer is always the second argument to &&. For ||, if you have False || False and False || True, the answer is always the second argument, so the first argument of each must be the identity element under those operators. Put simply:

True && x = x
x && True = x

False || x = x
x || False = x

Thus, the preferred answer when there are no elements to perform the operator on is the identity element for each operation.

---

It might help to also think about the identity elements for + and *, which are 0 and 1 respectively:

x + 0 = x = 0 + x
x * 1 = x = 1 * x

You can also extend this to operations like list concatenation (++ with []), function composition for functions of type a -> a ((.) with id), along with many others. Since this is starting to look like a pattern, you might ask if this is already a thing in Haskell, and indeed it is. The module Data.Monoid defines the Monoid typeclass that abstracts this pattern, and it's minimal definition is

class Monoid a where
    mempty :: a                   -- The identity
    mappend :: a -> a -> a        -- The binary operator

And it even aliases mappend as <> for ease of use (it was no accident that I choose it above for a generic binary operator). I encourage you to look at that module and play around with its definitions. The source code is quite easy to read and is enlightening.

回答2:

and and or are just folds, and a fold called on an empty list will produce its starting argument, which is True or False, respectively.

They are implemented using a fold only if Prelude is loaded, otherwise they are realised using explicit recursion, which in itself still is a fold despite not actually making use of foldr or foldl. They still behave the same as we can see by examining the source:

and [] = True
and (x:xs) = x && and xs
or [] = False
or (x:xs) = x || or xs

---

Here is a link to the implementations.

---

To clear the confusion in the comments: A fold is a function which takes a binary function and a starting value (often called accumulator) and traverses a list until it is empty. When called on an empty list, the fold will return the accumulator as is where it does not matter if the list has already been traversed or not. This is a sample implementation of foldr:

foldr _ acc [] = acc
foldr f acc (x:xs) = f x (foldr f acc xs)

and is simply

and = foldr (&&) True

which makes and [] evaluate to True.

回答3:

Excellent answers, but I think it's worth providing a more intuitive treatment. Instead of and :: [Bool] -> Bool, however, let's look at all :: (a -> Bool) -> [Bool] -> Bool. You can think of all this way. Picture the predicate (the a -> Bool argument) as a hypothesis about list elements. Then all returns False if and only if the list contains at least one counterexample to the hypothesis. If the list is empty there are no counterexamples, so it's trivially confirmed.

To bring it back to and, note that and and all are interdefinable. If you have and, you can define all this way:

all :: (a -> Bool) -> [a] -> Bool
all pred = and . map pred

And vice-versa, if you already had all, you could define and from it:

and :: [Bool] -> Bool
and = all id

回答4:

In addition to @bheklilr answer, let's recall that a Monoid is a tuple (M,e,<>), where M is a object (you can think of it as a type), e is a point of the object M (e : M - element of type) and <> is a binary operation, which is associative and has e as identity:

<> : M -> M -> M
e <> x = x
x <> e = x
(x <> y) <> z = x <> (y <> z)

There are monoid homomorphisms between some monoids. There is one free monoid - the monoid from which there is a homomorphism into any other. Such free monoid is a list: ([a], [], ++) can be mapped into any other monoid. For example:

([Int], [], ++) => (Int, 0, +)
([Int], [], ++) => (Int, 1, *)
([Bool], [], ++) => (Bool, True, &&)
([Bool], [], ++) => (Bool, False, ||)

Then sum, product, and, or are the respective monoid homomorphisms, mapping the elements of the types [Int] and [Bool]. By the definition of the monoid homomorphism, the mapping h of the monoids is performed in such a way that any list x++y is mapped into the point h(x ++ y) == (h x) <> (h y) - for example, and (x++[]) == (and x) && (and []). It becomes clear from the latter example, that since x++[] == x, so (and x) && (and []) == and x, therefore, and [] maps into the identity element of (Bool, True, &&).

回答5:

One way to think about True and False is as elements of the lattice ordered by False < True. && and || can be viewed as the binary "meet" (greatest lower bound) and "join" (least upper bound) operations for this lattice. Similarly, and and or are general finite meet and finite join operations. What is and []? It's the greatest lower bound of []. But True is (vacuously) less than or equal to every element of [], so it's a lower bound of [], and (of course) it's greater than any other lower bound (the other being False), so and [] = True. The algebraic view (thinking about monoids and such) turns out to be entirely equivalent to the order-theoretic view, but I think the order-theoretic one offers more visual intuition.

回答6:

The logic of and is to find the first entry in the list which is False. If the entry is not found, the result is True. For example:

and $ map even [2..]

will not iterate through the whole infinite list, but will stop at 3 and return False. There is no False element in the empty list, so we default to True.

For or it's similarly: it tries to find the first True and then stops, otherwise it's False.

回答7:

and means: "Is everything there True?". When it's empty, everything's that is in there (which isn't much) is true, so that's a yes (True).

or means: "Is anything there True?". When there's nothing there, there's nothing true there. (False)