55 Value Types

Example: Point type

The following declares a value type named Point, having two attributes x and y of type Real:

value Point
{
    Real x;
    Real y;
}

Note that Point and Real are types whereas x and y are attributes.

This is a nominal type declaration that does three things simultaneously:

• It introduces a new type, named Point.
• It introduces nominal constructor syntax using the type name. The preferred form names the attributes being supplied:

  
          var p = Point { x = 1, y = 2 };
          

  This form is stable if attributes are reordered or if optional attributes are later added. A positional shorthand is also available when every required base attribute is supplied in declaration order:

  
          var p = Point(1, 2);
          

  The positional form is shorthand for the named-field constructor. It is not an ordinary component function and it should not be used when the named form would be clearer.
• It introduces attributes x and y. In path expressions, these behave like projection or navigation from a point to its coordinates:
      x : Point → Real
    y : Point → Real
  
  The attributes are available using dot notation. For example:

  
          // Use the attributes as path expressions
          print p1.x, p1.y;
          

  In the logical interpretation, the same attributes are predicates. For example, p.x(X) is a formula using x as a predicate, meaning that X is an x-coordinate of p.

Why the keyword value instead of struct or record

Although struct or record may seem more conventional, the keyword value is used for two reasons:

• It signals nominality.
  The words struct and record suggest structural types. Predica already has explicit structural types, described in 47 Structural types. For example:

  
          type Point = { Real x; Real y; };
          

  declares Point as an alias for a structural type.
• It aligns with Predica’s conceptual model.
  Predica’s two primary nominal type constructors are value and entity. Their names reflect their intended metaphysical roles:
  • value types represent mathematical values
  • entity types represent things that exist in time and space
  Using value makes this distinction explicit and intuitive.

Example: Circle type

The Point type can be used in the definition of other types, such as the Circle type:

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

This may look like a tuple type, but it is not a tuple type. There are some important distinctions:

• The values may represent mathematical values like circles. A circle is a locus in R^2, not a tuple.
• A value type may include constraints that restrict its admissible values. In logical terms, these constraints are axioms about the type and its attributes.

A value type has these properties:

• It has no object identity beyond value equality.
• Two values are equal iff their attributes are equal.
• A value represents an abstract mathematical object, not a concrete object which physically exists in time and space.
• It has no key defined and it cannot be referenced by a key.
• It is always embedded, never referenced.

Value types are ordered by default when their base attributes provide a canonical comparison, unless the declaration uses unordered. They can also supply an explicit order declaration. The general rules are described in 66 Ordering.

Carrier set

The structural body of a value type is the structural type obtained from its attribute declarations, before applying any constraints. For example:

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

has structural body:

{
    Point centre;
    Real radius;
}

A value type declaration introduces a named type whose carrier is isomorphic to the constrained carrier of its structural body.

If S is the structural body of a value type V, and K is the conjunction of its constraints, then:

carrier(V) ≅ { v ∈ carrier(S) | K(v) }

The constraints K include constraints written in the constraints block and constraints introduced by where clauses on attributes. In the example above, K includes radius ≥ 0.

The isomorphism is canonical: a value of V has the same observable attribute extensions as the corresponding structural value. However, V is a nominal type, so it is not the same type as its structural body.