Sorts

Sort-sums

sort-sum ::= sort-summand { sort-summand }* sort-summand ::= | constructor [ slack-sort ] constructor ::= name

Sample sort-sum:

| Point XYpos | Line XYpos * XYpos

Restriction. The constructors of a sort-sum must all be different names.

The ordering of the sort-summands has no significance: | Zero | Succ Peano denotes the same "sum sort" as | Succ Peano | Zero.

A sort-sum denotes a sum sort, which is a sort that is inhabited by "tagged values". A tagged value is a pair (C, v), in which C is a constructor and v is a sorted value.

A sort-sum introduces a number of embedders, one for each sort-summand. In the discussion, we omit the optional embed keyword of the embedders. The embedders are similar to ops, and are explained as if they were ops, but note the Restriction specified under Structors.

For a sort-sum SS with sort-summand C S, in which C is a constructor and S a sort, the corresponding pseudo-op introduced is sorted as follows:

op C : S -> SS

It maps a value v of sort S to the tagged value (C, v). If the sort-summand is a single parameter-less constructor (the slack-sort is missing), the pseudo-op introduced is sorted as follows:

op C : SS

It denotes the tagged value (C, ()), in which () is the inhabitant of the unit sort (see under Sort-records).

The sum sort denoted by the sort-sum then consists of the union of the ranges (for parameter-less constructors the values) of the pseudo-ops for all constructors.

The embedders are individually, jointly and severally injective, and jointly surjective.

This means, first, that for any pair of constructors C1 and C2 of any sort-sum, and for any pair of values v1 and v2 of the appropriate sort (to be omitted for parameter-less constructors), the value of C1 v1 is only equal to C2 v2 when C1 and C2 are the same constructor of the same sum sort, and v1 and v2 (which then are either both absent, or else must have the same sort) are both absent or are the same value. In other words, whenever the constructors are different, or are from different sort-sums, or the values are different, the results are different. (The fact that synonymous constructors of different sorts yield different values already follows from the fact that values in the models are sorted.)

Secondly, for any value u of any sum sort, there is a constructor C of that sum sort and a value v of the appropriate sort (to be omitted for parameter-less constructors), such that the value of C v is u. In other words, all values of a sum sort can be constructed with an embedder.

For example, consider

sort Peano = | Zero | Succ Peano sort Unique = | Zero

This means that there is a value Zero of sort Peano, and further a function Succ that maps values of sort Peano to sort Peano. Then Zero and Succ n are guaranteed to be different, and each value of sort Peano is either Zero : Peano, or expressible in the form Succ (n : Peano) for a suitable expression n. The expressions Zero : Peano and Zero : Unique denote different, entirely unrelated, values. (Note that Unique is not a subsort of Peano. Subsorts of a sort can only be made with a sort-restriction, for instance as in (Peano | embed? Zero).) For recursively defined sort-sums, see also the discussion under Sort-definitions.

Note. Although the sum sorts | Mono and | Mono () have exactly the same set of inhabitants when considered as unsorted values, these two sorts are different, and the pseudo-ops they introduce have different sorts, only the second of which is a function sort:

Mono : | Mono Mono : () -> | Mono ()

Sort-arrows

sort-arrow ::= arrow-source -> sort arrow-source ::= sort-sum | slack-sort

Sample sort-arrow:

(a -> b) * b -> List a -> List b

In this example, the arrow-source is (a -> b) * b, and the (target) sort List a -> List b.

The function sort S -> T is inhabited by precisely all partial or total functions from S to T. That is, function f has sort S -> T if, and only if, for each value x of sort S such that the value of f x is defined, that value has sort T. Functions can be constructed with lambda-forms, and be used in applications.

In considering whether two functions (of the same sort) are equal, only the meaning on the domain sort is relevant. Whether a function is undefined outside its domain sort, or might return some value of some sort, is immaterial to the semantics of Metaslang. (For a sort-correct spec, the difference is unobservable.)

Sort-products

sort-product ::= tight-sort * tight-sort { * tight-sort }*

Sample sort-product:

(a -> b) * b * List a

Note that a sort-product contains at least two constituent tight-sorts.

A sort-product denotes a product sort that has at least two "component sorts", represented by its tight-sorts. The ordering of the component sorts is significant: unless S and T are the same sort, the product sort S * T is different from the sort T * S. Further, the three sorts (S * T) * U, S * (T * U) and S * T * U are all different; the first two have two component sorts, while the last one has three. The inhabitants of the product sort S₁ * S₂ * ... * S_n are precisely all n-tuples (v₁, v₂, ... , v_n), where each v_i has sort S_i, for i = 1, 2, ... , n. Values of a product sort can be constructed with tuple-displays, and component values can be extracted with tuple-patterns as well as with projectors.

Sort-instantiations

sort-instantiation ::= sort-name actual-sort-parameters actual-sort-parameters ::= closed-sort | ( proper-sort-list ) proper-sort-list ::= sort , sort { , sort }*

Sample sort-instantiation:

Map (Nat, Boolean)

Restriction. The sort-name must have been declared or defined as a parameterized sort (see Sort-declarations), and the number of sorts in the actual-sort-parameters must match the number of local-sort-variables in the formal-sort-parameters of the sort-declaration and/or sort-definition.

The sort represented by a sort-instantiation is the sort assigned for the combination of sorts of the actual-sort-parameters in the indexed family of sorts for the sort-name of the sort-instantiation.

Sort-names

sort-name ::= qualifiable-name

Sample sort-names:

Key Calendar.Date

Restriction. At the spec level, a sort-name may only be used if there is a sort-declaration and/or sort-definition for it in the current spec or in some spec that is imported (directly or indirectly) in the current spec. If there is a unique qualified-name for a given unqualified ending, the qualification may be omitted for a sort-name used as a sort.

The sort of a sort-name is the sort assigned to it in the model. (In this case, the context can not have superseded the original assignment.)

Sort-records

sort-record ::= { [ field-sorter-list ] } | ( ) field-sorter-list ::= field-sorter { , field-sorter }* field-sorter ::= field-name : sort field-name ::= name

Sample sort-record:

{center : XYpos, radius : Length}

Restriction. The field-names of a sort-record must all be different.

Note that a sort-record contains either no constituent field-sorters, or else at least two.

A sort-record is like a sort-product, except that the components, called "fields", are identified by name instead of by position. The ordering of the field-sorters has no significance: {center : XYpos, radius : Length} denotes the same record sort as {radius : Length, center : XYpos}. Therefore we assume in the following, without loss of generality, that the fields are ordered lexicographically according to their field-names (as in a dictionary: a comes before ab comes before b) using some fixed collating order for all marks that may comprise a name. Then each field of a record sort with n fields has a position in the range 1 to n. The inhabitants of the record sort {F₁ : S₁, F₂ : S₂, ... , F_n : S_n} are precisely all n-tuples (v₁, v₂, ... , v_n), where each v_i has sort S_i, for i = 1, 2, ... , n. The field-names of that record sort are the field-names F₁, ... , F_n, and, given the lexicographic ordering, field-name F_i selects positioni, for i = 1, 2, ... , n. Values of a record sort can be constructed with record-displays, and field values can be extracted with record-patterns and (as for product sorts) with projectors.

For the sort-record {}, which may be equivalently written as (), the record sort it denotes has zero components, and therefore no field-names. This zero-component sort has precisely one inhabitant, and is called the unit sort. The unit sort may equally well be considered a product sort, and is the only sort that is both a product and a record sort.

Sort-restrictions

sort-restriction ::= ( slack-sort | expression )

Sample sort-restriction:

(Nat | even)

Restriction. In a sort-restriction (S | P), the expression P must be a predicate on the sort S, that is, P must be a function of sort S -> Boolean.

Note that the parentheses in (S | P) are mandatory.

The inhabitants of sort-restriction (S | P) are precisely the inhabitants of sort S that satisfy the predicate P, that is, they are those values v for which the value of P v is true.

If P1 and P2 are the same function, then (S | P1) and (S | P2) are equivalent, that is, they denote the same sort.

The sort (S | P) is called a subsort of supersort S. Values can be shuttled between a subsort and its supersort and vice versa with relaxators and restrictors; see also Relax-patterns.

Metaslang does not require the explicit use of a relaxator to relax an expression from a subsort to its supersort if the context requires the latter. Implicit relaxation will take place when needed. For example, in the expression ~1 the nat-literal 1 of sort Nat is implicitly relaxed to sort Integer to accommodate the unary negation operator ~, which has sort Integer -> Integer.

Likewise, Metaslang does not require the explicit use of a restrictor to restrict an expression from a sort to a subsort if the context requires the latter. Implicit restriction will take place when needed. For example, in the expression 7 div 2 the nat-literal 2 of sort Nat is implicitly restricted to sort PosNat, a subsort of Nat, to accommodate the division operator div, whose second argument has sort PosNat. But note that implicit restriction engenders the same proof obligation as results when using an explicit restrictor.

Sort-comprehensions

sort-comprehension ::= { annotated-pattern | expression }

Sample sort-comprehension:

{n : Nat | even n}

Restriction. In a sort-comprehension {P : S | E}, the expression E must have sort Boolean.

Sort-comprehensions provide an alternative notation for sort-restrictions that is akin to the common mathematical notation for set comprehensions. The meaning of sort-comprehension {P : S | E} is the same as that of the sort-restriction (S | fn P -> E). So the meaning of the example sort-comprehension above is (Nat | fn n -> even n).

Sort-quotients

sort-quotient ::= closed-sort / closed-expression

Sample sort-quotient:

Nat / (fn (m, n) -> m rem 3 = n rem 3)

Restriction. In a sort-quotient S / Q, the expression Q must be a (binary) predicate on the sort S * S that is an equivalence relation, as explained below.

Equivalence relation. Call two values x and y of sort S "Q-related" if (x, y) satisfies Q. Then Q is an equivalence relation if, for all values x, y and z of sort S, x is Q-related to itself, y is Q-related to x whenever x is Q-related to y, and x is Q-related to z whenever x is Q-related to y and y is Q-related to z. The equivalence relation Q then partitions the inhabitants of S into equivalence classes, being the maximal subsets of S containing mutually Q-related members. These equivalence classes will be called "Q-equivalence classes".

The inhabitants of the quotient sort S / Q are precisely the Q-equivalence classes into which the inhabitants of S are partitioned by Q. For the example above, there are three equivalence classes of natural numbers leaving the same remainder on division by 3: the sets {0, 3, 6, ...}, {1, 4, 7, ...} and {2, 5, 8, ...}, and so the quotient sort has three inhabitants.