Why "and []" is true, and "or []" is false

Why does the "and" in the empty list return true, does this mean that the empty list contains True? Sorry, but I canโ€™t read and understand it correctly, so please correct me. Thanks.

Prelude> and [] True Prelude> or [] False 
+7
haskell monoids
source share
6 answers

In mathematics, it is often useful to talk about a binary operation such as && , || , + , * , etc. as having a personality. Identity is the value of e such that for some common binary operation <>

the following property is satisfied:
 e <> x = x x <> e = x 

For the above operators, they are commutative, which means x <> y = y <> x for all x and y , so we only need to check one of the above properties. For and , the binary operator && under consideration, and for or binary operator || . If we make a Cayley table for these operations, it will 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 False || False and False || True False || True , the answer is always the second argument, so the first argument of each of them should be an identification element under these operators. Simply put:

 True && x = x x && True = x False || x = x x || False = x 

Thus, the preferred answer, when there are no elements to execute the on statement, is an identification element for each operation.


It may also help to think of identity elements for + and * , which are 0 and 1 respectively:

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

You can also expand it to operations such as combining lists ( ++ with [] ), the composition of functions for functions like a -> a ( (.) With id ), as well as many others. Since this is starting to look like a template, you may ask if it is already in Haskell, and it really is. The Data.Monoid module defines the Monoid class, which abstracts this template, and its minimum definition.

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

And these are even mappend as <> for ease of use (it is not by chance that I chose it above for the general binary operator). I recommend that you look at this module and play around with its definitions. Source code is pretty easy to read and educate.

+35
source share

and and or are just bends, and dropping caused by an empty list will result in its initial argument, which is True or False respectively.

They are implemented using a fold only if Prelude loaded, otherwise they are implemented using explicit recursion, which itself is still a fold, even though foldr or foldl not actually used. They still behave in the same way as we can see when exploring the source:

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

Here is a link to implementations.


To eliminate the confusion in the comments: a fold is a function that takes a binary function and an initial value (often called a battery) and moves the list until it becomes empty. When called in an empty list, resetting returns the battery, since it does not matter if the list has already been passed or not. This is an example implementation of foldr :

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

and just

 and = foldr (&&) True 

which makes and [] evaluate to True .

+12
source share

In addition to @bheklilrโ€™s answer, we recall that the monoid is a tuple (M,e,<>) , where M is an object (you can think of it as a type), e is the point of an M object ( e : M is a type element) and <> is a binary operation, associative and having e as an identifier:

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

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

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

Then sum , product , and , or are the corresponding monoid homomorphisms that display elements of the types [Int] and [Bool] . By the definition of monoid homomorphism, the mapping of h monoids is performed in such a way that any list x++y maps to the point h(x ++ y) == (hx) <> (hy) - for example, and (x++[]) == (and x) && (and []) . From the last example, it becomes clear that since x++[] == x , therefore (and x) && (and []) == and x , therefore, and [] maps the element (Bool, True, &&) to unity.

+5
source share

Great answers, but I think it's worth offering a more intuitive treatment. Instead of and :: [Bool] -> Bool , let's look at all :: (a -> Bool) -> [Bool] -> Bool . You can think of all that way. Think of the predicate (argument a -> Bool ) as a hypothesis about list items. 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; therefore, it is trivially confirmed.

To return it to and , note that and and all are interdependent. If you have and , you can define all as follows:

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

Conversely, if you already have all , you can determine and from it:

 and :: [Bool] -> Bool and = all id 
+5
source share

One way to think about True and False is with lattice elements sorted by False < True . && and || can be considered as binary operations โ€œmeetโ€ (the largest lower bound) and โ€œjoinโ€ (the smallest upper bound) for this lattice. Similarly, and and or are general finite operations with a finite join and a finite join. What is and [] ? This is the largest lower bound [] . But True (empty) is less than or equal to each element of [] , so this is the lower bound [] and (of course) is larger than any other lower bound (the other is False ), therefore and [] = True . The algebraic view (thinking about monoids, etc.) turns out to be completely equivalent to the set-theoretic order, but I think that the set-theoretic order offers a more visual intuition.

+3
source share

The logic of and is to search for the first entry in the list, which is False . If the record is not found, the result will be True . For example:

 and $ map even [2..] 

will not go through the entire endless 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 similar: it tries to find the first True , and then stops, otherwise it is False .

+2
source share

All Articles