73 Subtypes of concrete types

Consider the following type, which defines both base and derived attributes:


value Rectangle
{
    Real width;
    Real height;
    → perimeter = 2 * (width + height);
    → area = width * height;
}

This type is concrete because it is not declared abstract. Note however that Rectangle is uncountable : : concreteness does not imply finiteness or countability.

Because Rectangle is concrete, it cannot appear as a supertype in an isa clause. The following is therefore illegal:


// illegal: cannot use isa with a concrete supertype
value Square isa Rectangle
{
    → height = width;
}

There are two valid ways to define Square as a subtype of Rectangle:

Refinement of a concrete supertype (adding constraints).
Embedding declaration into a concrete supertype.

In both cases, the subtype Square inherits the attributes of its supertype (width, height, perimeter, and area).

Hiding rule

Inheritance can produce name collisions. Predica applies a hiding rule:

Redefined attributes in a subtype hide attributes of the same name in a supertype.
If the same name appears in two supertypes that were not inherited through a common supertype, the name is ambiguous and produces an error.

Subtype through refinement

A subtype T where p expression restricts the carrier of a single concrete supertype using an additional predicate:


type Square = subtype Rectangle where width = height;

The where predicate may refer to the base type's attributes. Multiple constraints can be expressed by conjunction:


type Square = subtype Rectangle where width = height ∧ area > 0;

The keyword this refers to the base value within the where predicate. The first declaration above is syntactic sugar for:


type Square = subtype Rectangle where this.width = this.height;

The keyword this enables refinement of predefined types:


type PositiveReal = subtype Real where this > 0;

Subtype through embedding

A separately represented nominal type may be made a subtype of a concrete type by providing an embedding. In this alternative, Square must first declare the base attribute used by the embedding:


value Square
{
    Real side;
}

embed Square s isa Rectangle =
    Rectangle { width = s.side; height = s.side };

The general form is embed Source x isa Target = expression;. The expression is evaluated with x bound to the source value and must have type Target. The declaration defines an embedding Source → Target, making Source a subtype of Target.

This Square is different from the refinement type in the preceding section. The refinement denotes those existing Rectangle values whose width equals their height. The nominal Square above instead has its own representation, consisting of one base attribute side, and the embedding specifies the corresponding Rectangle value.

An embedding is a separate top-level declaration so that a subtype relationship can be provided after the source and target types have been declared, including when they are declared in different components. Keeping the embedding separate is useful for such retroactive relationships, although the source type and embedding may be placed together when they are designed as one unit.

The same form works for scalar or predefined supertypes:


embed Rational r isa Real =
    r.numerator / r.denominator;

For quotient source types, the embedding expression must be well-defined on equivalence classes: equivalent representatives must produce the same target value. An embedding must also preserve the source type's equality, so distinct source values do not collapse to the same target value.

Refining derived attributes through embedding

A subtype may provide a simpler calculation and a narrower type for an attribute of a concrete supertype. Because a nominal type can subtype a concrete type only through an embedding, the embedding must preserve the meaning of the attribute.

For example, a polygon calculates its area from its ordered vertices. An axis-aligned rectangle derives those vertices from a simpler representation and calculates the same area directly from its width and height:


value Polygon
{
    List<Point> vertex;
    → Real area = polygonArea(this);

    constraints
    {
        vertex.length ≥ 3;
    }
}

func Real polygonArea(Polygon polygon)
{
    var Integer count = polygon.vertex.length;
    var Real twiceSignedArea = 0;

    for Integer i in 0..count - 1 {
        var Integer next = if i + 1 = count then 0 else i + 1;
        var Point a = polygon.vertex[i];
        var Point b = polygon.vertex[next];

        twiceSignedArea += a.x * b.y - b.x * a.y;
    }

    return abs(twiceSignedArea) / 2;
}

value AxisAlignedRectangle
{
    Point origin;
    Float64 width;
    Float64 height;
    → List<Point> vertex = rectangleVertices(origin, width, height);
    → Float64 area = width * height;
}

embed AxisAlignedRectangle rectangle isa Polygon =
    Polygon { vertex = rectangle.vertex };

polygonArea applies the shoelace formula to consecutive vertices and wraps the final vertex back to the first. Taking the absolute value makes the result independent of whether the vertices are listed clockwise or anticlockwise.

Viewed as a Polygon, the area is defined by polygonArea(this). The rectangle's refined calculation must agree with that inherited meaning. Once the agreement is established, an implementation may use width * height, and the static type of AxisAlignedRectangle.area remains the narrower type Float64.

Previous72 Subtypes of abstract types Next74 Comparable Types