63 Derived Attributes

A derived attribute is an attribute whose extension is defined by an expression. It is a normal attribute for navigation and denotation; the difference is that its extension is calculated rather than supplied as stored state.

Every nominal type constructor supports derived attributes: value types, entity types, enum types, variant types, and quotient types. The rule is uniform because attributes are unary predicates on the values of the nominal type, and a derived attribute is just a unary predicate defined by an expression.

A derived attribute declaration begins with →. The marker distinguishes it from a base attribute independently of whether the declaration includes an explicit type. Canonical formatting places one space after the arrow.

Value and entity types

Value and entity types use the same member syntax for derived attributes:

value Circle
{
    Real radius where radius ≥ 0;
    → Real diameter = 2 * radius;
}

entity Person
{
    String email*;
    → Boolean hasEmail = email.Σexists;
}

The derived attributes diameter and hasEmail are available through ordinary path navigation. They do not introduce additional stored fields.

Enum types

Enum types also support derived attributes. Enum base attributes have type {}, so a derived attribute in an enum is evaluated against the selected enum value in the same way as any other derived attribute.

enum TrafficLight
{
    red,
    amber,
    green,

    → Boolean stop = red ∨ amber;
}

For a value t of type TrafficLight, t.stop is true for red and amber, and false for green.

Variant types

Derived attributes on variants are ordinary members of the variant type. They may test which variant attribute is active, inspect a payload, or expose a value calculated from the active case.

variant Payment
{
    Cash cash;
    Card card;

    → Boolean electronic = card.Σexists;
}

Quotient types

Quotient types may define derived attributes from their representation fields. A derived attribute intended to describe the quotient value should be well-defined on equivalence classes.

quotient Rational
{
    Integer numerator;
    Integer denominator where denominator > 0;

    → Boolean zero = numerator = 0;

    equivalence
    {
        x ~ y where x.numerator * y.denominator = y.numerator * x.denominator;
    }
}

The attribute zero is well-defined for rational values because replacing a representative by an equivalent representative preserves whether the represented rational number is zero.