Type-descriptors

Type-sums

type-sum ::= type-summand { type-summand }* type-summand ::= | constructor [ slack-type-descriptor ] constructor ::= simple-name

Sample type-sum:

| Point XYpos | Line XYpos * XYpos

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

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

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

A type-sum introduces a number of embedders, one for each type-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 type-sum T with type-summand C S, in which C is a constructor and S a type-descriptor, the corresponding pseudo-op introduced is typed as follows:

op C : S -> T

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

op C : T

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

The sum type denoted by the type-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 type-sum, and for any pair of values v1 and v2 of the appropriate type (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 type, and v1 and v2 (which then are either both absent, or else must have the same type) are both absent or are the same value. In other words, whenever the constructors are different, or are from different type-sums, or the values are different, the results are different. (The fact that synonymous constructors of different types yield different values already follows from the fact that values in the models are typed.)

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

For example, consider

type Peano = | Zero | Succ Peano type Unique = | Zero

This means that there is a value Zero of type Peano, and further a function Succ that maps values of type Peano to type Peano. Then Zero and Succ n are guaranteed to be different, and each value of type 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 subtype of Peano. Subtypes of a type can only be made with a type-restriction, for instance as in (Peano | embed? Zero).) For recursively defined type-sums, see also the discussion under Type-definitions.

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

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

Type-arrows

type-arrow ::= arrow-source -> type-descriptor arrow-source ::= type-sum | slack-type-descriptor

Sample type-arrow:

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

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

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

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

Type-products

type-product ::= tight-type-descriptor * tight-type-descriptor { * tight-type-descriptor }*

Sample type-product:

(a -> b) * b * List a

Note that a type-product contains at least two constituent tight-type-descriptors.

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

Type-instantiations

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

Sample type-instantiation:

Map (Nat, Boolean)

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

The type-descriptor represented by a type-instantiation is the type assigned for the combination of types of the actual-type-parameters in the indexed family of types for the type-name of the type-instantiation.

Type-names

type-name ::= name

Sample type-names:

Key Calendar.Date

Restriction. At the spec level, a type-name may only be used if there is a type-declaration and/or type-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 type-name used as a type-descriptor.

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

Type-records

type-record ::= { [ field-typer-list ] } | ( ) field-typer-list ::= field-typer { , field-typer }* field-typer ::= field-name : type-descriptor field-name ::= simple-name

Sample type-record:

{center : XYpos, radius : Length}

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

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

A type-record is like a type-product, except that the components, called "fields", are identified by name instead of by position. The ordering of the field-typers has no significance: {center : XYpos, radius : Length} denotes the same record type 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 type with n fields has a position in the range 1 to n. The inhabitants of the record type {F₁ : T₁, F₂ : T₂, ... , F_n : T_n} are precisely all n-tuples (v₁, v₂, ... , v_n), where each v_i has type T_i, for i = 1, 2, ... , n. The field-names of that record type 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 type can be constructed with record-displays, and field values can be extracted with record-patterns and (as for product types) with projectors.

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

Type-restrictions

type-restriction ::= ( slack-type-descriptor | expression )

Sample type-restriction:

(Nat | even)

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

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

The inhabitants of type (T | P) are precisely the inhabitants of type T 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 (T | P1) and (T | P2) are equivalent, that is, they denote the same type. Furthermore, (T | fn _ -> true) is equivalent to T.

The type (T | P) is called a subtype of supertype T. Values can be shuttled between a subtype and its supertype and vice versa with relaxators and restrict-expressions; see also Relax-patterns.

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

Likewise, Metaslang does not require the explicit use of a restrict-expression to restrict an expression from a type to a subtype 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 type Nat is implicitly restricted to type PosNat, a subtype of Nat, to accommodate the division operator div, whose second argument has type PosNat. But note that implicit restriction engenders the same proof obligation as results when using an explicit restrict-expression.

Type-comprehensions

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

Sample type-comprehension:

{n : Nat | even n}

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

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

Type-quotients

type-quotient ::= closed-type-descriptor / closed-expression

Sample type-quotient:

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

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

Equivalence relation. Call two values x and y of type T "Q-related" if (x, y) satisfies Q. Then Q is an equivalence relation if, for all values x, y and z of type T, 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 T into equivalence classes, being the maximal subsets of T containing mutually Q-related members. These equivalence classes will be called "Q-equivalence classes".

The inhabitants of the quotient type T / Q are precisely the Q-equivalence classes into which the inhabitants of T 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 type has three inhabitants.