tuple ≝ <any…|>

A tuple is an immutable, finite, ordered list of indexable, heterogeneous values, called elements, each of which is accessible by a natural number subscript. The number of elements is the size of the tuple. Taking this apart:

• Immutable means that neither the composition nor the ordering of a tuple is subject to change. No operations are, or can be, provided to modify a tuple in any way; only operations that derive new tuples from existing tuples are possible.
• Finite means that the size of a tuple is never the value ∞. To store a tuple in memory requires space proportional to the size of the tuple, and memory is clearly always finite. Additional limits to the practical size of tuples may be imposed by the implementation.
• Ordered means that the elements of a tuple occur in a particular order, and that two orderings are distinguishable so long as the transposed elements are not equal. A tuple comprising the values 1, 2, and 3 is distinct from one comprising the values 3, 2, and 1.
• Indexable means that an element can be accessed using a numeric key that describes its position within the tuple. For a tuple, this key, called the subscript, is a natural number ranging from 1 to the size of the tuple. Given that t is a tuple and i is a natural number, then |t| is the size of t, and t[i] is the i-th element of t. If a tuple t has n elements, that is, |t| = n, then the elements of t are t[1], t[2], …, and t[n]. The methods for sizing and subscripting are "`|_`|" and "_[_]", respectively.
• Heterogeneous means that the elements do not universally conform to a single most general type. Type conformance of elements, when considered relative to a tuple type, is by position within a tuple. More will be said on this below.

A literal tuple is expressed as a less-than sign < (U+003C), then a list of elements separated by commas , (U+002C), and finally a greater-than sign > (U+003E). Examples of tuples include <1>, <"Moe", "Larry", "Shemp", "Curly", "Joe", "Joe">, <[1 + 3], [x : integer | x + 3]>, and <2, "radish", ¢=, <"hey", "nonny", "nonny">>. The empty tuple is written as <>.

The elements of a tuple need not be statically well-known as they are in the above examples. Tuples are built with the macro "<«_‡,»>", and not through special syntax hardwired into the compiler. When the compiler is able to 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 giving it the same force as a literal understood primitively by the compiler.

The tuple type specifies three parameters for completion:

• The leading types associate some of the prefix positions — that is, the left-hand side — of a tuple with types to which the elements at those positions must conform. To demystify this, consider a tuple type whose leading types are number, any, and [10..20]. Every instance of this type is a tuple (t) whose first element (t[1]) is a number, whose second element (t[2]) is any value whatsoever, and whose third element (t[3]) is an integer from 10 to 20. The leading types comprise a tuple of types, <type…|>; more on reading this notation below. The method "_'s⁇leading types" answers the leading types of a tuple type.
• The default type specifies the type of every element residing at a suffix position — that is, a position to the right of the last position governed by a leading type. Assume that a tuple type's leading types are string and function. Further assume that its default type is integer. Then every instance of this type is a tuple (t) such that t[1] is a string, t[2] is a function, and t[3], t[4], …, and t[|t|] are integers. The method "_'s⁇default type" answers the default type of a tuple type.
• The cardinality restriction is an integral type that specifies the range of sizes that describe instances. If the cardinality restriction is [2..4], then only a tuple whose size is 2, 3, or 4 is an instance. The method "`|`|_`|`|", read as sizes of, answers the cardinality restriction of a tuple type. The floor operation, ⎣_⎦, answers the lower bound of a tuple type's cardinality restriction. The ceiling operation, ⎡_⎤, answers the upper bound of a tuple type's cardinality restriction.

When applied to a tuple type instead of a tuple, the method "_[_]" answers the element type at the specified subscript. Given a tuple type U and a subscript i, if i ≤ |U's leading types|, then the answer is U's leading types[i], the i-th leading type; if |U's leading types| < i ≤ ⎡U⎤, then the answer is U's default type; but if i > ⎡U⎤, then the answer is ⊥.

The primitive tuple type constructor is "<_,_`…`|_>". It accepts the leading types, default type, and cardinality restriction, respectively. This method supports the most general type construction case, that of three 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 tuple type completion arguments will be known at compile-time. For these cases, the system library provides the following convenience methods:

• The method "<«_‡,»`…|_.._>" accepts a nonempty lexical tuple of types, the lower bound of the cardinality restriction, and the upper bound of the cardinality restriction, respectively. The first argument comprises both the leading types and the default type; the default type is simply the last type named before the horizontal ellipsis (…). Just to be explicit, if only one type is specified, then the leading types are <> and the type named is the default type. 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 tuple type with an inclusive upper bound on its cardinality * restriction. */ tupleType ::= <integer, float, double…|1..3>; Assert: tupleType's leading types = <integer, float>; Assert: tupleType's default type = double; Assert: ||tupleType|| = [1..3]; /* And here's one with an exclusive upper bound. */ Assert: ||<integer, float, double…|1..∞>|| = [1..∞); /* Here are some example instances of "tupleType". */ Assert: <41> ∈ tupleType; Assert: <55, 7.0→float> ∈ tupleType; Assert: <69, 3.5→float, π> ∈ tupleType; /* And here is an example non-instance (because it's too big). */ Assert: <69, 3.5→float, π, Euler's number> ∉ tupleType;
• The method "<«_‡,»`…|_..>" accepts a nonempty lexical tuple of types and the lower bound of the cardinality restriction, respectively. The first argument comprises both the leading types and the default type. To determine the cardinality restriction, take the specified lower bound, lower, and compute the type [lower..∞).
  tupleType ::= <string…|2..>; Assert: tupleType's leading types = <>; Assert: tupleType's default type = string; Assert: ||tupleType|| = [2..∞); /* Here are some example instances of "tupleType". */ Assert: <"Batman", "Robin"> ∈ tupleType; Assert: <"Candide", "Cunégonde", "Pangloss"> ∈ tupleType; /* And here is an example non-instance (because it's too small). */ Assert: <"lonely"> ∉ tupleType;
• The method "<«_‡,»`…|.._>" accepts a nonempty lexical tuple of types and the upper bound of the cardinality restriction, respectively. The first argument comprises both the leading types and the default type. To determine the cardinality restriction, take the specified upper bound, upper, and compute the type [0..upper+1).
  tupleType ::= <string, string, integer…|..3>; Assert: tupleType's leading types = <string, string>; Assert: tupleType's default type = integer; Assert: ||tupleType|| = [0..3]; /* Here are some example instances of "tupleType". */ Assert: <> ∈ tupleType; Assert: <"picturesque"> ∈ tupleType; Assert: <"Phil", "Harmonic"> ∈ tupleType; Assert: <"A", "K", 47> ∈ tupleType;
• The method "<«_‡,»`…|_>" accepts a nonempty lexical tuple of types and a whole number representing the exact size of instances, respectively. The first argument comprises both the leading types and the default type. To determine the cardinality restriction, take the argument, exact, and compute the type [exact..exact].
  tupleType ::= <1's type, [1..3]…|3>; Assert: tupleType's leading types = <1's type>; Assert: tupleType's default type = [1..3]; Assert: ||tupleType|| = [3..3]; /* Here are all the instances of "tupleType". */ Assert: <1, 1, 1> ∈ tupleType; Assert: <1, 1, 2> ∈ tupleType; Assert: <1, 1, 3> ∈ tupleType; Assert: <1, 2, 1> ∈ tupleType; Assert: <1, 2, 2> ∈ tupleType; Assert: <1, 2, 3> ∈ tupleType; Assert: <1, 3, 1> ∈ tupleType; Assert: <1, 3, 2> ∈ tupleType; Assert: <1, 3, 3> ∈ tupleType;
• The method "<«_‡,»`…|>" accepts a nonempty lexical tuple of types. The argument comprises both the leading types and the default type. The cardinality restriction is [0..∞).
  tupleType ::= <integer, string…|>; Assert: tupleType's leading types = <integer>; Assert: tupleType's default type = string; Assert: ||tupleType|| = [0..∞); /* Here are some example instances of "tupleType". */ Assert: <> ∈ tupleType; Assert: <0> ∈ tupleType; Assert: <1, "fish"> ∈ tupleType; Assert: <2, "fish"> ∈ tupleType; Assert: <7, "I", "don", "'", "t", "like", "spam", "!"> ∈ tupleType;

A tuple type is covariant by positional element type and cardinality restriction. Given two tuple types U and V, U is a subtype of V if and only if ||U|| is a subtype of ||V|| and every element type of U is a subtype of the corresponding element type of V. In symbols, ∀U, V ⊆ tuple, i : 1 ≤ i ≤ min ⎡U⎤, ⎡V⎤: (||U|| ⊆ ||V|| ∧ U[i] ⊆ V[i]) ↔ U ⊆ V.

Here are some examples of tuple type relations: