71 Abstract types

Concrete types

Consider a concrete type such as:


value Code
{
    Integer number;
}

We say this is concrete because its attributes uniquely determine its carrier. For example, in this case the carrier for Code is:


{ Code{ number={N} } | N ∈ ℤ }

Uncountable types

In Predica, a type may be uncountable, even though no finite representation can denote all of its values. The predefined type Real is the canonical example.

Types with attributes of uncountable types are typically uncountable themselves. For example, the following type is uncountable because its attributes range over Real:


value RealPoint { Real x; Real y; };

The type Real denotes the mathematical continuum. Implementations may approximate Real using representational numeric types such as Float32, but such approximations are not part of the denotation.

Although RealPoint is uncountable, we say it is concrete because its carrier is determined by its attributes:


{ RealPoint{ x={X}, y={Y} } | X ∈ ℝ and Y ∈ ℝ }

Abstract types

The abstract keyword introduces an abstract type and may be used for both value and entity types.

Informally, an abstract type has a domain, and its attributes are unary predicates on that domain. The domain and attributes may be described informally using metadata. For example:


@domain("A shape is a locus of points in Euclidean 2d space")
abstract value Shape
{
    @predicate("The area of the shape is [area]")
    Real area;

    → Real equivalentRadius = sqrt(area / pi);
}

Definition: The supertypes of a type are the type itself plus its directly declared supertypes and their supertypes and so on.

Definition: The direct and indirect attributes of a type means the attributes in its supertypes (including itself).

Definition: A value type or entity type which is declared abstract means its carrier is not determined by its direct and indirect attributes. The direct and indirect attributes describe properties of its values but do not collectively identify a value in its carrier. It is possible that distinct carrier values can have identical attribute extensions, for every direct and indirect attribute.

For example, Shape is abstract because the attribute area doesn't determine a shape value.

Note that the metaphysical distinction between value and entity types is irrelevant. Both entity and value types have carriers which are mathematical sets, not naive sets. A concrete entity type has attributes that identity a value in its carrier. The attributes of a concrete (non-abstract) value or entity type define what the carrier is. The fact that entity types are intended to be associated with entities in the real world that have additional properties not modelled by the attributes is irrelevant.

Because the attributes of an abstract type do not collectively identify a value, they cannot be used with nominal constructor syntax to denote one.

Any type, whether abstract or not, may declare:

a list of supertypes
constraints
derived attributes
theorems

Variables may have an abstract type, but an abstract type cannot be used with nominal constructor syntax to denote values. This is a direct consequence of what abstract means. The following is therefore illegal:


var s = Shape { area = 10.0 };      // Error: cannot instantiate abstract type

Shape is not abstract because it is “conceptual”. There is nothing abstract about shapes being subsets of ℝ². It is abstract because its attributes don't determine a shape value.

Abstract types tend to be uncountable:

The set of all shapes in ℝ² is uncountably infinite.
No finite set of constructors can enumerate them.
No concrete representation can cover the entire domain.
Any concrete subtype (Circle, Rectangle, Polygon, etc.) captures only a subset.

but that is not the defining characteristic of "abstract". For example, RealPoint is uncountable, but not abstract.

An abstract type conceptually introduces a carrier set but does not specify its representation, its elements, or its structure. It is a semantic placeholder. When a nominal type subtypes an abstract type, it selects a subset of that abstract carrier as its own carrier.

Equality on abstract types

Predica defines equality on every type. For abstract types, however, equality and the implementation of attribute extensions must be considered separately for value types and entity types.

Abstract entity types

Every abstract entity type must have at least one explicitly declared or inherited key. An attribute extension whose element type is an abstract entity can therefore use the complete extensions of the key attributes for membership, indexing, duplicate detection and keyed replacement, including when its members have different concrete subtypes.

A key does not define equality on the abstract entity carrier. It is an extension-local constraint: two distinct carrier values with the same key profile may not coexist in an extension governed by that key. The existence of a key therefore does not imply that the abstract entity's attributes collectively determine its carrier values, and does not make the entity type concrete.

Abstract value types

Abstract value types have no entity key available to implement their extensions. An attribute such as Shape shape* therefore requires equality to be available between all concrete values which may inhabit Shape. Declaring a new subtype is valid only when its values remain comparable with the other values of the abstract type. That comparability may follow from an existing common concrete supertype, an explicit equality definition, or a disjointness declaration.

This mutual-comparability requirement permits values of different concrete subtypes to coexist in an extension of the abstract value type. Membership, set operations and folds such as Σcount then remain well-defined on that extension.

TODO: Determine how mutual comparability is established in an open subtype hierarchy. For example, independent third-party components may each declare a new subtype of Shape without depending on one another, so no component is naturally responsible for declaring equality or disjointness between every pair of subtypes. The language needs a practical rule which preserves separate extensibility while ensuring that extensions of Shape still have well-defined equality.

Abstract attribute requirements

An underived attribute declared by an abstract type is an interface requirement on its subtypes. The attribute and its predicate are inherited, but the abstract declaration does not provide a base or derived implementation of the attribute. A concrete subtype must provide an implementation. An abstract type may also declare a derived attribute; its definition is inherited as an implementation rather than as an outstanding requirement.

For example, RectangleShape.width and RectangleShape.height are attribute requirements, whereas RectangleShape.area is a derived attribute with an implementation:


abstract value RectangleShape
{
    Real width;
    Real height;
    → Real area = width * height;
}

value ConcreteRectangle isa RectangleShape
{
    Real width;
    Real height;
}

ConcreteRectangle must implement width and height, but it does not need to implement area because it inherits the derived definition. A subtype may optionally provide a refined derived definition as described below.

Unimplemented attribute requirements

An abstract subtype may leave an inherited attribute requirement unimplemented, passing the requirement on to its own subtypes. A concrete type must implement every direct and indirect abstract attribute requirement.

For example, the abstract subtype Quadrilateral may leave Shape.area unimplemented. The requirement passes to IncompleteRectangle, which is illegal because it is concrete and still does not implement it:


abstract value Quadrilateral isa Shape
{
}

value IncompleteRectangle isa Quadrilateral
{
    Float64 width;
    Float64 height;
}

The compiler reports the unimplemented requirement:

Concrete type IncompleteRectangle does not implement
attribute area defined in supertype Shape.

Inherited constraints

Constraints declared by an abstract type are inherited by its subtypes. A subtype does not need to repeat an inherited constraint and cannot remove or weaken it. It may declare additional constraints which further narrow its carrier.

For example, Length implements the magnitude attribute requirement and inherits the constraint that its value is non-negative:


abstract value NonnegativeMeasure
{
    Real magnitude;

    constraints
    {
        magnitude ≥ 0;
    }
}

value Length isa NonnegativeMeasure
{
    Real magnitude;
}

var invalid = Length { magnitude = -1 };  // Error: inherited constraint is violated

Omitting the constraint from Length, or declaring a weaker constraint there, does not admit values excluded by NonnegativeMeasure. All inherited and directly declared constraints apply conjunctively.

Keys

Every abstract entity type must have at least one explicitly declared or inherited key. An abstract entity does not receive the default all-base-attribute key because its attributes do not collectively identify its carrier values. A root abstract entity must therefore declare a key. An abstract subtype may inherit a key without repeating it. The general rules for keys and key attributes are specified in 57 Keys.


abstract entity Identified
{
    String identifier;

    key {identifier};
}

entity Customer isa Identified
{
    String identifier;
    String name;
}

The key on Identified is inherited. Customer cannot remove or replace it, and must implement the identifier requirement, but does not repeat the key declaration. The inherited key allows an attribute of type Identified to distinguish and index values uniformly, including when its extension contains values of different concrete subtypes. A subtype may declare additional candidate keys.

Covariant attribute types

A subtype may implement an abstract attribute as either a base attribute or a derived attribute. The implementing attribute may have the same type as the abstract attribute or a subtype of it. Every value permitted by the implementation must be permitted by the abstract attribute requirement. This rule is called covariance: the implementing attribute type is permitted to vary in the same direction as the subtype relation.

For example, the following Point and Circle types use Float64 attributes. Circle implements the inherited Shape.area : Real requirement as a derived Float64 attribute. This is valid because Float64 is a subtype of Real:


value Point
{
    Float64 x;
    Float64 y;
}

value Circle isa Shape
{
    Point centre;
    Float64 radius;
    → Float64 area = pi * radius * radius;
}

Refining inherited derived attributes

A subtype may provide a refined calculation for an inherited derived attribute. The refined calculation does not replace the inherited definition: both definitions constrain the same attribute extension and must agree for every value in the subtype carrier. The subtype may also narrow the attribute type when the refined result belongs to a subtype of the inherited type.

For example, Shape.equivalentRadius calculates the radius of a circle having the same area. The area attribute does not identify a shape, but it provides enough information for this derived calculation. For a disk, the equivalent radius is simply its radius:


abstract value Shape
{
    Real area;
    → Real equivalentRadius = sqrt(area / pi);
}

type NonnegativeReal = subtype Real where this ≥ 0;

value Disk isa Shape
{
    NonnegativeReal radius;
    → Real area = pi * radius * radius;
    → NonnegativeReal equivalentRadius = radius;
}

The inherited definition → equivalentRadius = sqrt(area / pi) remains part of Disk and must agree with the refined definition → equivalentRadius = radius. The refined calculation is simpler and narrows the static result type from Real to NonnegativeReal without changing the inherited meaning.

Refining free functions on subtypes

A free function defined for an abstract type may be refined by declaring an overload whose parameter type is a subtype. Calls with the more specific static argument type select the refined overload.


func String describe(Shape shape) = "shape";
func String describe(Circle circle) = "circle";

Circle circle = ...;
Shape shape = circle;

describe(circle)  // selects describe(Circle)
describe(shape)   // selects describe(Shape)

This is static overload refinement, not method overriding or dynamic dispatch. Free functions are not members of a type and are not inherited. The subtype overload is selected because its parameter type is more specific, not because the runtime value has that subtype.

Narrowing cardinality constraints

A subtype may implement an abstract attribute with a narrower cardinality constraint. Every cardinality permitted by the implementation must be permitted by the abstract attribute requirement.

For example, Path.point* permits any number of points, including none. NonemptyPath implements the attribute as point+, narrowing its cardinality to one or more:


abstract value Path
{
    Point point*;
}

value NonemptyPath isa Path
{
    Point point+;
}

Previous70 Necessarily disjoint and non-disjoint Next72 Subtypes of abstract types