59 Variant types

The following is an example of a variant type:


variant Shape
{
    Circle circle;
    Triangle triangle;
    Rectangle rectangle;
}

This represents a sum type. Although circle, triangle, and rectangle can be regarded as alternatives, they are called attributes just as for value and entity types, and they likewise are unary predicates having extensions. The attributes do not exist conditionally: all three attributes exist for every Shape and always have extensions. The variant constraint makes exactly one of those extensions non-empty. Indeed, we could annotate the attributes with their natural language predicates using metadata:


variant Shape
{
    @predicate("The shape is a circle value equal to [circle]")
    Circle circle;

    @predicate("The shape is a triangle value equal to [triangle]")
    Triangle triangle;

    @predicate("The shape is a rectangle value equal to [rectangle]")
    Rectangle rectangle;
}

In this case the attribute types are nominal types. The attribute types may also be structural types, and a variant may mix these forms. For example:


variant Shape
{
    { Real radius; } sphere;
    { Real side; } cube;
    { Real radius; Real height; } cone;

    → Real volume = sphere.(4.0/3.0*pi*radius^3)
                  | cube.(side^3)
                  | cone.(pi*radius^2*height/3);
}

A variant type is closed. In any loaded schema version, the set of current base attributes is fixed by the declaration. To model an open variant, declare an abstract value or entity type and allow concrete types to subtype it.

Variant types do not have a value/entity distinction. A variant cannot declare a key, but it may inherit one from an abstract entity supertype. A variant may declare abstract value types and abstract entity types as supertypes using isa. The need to implement the inherited attributes and key of an abstract entity is likely to limit the practical usefulness of abstract entity supertypes for variants.

An inherited abstract attribute does not independently become another variant alternative. A directly declared base attribute may implement that inherited requirement; alternatively, an inherited requirement may be implemented by a derived attribute.

Variant types may declare derived attributes. The alternative operator | is often useful for combining the results produced by different base attributes into one derived result, as in the definition of volume above.

To support 117 Schema evolution in databases and serialisation formats, previously existing base attributes can be dropped, allowing for deserialising older versions. When we speak of the base attributes of a variant type we do not include the attributes that have been dropped.

Carrier set

Before applying declared and inherited constraints, the carrier induced by the variant representation is the labelled disjoint union of the carriers of its base attributes.

variant Shape
{
    Circle circle;
    Rectangle rectangle;
}

has carrier:

carrier(Shape) =
    ({circle} × carrier(Circle))
    ∪ ({rectangle} × carrier(Rectangle))

More generally, if:

W = variant { T₁ A₁; ...; T_n A_n; }

then:

carrier(W) =
    ⋃_i=1ⁿ ({A_i} × carrier(T_i))

The attribute labels keep the summands distinct even when two attributes have the same underlying carrier.

Variant constraint

A variant type induces a mutual exclusivity constraint across its base attributes. For any instance, exactly one of those base attributes has a non-empty extension and every other base attribute has an empty extension. Derived attributes do not participate in this constraint.

This applies equally to attributes with the empty structural type {}.

Additional constraints may be specified either with where on an attribute or in a constraints block. The effective constraint on a variant type is the conjunction of its implicit mutual-exclusivity constraint, all inherited constraints, and all directly declared constraints. These constraints may mention multiple base attributes, including attributes that implement inherited abstract attribute requirements.

Constraints inherited from an abstract supertype

Consider the following example:


abstract value Solid
{
    { Real radius; } sphere?;
    { Real side; } cube?;

    constraints
    {
        // ∀S:{ Real radius; } ∀R:Real
        //     (this.sphere(S) ∧ S.radius(R)) → R > 0
        sphere.(radius > 0);

        // ∀C:{ Real side; } ∀L:Real
        //     (this.cube(C) ∧ C.side(L)) → L > 0
        cube.(side > 0);
    }
}

variant BasicSolid isa Solid
{
    { Float64 radius; } sphere where sphere.radius > 1;
    { Float64 side; } cube;
}

This deliberately contrived example illustrates several aspects of subtyping and constraints:

Sum types and product types are uniformly formalised through sets of attributes. This provides a powerful unification: queries can navigate both forms uniformly, without conditional field access. In this example, the sum type BasicSolid even subtypes the product type Solid.
The abstract value type Solid requires attributes named sphere and cube. For each required attribute, a concrete subtype must:
- implement the attribute;
- use the same or a narrower cardinality constraint; and
- use the same attribute type or a subtype of it.
The abstract requirements use ?, so each predicate may have an empty or singleton extension. In BasicSolid, each base attribute has declared cardinality 1 when selected, but effective cardinality ? because it is empty when another alternative is selected. It can therefore implement the corresponding abstract requirement without widening its cardinality. The implicit variant constraint additionally requires exactly one base attribute to be selected.
BasicSolid implements the payload types covariantly: { Float64 radius; } and { Float64 side; } are subtypes of the corresponding structural types containing Real.
BasicSolid inherits both constraints declared by Solid. For each value, the constraint on the selected alternative must be satisfied; the constraint on the absent alternative is vacuously satisfied because its antecedent is false.
The where clause on BasicSolid.sphere is an additional, directly declared constraint. It strengthens the inherited requirement from radius > 0 to radius > 1.

Payload-free attributes

A variant attribute which carries no application data may be written as a bare attribute name. For example:

variant PaymentResult
{
    completed;
    cancelled;
    String declined;
    { String provider; String reference; } pending;
}

The declarations completed; and cancelled; are syntactic sugar for attributes whose payload type is the empty structural type {}. The declaration above is therefore equivalent to:

variant PaymentResult
{
    {} completed;
    {} cancelled;
    String declined;
    { String provider; String reference; } pending;
}

The bare name is the attribute name and must be an identifier rather than a reserved keyword. Although the source form omits a type, the attribute is not untyped: its effective payload type is {}. When completed is selected its unary relation contains the single empty structural value; otherwise that relation is empty. It can therefore be navigated and tested like any other variant attribute.

In carrier-set terms, the payload-free summand contributes {completed} × carrier({}) to carrier(PaymentResult). Its attribute label distinguishes it from the other summands even though its payload carries no fields.

Cardinality constraints

Cardinality constraints apply within each variant base attribute in the usual way. The inactive current base attributes have empty extension, and the selected base attribute is the one with non-empty extension. Therefore a variant base attribute's declared cardinality must have lower bound at least one. For example:


variant Shape
{
    Circle circle;
    Point point+;
}

allows a shape to be either a single circle or a non-empty point set.

This implicitly means:

circle has declared cardinality one when selected
point has declared cardinality one or more when selected
the variant constraint ensures that exactly one effective current base attribute has a non-empty extension

A variant base attribute cannot be declared with cardinality ? or *, because those constraints allow an empty selected case. An empty extent already means the attribute is inactive.

To support an empty point set as a legitimate selected case, use a dedicated point set type and make the variant attribute a single value of that type:


variant Shape
{
    Circle circle;
    PointSet pointSet;
}

Generalisation to Algebraic Data Types

Algebraic Data Types are supported. For example:


@domain("A finite binary tree with integers at a subset of the leaf nodes")
variant BinaryTree
{
    @predicate("The binary tree is an empty node")
    {} empty;

    @predicate("The binary tree is a leaf node holding the integer value [leaf]")
    Integer leaf;

    @predicate("The binary tree is a binary node equal to [node]")
    { BinaryTree left; BinaryTree right; } node;
}

Note:

Recursive types are permitted
Attributes may use the empty structural type {} when they have no payload. These are ordinary unary attributes of type {}, similarly to enum attributes.
The attribute node has a unary predicate and holds a unary relation.
The type of attribute node is the structural type { BinaryTree left; BinaryTree right; }.

Previous58 Enumerated Types Next60 Quotient types