The Avail Programming Language

set ≝ {any|}

type lattice focused on sets

A set is an immutable, finite, unordered collection of distinct, homogeneous values, called members or elements. The number of elements is the cardinality of the set. Breaking this down:

  • Immutable means that the composition of a set is not subject to change. No operations are, or can be, defined to modify a set in any way; only operations that derive new sets from existing sets are expressible.
  • Finite means that the cardinality of a set is never the value . To store a set in memory requires space proportional to its cardinality, and memory is clearly always finite. Additional limits to the practical cardinality of sets may be imposed by the implementation.
  • Unordered means that the members of a set do not occur in any particular order. Any two sets with the same membership are therefore equal.
  • Distinct means that a member occurs only once in the membership of a set. Thus a value is either a member of a set or it is not.
  • Homogeneous means that the members of a set universally conform to a single most general type.

A literal set is expressed as a left curly bracket { (U+007B), then a list of members separated by commas , (U+002C), and finally a right curly bracket } (U+007D). Examples of sets include {7}, {"Gnaeus Pompeius Magnus", "Gaius Julius Caesar", "Marcus Licinius Crassus"}, and {"Leaping", ¢a, 10, "Lords"}. The members are ordered atypically to emphasize the unordered nature of sets. The empty set is written as (U+2205).

The elements of a set need not be known statically. Sets are constructed with the macro "{«_‡,»}"; there is no special built-in syntax for constructing sets. When the compiler can infer an instance type for each argument expression of a particular send of this message, then the semantic restriction is able to strengthen the result to an instance type, thereby according it the same force as a literal understood primitively by the compiler.

The set type specifies two parameters for completion:

  • The member type (or element type) specifies a type that includes every member. For example, a set type whose member type is double has as instances the sets {1.0}, {2.0, 4.0, 8.0}, and {π, Euler's number}. The method "_'s⁇element|member type" answers the member type of a set type.
  • The cardinality restriction is an integral type that specifies the range of sizes that describe instances. If the cardinality restriction is [1..3], then only a set whose cardinality is 1, 2, or 3 is an instance. The method "`|`|_`|`|", read as sizes of, answers the cardinality restriction of a set type. The floor operation, ⎣_⎦, answers the lower bound of a set type's cardinality restriction. The ceiling operation, ⎡_⎤, answers the upper bound of a set type's cardinality restriction.

The primitive set type constructor is "{_|_}". It accepts the member type and cardinality restriction, respectively. This method supports the most general type construction scenario, that of two statically unknown type completion arguments. Most type construction is done by the compiler during execution of type annotations, however, so typically most or all of the set type completion arguments will be known at compile-time. For these more common situations, the system library provides the following convenience methods:

  • The method "{_|_.._}" accepts the member type, the lower bound of the cardinality restriction, and the upper bound of the cardinality restriction, respectively. To determine the cardinality restriction, take the specified lower and upper bounds — lower and upper, respectively, in the following expression — and compute the type [lower..upper+1). Canonization of integral ranges causes the specified upper bound to be considered inclusive if it is finite and exclusive if it is infinite.
    /* Here's a set type with an inclusive upper bound on its cardinality * restriction. */ setType ::= {integer|2..4}; Assert: setType's member type = integer; Assert: ||setType|| = [2..4]; /* And here's one with an exclusive upper bound. */ Assert: ||{string|13..∞}|| = [13..∞); /* Here are some example instances of "setType". */ Assert: {2, 9001} ∈ setType; Assert: {-1, -4, -7} ∈ setType; Assert: {3, 5, 8, 13} ∈ setType; /* And here is an example non-instance (because it's too small). */ Assert: {0} ∉ setType;
  • The method "{_|_..}" accepts the member type and the lower bound of the cardinality restriction, respectively. To determine the cardinality restriction, take the specified lower bound, lower, and compute the type [lower..∞).
    setType ::= {string|1..}; Assert: setType's element type = string; Assert: ||setType|| = [1..∞); /* Here are some example instances of "setType". */ Assert: {"loneliness"} ∈ setType; Assert: {"Sargon", "Hammurabi", "Ashurbanipal", "Gilgamesh"} ∈ setType;
  • The method "{_|.._}" accepts the member type and the upper bound of the cardinality restriction, respectively. To determine the cardinality restriction, take the specified upper bound, upper, and compute the type [0..upper+1).
    setType ::= {tuple|..2}; Assert: setType's member type = tuple; Assert: ||setType|| = [0..2]; /* Here are some example instances of "setType". */ Assert: ∅ ∈ setType; Assert: {<1, "fish", 2, "fish">} ∈ setType; Assert: {<>, <"megaphone">} ∈ setType;
  • The method "{_|_}" is overridden to accept, respectively, the member type and a whole number that specifies the exact size of instances. To determine the cardinality restriction, take the argument, exact, and compute the type [exact..exact].
    setType ::= {[2..4]|3}; Assert: setType's element type = [2..4]; Assert: ||setType|| = [3..3]; /* Here is the sole instance of "setType". */ Assert: {2, 3, 4} ∈ setType; /* And here is the proof that it's the only instance. */ Assert: {2, 3, 4} = {2, 4, 3} = {3, 2, 4} = {3, 4, 2} = {4, 2, 3} = {4, 3, 2};
  • The method "{_|}" accepts the member type. The cardinality restriction is [0..∞).
    setType ::= {character|}; Assert: setType's member type = character; Assert: ||setType|| = [0..∞); /* Here are some example instances of "setType". */ Assert: {¢a, ¢b, ¢c} ∈ setType; Assert: {¢∪, ¢∩} ∈ setType; Assert: {¢1, ¢2, ¢3, ¢4, ¢5} ∈ setType; Assert: {¢{, ¢,, ¢¢, ¢}} ∈ setType;

A set type is covariant by member type and cardinality restriction.

string | Return to Type System | map