ABSTRACT
Before proceeding with a definition of a type, we need to understand a simple construction called a set comprehension. Suppose that we wanted to write down the set of all integers between 20 and 30 inclusive. One way of doing this would be the direct way of listing the elements: https://www.w3.org/1998/Math/MathML"> { 20 , 21 , 22 , 23 , 24 , 25 , 26 , 27 , 28 , 29 , 30 } https://s3-euw1-ap-pe-df-pch-content-public-p.s3.eu-west-1.amazonaws.com/9780203211991/94c3b92a-0a16-4a4e-9014-02b93290d004/content/math_421_B.tif" xmlns:xlink="https://www.w3.org/1999/xlink"/> but this could become impractical as the range of numbers increased. A set comprehension allows the same information to be declared without an explicit listing of the elements: https://www.w3.org/1998/Math/MathML"> { x | 20 ≤ x ∧ x ≤ 30 } https://s3-euw1-ap-pe-df-pch-content-public-p.s3.eu-west-1.amazonaws.com/9780203211991/94c3b92a-0a16-4a4e-9014-02b93290d004/content/math_422_B.tif" xmlns:xlink="https://www.w3.org/1999/xlink"/> The vertical bar here might be read as “such that” and this comprehension represents the set of elements x such that x is greater than or equal to 20 but less than or equal to 30. Comprehensions are very powerful and easily implemented in languages such as Miranda that have a list comprehension facility. Set comprehensions of the general form {x | P(x)} define the elements x of a set in terms of some qualifying predicate P such as the greater-than or smaller-than predicates. Thus, the set of odd numbers may be written in this notation as {n | Odd{n)} whereas an explicit description of the infinitely many odd numbers is impossible. An object c is a member of a set defined through a comprehension if and only if it has the property required for set membership: https://www.w3.org/1998/Math/MathML"> c ∈ { x | P ( x ) } ↔ P ( c ) https://s3-euw1-ap-pe-df-pch-content-public-p.s3.eu-west-1.amazonaws.com/9780203211991/94c3b92a-0a16-4a4e-9014-02b93290d004/content/math_423_B.tif" xmlns:xlink="https://www.w3.org/1999/xlink"/> If we define the set of all woodpeckers through the comprehension {x | Woodpecker(x)} then an individual bird called woody is a member of the set if and only if he has the property of being a woodpecker: https://www.w3.org/1998/Math/MathML"> w o o d y ∈ { x | w o o d p e c k e r ( x ) } ↔ w o o d p e c k e r ( w o o d y ) https://s3-euw1-ap-pe-df-pch-content-public-p.s3.eu-west-1.amazonaws.com/9780203211991/94c3b92a-0a16-4a4e-9014-02b93290d004/content/math_424_B.tif" xmlns:xlink="https://www.w3.org/1999/xlink"/> Woodpeckers are divided into classes such as lesser spotted and greater spotted, so the woodpecker set has a number of recognisable subsets, each of which might be described by a comprehension similar to that above. If bill is a lesser spotted woodpecker, we may write https://www.w3.org/1998/Math/MathML"> b i l l ∈ { x | L e s s e r − s p o t t e d ( x ) } https://s3-euw1-ap-pe-df-pch-content-public-p.s3.eu-west-1.amazonaws.com/9780203211991/94c3b92a-0a16-4a4e-9014-02b93290d004/content/math_425_B.tif" xmlns:xlink="https://www.w3.org/1999/xlink"/> and is a member of the set because he has all the properties of a lesser spotted woodpecker. If helmut and John are both members of the set of greater spotted woodpeckers, we could write membership relations similar to those above for each one. Given that both of these birds are members of the greater spotted set, it seems reasonable to consider a set containing the two of them as a member of the set of all greater spotted woodpeckers: https://www.w3.org/1998/Math/MathML"> { h e l m u t , j h o n } ∈ { x | G r w a t e r − s p o t t e d ( x ) } https://s3-euw1-ap-pe-df-pch-content-public-p.s3.eu-west-1.amazonaws.com/9780203211991/94c3b92a-0a16-4a4e-9014-02b93290d004/content/math_426_B.tif" xmlns:xlink="https://www.w3.org/1999/xlink"/> A certain set of woodpeckers might then be written in the form {woody, bill, {helmut, john}}, with a subset indicating a common species or type of bird.
