45 Types

Up to now we have used the word ‘type’ informally to refer to the kinds of values introduced by nominal type declarations. We now give the semantic definition of a type and explain how types relate.

A type is a semantic classification of values. Each type has a carrier set: the set of values classified by that type. Predica types are introduced or described in the following ways:

• It is a predefined type.
• It is a structural type.
• It is a nominal type introduced by a nominal type declaration.
• It is a type expression formed from existing types, such as Set<T>, a subtype T where p refinement, a union, or an intersection.
• It is the intersection of two or more comparable types, where comparability ensures a unique least common supertype with defined equality

Any type may have multiple names.

In the semantic model, type equality is equality of carrier sets. Consequently, two types are equal exactly when they have the same carrier set.

A type expression denotes a type, and therefore determines a carrier set drawn from a fixed background universe of sets. Type expressions provide the syntax for referring to types.

Some declarations, such as value and entity, introduce new nominal type identity. Other declarations, such as type aliases, bind a name to a type expression without creating a new carrier set. A subtype T where p type expression denotes a subset of an existing type.

Type test expressions

The expression L isa T tests the relationship of its left operand L to the type denoted by its right operand T. Its result type is Boolean. The left operand may be either a value expression or a type expression.

When L is a value expression, L isa T tests whether the value denoted by L is a member of T. The test is about the value of L, not the syntactic form of the expression that produced it. When L is a type expression, L isa T tests whether the type denoted by L is a subtype of T.

abstract entity Animal {}

entity Dog isa Animal
{
    String bark;
}

entity Owner
{
    Animal pet;

    → Boolean petIsDog = pet isa Dog;
    → String sound? = if pet isa Dog then pet.bark else none;
}

For a value left operand, a type test is invalid when the static type known for the value is necessarily disjoint from T, because such a test cannot be satisfied. For a type left operand, the test is false when the left type is not a subtype of T.

A positive type test narrows the static type known for the tested expression in the guarded scope. For example, in if pet isa Dog then pet.bark else none, the then-branch may use members of Dog through pet. In pet isa Dog ∧ pet.bark = "woof", the right-hand side of the conjunction is checked with the same positive narrowing. The test does not introduce a general negative narrowing rule for else-branches or disjunctions.