9 Types

Predica largely accepts Date and Darwen’s value, type and variable semantics, logical interpretation, explicit identity and rejection of OO machinery. It departs from them by applying those principles to entity types and to the database as a whole. Where D&D retain relvars as variables outside the type system, Predica treats the database as a variable of a nominal type and obtains relvar-like pseudovariables through its attributes.

A type classifies mathematical values. It defines a carrier set of values and the operations that can be performed on those values.

A type has a set of attributes (i.e. names) which are available to be used in queries, and sometimes can be the target for update operations.

Structural types

A structural type is described by a type expression such as:

{ Integer a; Real b*; String c?; }

A value of a structural type is a tuple that records an extension for each attribute. For example:

(
    a = {-4},  
    b = {2.5, 3.7, 10.0},  
    c = {"hello"}
)

The extension of an attribute is a set of values of the attribute's declared type, regardless of its cardinality constraint.

Value types

An example of a value type is:

value Circle
{
    Point centre;
    Real radius where radius ≥ 0;
}

A value type is a nominal type. Its carrier is isomorphic to the carrier of the corresponding structural type using its non-derived attributes, after imposing the constraints.

Entity types

An example of an entity type is:

entity Supplier
{
    String id;
    String name;
    Integer status;
    key {id};
}

As for value types, entity types have a carrier which is a set of abstract mathematical values, and that set is defined in exactly the same way as for value types. In the formal language semantics entity types are treated like value types. At the level of the semantic model, however, a value in an entity type's carrier records the extensions of attribute predicates about an entity.

Entity types may declare keys, but these are irrelevant to how the carrier set and equality of the entity type are defined. Key constraints conveniently impose constraints on attributes that use the entity type. For example, the key constraint defined on Supplier is imposed on attribute supplier of ShipmentsSystem:

entity ShipmentsSystem
{
    Supplier supplier*;
}

At the level of the semantic model, the main purpose of distinguishing entity types from value types is to express a metaphysical distinction. Attributes express predicates about the things classified by those types, and all changing database state resides in their extensions.

In most cases, the intended modelling role makes it clear whether a type should be an entity type or a value type. This can readily be seen by considering the examples in the table.

The metaphysical distinction is only informal. It is useful in practise to think of entities as things that exist in time and space and can be referred to, albeit taking this very liberally. An entity need not be a physical object; it may also be an organisation, event, action, or relationship. A birth, a marriage, a shipment, or an ownership are all entities in this sense. Predica therefore has no separate category of relationship types.

The Entity–Relationship Model (ERM) distinguishes entity boxes from relationship diamonds. Predica has no corresponding category of relationship types.

Computer representations are not the values they denote or the entities they identify, and the same value or entity may have many representations. Predica permits types to classify both mathematical values and modelled entities while keeping them distinct. This allows a schema to express the kinds of things in its model directly.

Semantic distinction: entity occurrences can be shared

Values have no identity beyond their structure, so two locations may independently hold equal values. Entities can instead have shared occurrences in a model: several paths may reach the same occurrence, and an update through any one of those paths updates the location shared by all of them. This sharing is established by the schema constraints; an entity type by itself does not make arbitrary occurrences shared. Location denotation is interpreted under those constraints and retains the entity witnesses needed to identify shared attribute locations. Sharing is therefore observable language behaviour, not merely a choice of physical representation. An implementation may realise shared locations using references and key-indexed collections, but it must preserve the behaviour defined by the constrained location semantics.

For example, consider a supplier-and-parts schema in which shipments are recorded under both their supplier and their part:

entity Supplier
{
    Integer id;
    Shipment shipment* where shipment.supplier = this;
    key {id};
}

entity Part
{
    Integer id;
    Shipment shipment* where shipment.part = this;
    key {id};
}

entity Shipment
{
    Supplier supplier;
    Part part;
    Integer qty;
    key {supplier, part};
}

entity ShipmentsSystem
{
    Supplier supplier*;
    Part part*;
    → Shipment shipment* = either supplier.shipment, part.shipment;
}

The where constraints require a shipment under a supplier to name that supplier and a shipment under a part to name that part. Together with the key on Shipment and the definition of ShipmentsSystem.shipment, these constraints determine when the two paths reach the same shipment occurrence. Thus a shipment h for supplier s and part p is visible through both s.shipment and p.shipment as one shared occurrence, not as independent copies. The following targets therefore denote the same Shipment.qty location:

s.shipment.[part = p].qty
p.shipment.[supplier = s].qty

After an assignment through either target, a query through the other path observes the assigned quantity. The derived ShipmentsSystem.shipment attribute observes that same updated shipment as well. A conforming implementation must exhibit this behaviour whether it represents the shipment once and shares a reference, maintains indexes over it, or uses another physical representation.

TODO: Complete the location semantics by defining location denotation relative to the schema constraints and stating when those constraints entail that entity witnesses reached through different paths denote the same occurrence. In particular, the rules must derive from the schema above that the two targets produce the same concrete address.

TODO: Define how a write to an attribute of a shared entity occurrence updates every base extension that contains that occurrence while preserving the constraints on the enclosing values. This definition must cover an update to a key attribute as well as an update to a non-key attribute such as qty.

TODO: Reconcile the general location-semantics rule that ∪= computes set union with the keyed replacement semantics of ∪= on entity-typed extensions, including the unresolved case where different candidate keys match different existing members.

Another possible distinction when value types have keys

If value types can declare keys, a further formal distinction arises between value and entity types.

Note: The formal semantics distinction is deontic:

• Value types must satisfy the determinacy condition.
• Entity types are not required to satisfy it.

The following value type satisfies the determinacy condition, but only because its constraints establish the internal isomorphism between its Cartesian and polar coordinates:

value Point
{
    Real x;
    Real y;
    Real r;
    Real θ;

    key {x,y};
    key {r,θ};

    constraints
    {
        r = sqrt(x^2 + y^2);
        θ = atan2(y,x);
        x = r * cos θ;
        y = r * sin θ;
    }
}

Without these constraints, Point would violate the determinacy requirement for a value type.

Attributes

Attributes are part of the type system, but they are also logical predicates. An attribute does not store a collection inside a value. It denotes a unary predicate from an instance of the containing type to an extension of values of the attribute type.

The cardinality marker constrains that extension:

entity Supplier
{
    Integer id;
    String name;
    City city*;

    key {id};
}

Here city* does not mean that the attribute type is “set of cities”. The attribute type is City. The * says that the extension of the city predicate may contain zero or more city values for a supplier. The same pattern covers single-valued, optional, non-empty, and bounded attributes.

Type expressions

A type expression is syntax that denotes a type. It may refer to a nominal type by name, write a structural type directly, or form a type from existing types:

String
Set<String>
subtype Real where this > 0
union { EmailContact, PhoneContact }
intersection { Shape, Visible }
{ String name; Point point; }

For example, union { A, B } denotes the union of the carrier sets of A and B, while intersection { A, B } denotes values that inhabit both. Union and intersection of two types are only permitted when equality is defined across them.

Type expressions are recursive, so they can be nested inside each other:

Set<(subtype (union { EmailContact, PhoneContact }) where verified)>

Type aliases

A type declaration gives a name to a type expression. The name can then be used in place of that type expression to mean the same thing; it does not declare a new type:

type Names = Set<String>;
type PositiveReal = subtype Real where this > 0;

Subtyping

Subtyping is subset inclusion:

A is a subtype of B iff A ⊆ B

The subtype relation gives rise to a type graph.

Abstract types and nominal subtyping

An abstract type introduces a carrier set without providing constructors for all of its values. Concrete nominal types can select subsets of that carrier. Abstract types are useful when the model needs a common domain, but no single concrete representation covers every possible value.

abstract value Shape
{
    Real area;  // Abstract types can declare attributes.
}

value Circle isa Shape
{
    Point centre;
    Real radius;
    → area = pi * radius * radius;  // Can implement inherited attributes.
}

Circle isa Shape declares Circle as a nominal subtype of Shape. The area attribute declared by the abstract type is given a derived definition by Circle.

Refinement types

A refinement type denotes the subset of an existing type whose values satisfy a predicate.

type Adult = subtype Person where age ≥ 18;

Adult is a type alias for the subset of Person values whose age satisfies the refinement predicate. It does not declare a new nominal type.

Equality and comparability

Equality is not automatically available between every pair of types. An equality expression is well-typed only when equality is defined for the relevant static types. Values of the same concrete value type usually have intrinsic equality. Structural, enum, and quotient types define equality by their own rules. Subtypes use equality from their base type.

value BadComparison
{
    Point p;
    Supplier s;

    constraints
    {
        // Static type error.
        // Equality is undefined between Point and Supplier.
        p = s; 
    }
}

Two different types can also become comparable through a concrete common supertype with defined equality, through an explicit equality function, or through a disjointness declaration that makes cross-type equality always false. This is why type expressions and equality evidence are separate concerns.

Static typing and cardinality

Predica is statically typed by default. A variable, attribute, parameter, or expression has an element type known to the checker. Locations and path expressions also have cardinality information. These are separate checks:

• The element type says what kind of value may appear.
• The cardinality says how many such values may appear.

For example, Integer id* has element type Integer and cardinality zero or more. It is not an attribute of type Set<Integer>. Flow-sensitive checks may refine cardinality or type inside a guarded scope, such as after testing that an optional path is not none, or after a positive isa type test.