50 Equality Between Types

Equality in Predica is defined between pairs of static types. It must be reflexive, symmetric, and transitive wherever it is defined, but it is not necessarily defined between every pair of types. An expression such as x = y is well-typed only when equality is available for the static type of x and the static type of y. When no such equality is available, the two types are incomparable for equality and the comparison is a type error.

value B { Integer x; };
value C { Integer x; };

var b = B { x = 1 };
var c = C { x = 1 };

print b = c;        // type error unless equality between B and C is defined

Intrinsic equality

Every type defines equality on its own values, so values of the same static type can always be compared. Predefined scalar types, concrete value and entity types, enumerated types, structural types, and quotient types define equality according to their own rules. Equality on abstract types is specified in 71 Abstract types. Equality between two different static types still requires the types to be comparable.

Equality can also be available through a concrete common supertype. If two static types share a unique least common supertype with defined equality, then values of those two types can be compared using equality at that supertype.

Pairwise equality definitions

Equality between two different types can be defined explicitly by declaring the equality function for that pair:

value B { Integer x; };
value C { Integer x; };

func Boolean =(B b, C c) = b.x = c.x;

The declaration defines symmetric equality between B and C: b = c and c = b use the same predicate. The predicate must return Boolean, and it must be compatible with all other equality definitions involving B and C so that equality remains reflexive, symmetric, and transitive wherever it is defined.

Compound type expressions

Compound type expressions can require equality to be available across their members. The syntax of the type expression is independent of this requirement: union { ... } and intersection { ... } are parsed as ordinary type expressions, and the type checker then verifies the equality evidence needed by the context.

For a union type expression such as:

type Contact = union { EmailContact, PhoneContact, PostalContact };

equality on Contact is available only when equality is defined for every relevant pair of member types. Pairs that already share defined equality need no extra declaration. Other pairs require an explicit equality definition or some other declaration that makes equality available.

Intersection types have the corresponding requirement that the member types be comparable with a coherent equality. For example, intersection { A, B } denotes values that inhabit both member types, so the identity of such values must not depend on which member type is used to observe them.

Disjointness declarations

A disjointness declaration is the compact form for the common case where a set of types are known to have no values in common:

disjoint EmailContact, PhoneContact, PostalContact;
type Contact = union { EmailContact, PhoneContact, PostalContact };

The declaration asserts pairwise disjointness between the listed types. Therefore equality between values of distinct listed types is defined and always false. It is rejected if the type graph or intrinsic language rules already imply that any listed pair necessarily overlaps.

From the point of view of making equality available, disjoint A, B; behaves like shorthand for defining cross-type equality as false. It is stronger than an equality function returning false, because it also records the type-graph fact that the carrier sets of A and B do not overlap.