38 Type Checking Path Expressions

This chapter gives an informal way to think about type checking path expressions. The full definition is recursive: each path tail is checked in the context produced by the tails before it. Part XIV: Semantics formalises the propagation of type information recorded in frames, and therefore formalises the static typing of path expressions. Here the aim is only to make the typing intuition clear.

Attributes are generally named with singular nouns, such as course or name, and have singular types like Course or String. Predica path expressions have the singular type of each reached value. A path may reach many values through such an attribute, but each reached value still has the attribute's singular type. Set-valued expressions are available when the set itself is needed, for example by writing course.Σ.

Current type

While reading a path from left to right, the type checker keeps track of the current type. A navigation step may be used when the current type has the named attribute. After the step, the current type is the declared type of that attribute.

For example, if course has type Course and code has type String, then:

u.course.code

is checked by first reaching courses from u, then checking code from each reached course. The code step reaches String values.

Cardinality is not part of the type

An attribute's cardinality says how many values may be reached. It is not part of the type itself. A plural attribute of type Real still reaches Real values, one at a time.

For example:

value X
{
    Real v*;
}

The attribute v can reach many values, but each reached value has type Real. This is why the following expression type checks:

func Real square(Real x) = x*x;

x.(square(v) as product)

The function square takes one Real. The path tail v reaches Real values, so square(v) applies the function to each reached value. The result may have many product values, but each individual function call is still a call on a Real value.

This is the same rule described earlier for filters: do not mistake a plural attribute for a set-valued expression. If name has type String, then each reached name is a String, even when many names can be reached.

u.department.[name ∈ {"Mathematics", "Physics"}]

The condition uses ∈ because each reached name is a String. It does not use ⊆, because name is not a set-valued expression.

Tuple construction

In tuple construction, each component is checked from the same current type. The current value denoted by this does not change between components.

u.course.(code, title)

Both code and title are checked from Course, because both are inside the tuple construction following u.course.

Filters

A filter condition is checked from the current type, and the filter keeps current values for which the condition holds. The condition must be a Boolean-valued expression. The filter does not change the type of the current value.

u.course.[advanced].code

The filter [advanced] is checked from Course and keeps courses. The following .code is still checked from Course, not from Boolean.

A Boolean condition may be false for every current value. This is still a well-typed path expression:

u.[false]

The result has the same current type as u, namely University, but reaches no values.

Calculated outputs

A calculated output is checked as an ordinary expression in the current path context. The expression must be well typed. Its result type becomes the type of the output attribute named by the as clause.

u.course.assessment.exam.(durationMinutes/maxMark as minutesPerMark)

Inside the parentheses, durationMinutes and maxMark are both checked from the current exam assessment value. The output attribute minutesPerMark has the result type of the / expression.

Σ gives a Set<T>

When a calculation really needs the set of all values reached by a plural path, use a fold to make that set explicit. In the following example, v.Σ has type Set<Real>, so it can be compared with a set:

x.((if v.Σ ⊆ {1, 2, 3} then 1 else 2) as a)

The condition in the if expression is Boolean-valued because ⊆ compares two sets. This differs from using v directly: v reaches Real values one at a time, while v.Σ collects the reached values into a set.