60 Quotient types

Definition (Quotient Type). A construct of the form quotient T {...} defines a type named T whose values are equivalence classes over a representation defined by a set of attributes of given types. Two representatives x and y denote the same value iff the predicate in the equivalence block holds for them.


quotient Rational
{
    // Base attributes for the representation
    Integer numerator;
    Integer denominator where denominator > 0;

    // Derived attribute
    → Boolean zero = numerator = 0;

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

The ordinary attributes of a quotient type are representation fields. where clauses and constraint blocks restrict the allowed representatives. Derived attributes may be defined from the representation fields and are available through values of the quotient type.

Carrier set

The carrier of a quotient type is the set of equivalence classes of its allowed representatives.

Let S be the structural body obtained from the quotient type's representation fields, and let K be the conjunction of its representative constraints, including where clauses on representation fields and constraints written in a constraints block. The allowed representatives are:

Rep(T) = { r ∈ carrier(S) | K(r) }

If ~T is the equivalence relation declared by the equivalence block, then:

carrier(T) = Rep(T) / ~T

For the Rational example above, the representatives are pairs of integers (numerator, denominator) with denominator > 0, and two representatives are in the same carrier element exactly when cross-multiplication gives the same rational value.

Derived attributes of a quotient type may also be representation-dependent. For example, zero above is well-defined for rational values, but a derived attribute such as → hasNumeratorOne = numerator = 1 would observe the chosen representative unless the quotient also guarantees a canonical representation. The base language allows both forms.

Representatives and equality

For a quotient type T, write Rep(T) for the type of its representation. For Rational, Rep(Rational) has attributes numerator and denominator, subject to the declared representative constraints such as denominator > 0.

The equivalence block defines an equivalence relation ~T on Rep(T). A value of type T is an equivalence class of representatives under ~T. Equality of quotient values is equality of those equivalence classes, not structural equality of the representative attributes.

Representation fields are ordinary attributes for navigation. They may be used in path expressions, queries, functions, and derived attributes without a special access rule. This is useful for debugging, rendering, efficient algorithms, and definitions that are naturally written against the representation.

The equivalence predicate is checked in a context where the two distinct variables denote representatives with the declared representation fields. The predicate must have type Boolean.

Well-defined quotient operations

An expression over quotient values is well-defined on quotient values when replacing any representative by an equivalent representative leaves the result equal, using the equality of the result type.

For a function


func B f(A x);

where A is a quotient type, well-definedness means:


x ~ y ⇒ f(x) = f(y)

Here ~ is the equivalence relation of A, and = is equality of the result type B. If B is a quotient type, this result equality is its quotient equality. The same condition extends to functions with more parameters by replacing each quotient-typed argument by an equivalent representative.

Using representation fields can make an expression depend on the chosen representative. This is not rejected by the base language: a query might deliberately ask for the stored numerator and denominator of a rational value. However, an operation intended to be a property of the quotient value should be well-defined on equivalence classes. In other words, if x ~ x' and y ~ y', then such an operation should return the same result for (x, y) and (x', y'). Tools may warn about representation-dependent definitions, or treat such warnings as errors in applications that require a stricter abstraction boundary.


func Boolean ≤(Rational x, Rational y) =
    x.numerator * y.denominator ≤ y.numerator * x.denominator;

For the Rational declaration above this comparison is well-defined because every allowed representative has a positive denominator. Replacing either argument with an equivalent representative preserves the truth of the cross-multiplication comparison. If negative denominators were allowed as arbitrary representatives, this particular expression would not be well-defined without first normalising the sign or otherwise accounting for it.

The block form is deliberately heavier than a single inline equation. A quotient type has one defining equivalence relation, but that relation may need associated representation policy.

TODO: the following canonical-representative clause is an experimental idea. There is a good chance it will not be supported by the base language. This example is non-normative.


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

    canonical x:
        gcd(abs(x.numerator), x.denominator) = 1;
}

If supported, a canonical clause would not define equality. It would select a preferred representative for each equivalence class when such a representative is available and unique. This could guide storage, rendering, indexing, and deterministic comparison, while the equivalence predicate remains the source of the quotient's equality.

Previous59 Variant types Next61 Attributes