66 Ordering

Some Predica operations require a stable comparison on values, such as ordered comparison operators, ordered indexes, deterministic rendering, and query operations such as orderBy. A type is ordered when the language defines a standard order relation ≤ on its values. This relation is the type's canonical comparison; it is total and non-exceptional.

Ordering is a semantic property of a type. It does not change the type's carrier set, equality relation, subtype relationships, or identity rules. It only says how two values of the same type are compared when an ordered comparison is required.

Order axioms

For an ordered type T, the standard order relation ≤ is a binary relation on values of type T. For all x, y, and z of type T, it must satisfy:

Reflexivity: x ≤ x.
Antisymmetry: x ≤ y ∧ y ≤ x ⇒ x = y.
Transitivity: x ≤ y ∧ y ≤ z ⇒ x ≤ z.
Totality: x ≤ y ∨ y ≤ x.

The relation is also non-exceptional: for any two values of the same ordered type, x ≤ y is defined and evaluates to a Boolean value.

Derived comparison operators

The standard order operator ≤ is the primitive comparison associated with an ordered type. The other ordered comparison operators are derived from ≤ and equality:

x < y iff x ≤ y ∧ x ≠ y.
x ≥ y iff y ≤ x.
x > y iff y ≤ x ∧ x ≠ y.

These derived operators do not add separate ordering semantics. They are available exactly when the standard order relation ≤ is available for the compared values.

Default ordering and opt-out

When a declaration kind has an implicit default order, the type is ordered by default. The unordered modifier suppresses that default order and is written just before the nominal type name. It is valid only when the declaration would otherwise have an implicit default order.


enum Month
{
    jan, feb, mar, apr, may, jun, jul, aug, sep, oct, nov, dec
}

value Time
{
    Integer hour where hour ∈ [0..23];
    Integer minute where minute ∈ [0..59];
    Integer second where second ∈ [0..59];
}

value unordered DebugTime
{
    Integer hour where hour ∈ [0..23];
    Integer minute where minute ∈ [0..59];
    Integer second where second ∈ [0..59];
}

Implicit ordering

Predica may define an implicit order when the declaration contains enough ordered structure to compare values without adding policy. The default orders are:

Boolean's ≤ relation is the order with false ≤ true.
Real's ≤ relation is the standard mathematical order.
String's ≤ relation is lexicographic order over Unicode scalar values. It is not locale-sensitive collation and does not depend on the string's physical encoding.
A subtype of an ordered type inherits the ordering on its supertype. Note therefore that the predefined types Int8, Int16, ..., Float32, Float64, and Integer inherit an order from Real.
An attribute of type T is ordered if and only if T is ordered and the cardinality constraint is exactly one. Optional, set-valued, and relation-valued attributes do not acquire an order merely because their element type is ordered.
A structural type is ordered if and only if each of its attributes is ordered. Structural values are compared lexicographically by the type's attribute sequence, all ascending. Once the type is fixed, the comparison uses the ordered attribute values. The empty structural type is trivially ordered.
An enumerated type is ordered by default using the source order of its attributes.
A value type is ordered by default when each base attribute is ordered. Its default order is the structural order of its base attributes in declaration order. Derived attributes are not part of the implicit default order.
An entity type is ordered by default when its first declared key exists and each key attribute is ordered. Its default order is lexicographic order by the attributes of that key. An entity type without a key has no implicit default order.
A variant type is ordered by default first by its active attribute discriminant, using the source order of the attributes. If the discriminants are equal, the payloads are compared using the order of the attribute's payload type. Payload-free attributes compare by discriminant alone. An attribute with a multi-valued payload has no implicit payload order.
A quotient type has no implicit default order. Its values are equivalence classes, not representation tuples. In general, lexicographic order on the representation fields is not well-defined on the quotient values: equivalent representatives may have different positions in the representation order. Therefore it does not generally define a ≤ relation satisfying the order axioms on the quotient type.

If no implicit default order is available and no explicit order is supplied, the type is not ordered. The unordered modifier cannot be combined with an explicit order. Sets remain mathematical sets; use explicit ordering operations when an ordered list is required.

Ordering value and entity types

An order can be defined explicitly by implementing function Boolean ≤(T x, T y).

Value and entity types can also define a custom order with an order declaration. The order keys are expressions evaluated in the scope of the value being compared. Keys are compared lexicographically from left to right.


value Date
{
    Integer year;
    Month month;
    Integer day;

    order [year↓, month, day];
}

Order keys can be expressions, not only attribute names:


value Point
{
    Real x;
    Real y;

    order [x*x + y*y, x, y];
}

The direction marker is written after the key expression: ↑ means ascending and ↓ means descending. If no direction marker is written, ascending order is assumed. The postfix marker keeps the key expression and the ordering direction separate; for example, year ↓ says to compare the year key in descending order, not to compare the arithmetic expression -year.

Every order key must be single-valued and ordered. The declared keys must induce a total order compatible with equality: if all order keys compare equal, the two values must be equal values of the type. A partial sort key is appropriate for query-level orderBy, but not for the canonical order of an ordered type.

Ordering an enum type

An order can be defined explicitly on an enum by implementing ≤:


enum Color
{
    red,
    green,
    blue
}

// Explicit order: blue < green < red.
func Boolean ≤(Color x, Color y) =
    if x = y then
        true
    else if x = blue then
        true
    else if y = blue then
        false
    else if x = green then
        true
    else
        false;

Ordering a quotient type

A quotient type has no implicit default order, but it can still define ≤ using an expression whose truth is invariant under the quotient equivalence. For example, rational numbers can be represented by integer numerator-denominator pairs with positive denominators:


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

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

The quotient can be embedded in Real by interpreting each rational value as its mathematical real value:


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

This embedding is well-defined on equivalence classes. Because Real is ordered, Rational inherits Real's standard ≤ relation through the embedding. In terms of the numerator and denominator representation, the inherited order is equivalent to cross multiplication:


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

Because denominators are positive, the cross-multiplication form is invariant under the equivalence relation: choosing different representatives of the same rational values does not change the truth value of x ≤ y. It therefore describes a relation on rational values, not merely on representation tuples, and that relation satisfies the order axioms.

Previous65 Generics Next67 Constraints