22 Navigation

The University database

Let u be a program variable of type University. It can be thought of as the database being queried.

University u;

The aim for the chapters in this part is to explain how to write read-only queries on u. The emphasis will be on using examples to illustrate how it works, without delving into the formal denotational semantics.

Path expressions

A path expression is an expression which can appear in Predica programs and in queries:

u.student.name
u.course.[advanced].code
u.course.(code, title)
u.student.name as studentName
u.course.session.time.(day, startMinute)
u.course.let c = this in c.prerequisite.code
u.course.assessment.exam.durationMinutes.Σsum
u.course.[advanced]⇒session.time.day

Path expressions are analogous to relational algebra expressions used to express queries on a relational database.

In our examples path expressions start at u then typically follow attributes through the schema.

Frames

Here we give an informal description of frames and explain the notation used to write them. They underpin the semantics of Predica.

Consider the following set builder notation for the points on the unit circle:

{ (X,Y) ∈ ℝ² | X² + Y² = 1 }

In an analogous way we can use a set builder notation to denote a relation with two attributes code and title which represents a query on the university database:

{ { (code=X:String), (title=T:String) } 
  where ∃C:Course 
        u.course(C) ∧ C.code(X) ∧ C.title(T) }

This is an expression of the form {R where Ψ}.

In this case we are ranging over the variables in R. That is not always the case, the more general form is written {R for F where Ψ}. The following illustrates use of for in a set builder notation:

{ r(X,Y) for X:A,Y:B where p(X,Y) }

In the formal denotational semantics a path expression denotes a frame (R,F,Ψ), i.e. the three components of a set builder notation of an n-ary relation.

It is convenient to write a frame using the notation R for F where Ψ or sometimes just R where Ψ.

For example, the path expression u.student denotes the frame:

student=S:Student where u.student(S)

Navigation

The simplest paths select one kind of object from the university.

u.student
u.course
u.department
u.enrolment

A path is read from left to right. The expression u.student.name starts with the university, reaches its students, and then reaches each student's name.

u.student.name

The same idea works for longer paths. The following expression starts at the university, reaches students, reaches their enrolments, reaches the courses for those enrolments, and finally reaches the course codes.

u.student.enrolment.course.code

This is relational-join-like traversal: the path crosses from students to enrolments to courses by following declared relationships instead of writing the relational joins explicitly.

Paths can move through derived attributes in the same way as stored attributes. Student.enrolled is calculated from Student.enrolment.course, so these two expressions reach the same courses. Path expressions do not need to distinguish between base attributes and derived attributes.

u.student.enrolment.course
u.student.enrolled

A path may reach many values. The expression u.course.session.room reaches the rooms used by course sessions; it is not a single room unless the data and the schema make it single-valued.

u.course.session.room

Navigation can also follow relationships that were written in the reverse direction for convenience. Department.course is derived from Course.department, but it still reads as ordinary navigation from a department to the courses it offers.

u.department.course.code

The important habit is to keep track of the current kind of value at each step. In u.student.enrolment.course.department.name, the path passes through a university, students, enrolments, courses, departments, and finally department names.

u.student.enrolment.course.department.name

For example, the path u.student.enrolment.course.code corresponds to a chain of relationships in logic:

code=X:String
where
  ∃S:Student ∃E:Enrolment ∃C:Course
    u.student(S)
  ∧ S.enrolment(E)
  ∧ E.course(C)
  ∧ C.code(X)

The result attribute is code, bound to X. The variables S, E and C are the intermediate values reached by the path. Each dotted step contributes another predicate, and the intermediate values are existentially quantified. This is why a dotted path should be read as relational navigation, not as ordinary object property access.

Navigation is uniform across type kinds

This is an important unification in Predica, and may be surprising at first. Base and derived attributes of value types, entity types and quotient types, fields of structural types, and attributes of enum types and variant types are all navigated in the same way. Enum and variant attributes are regarded as always present as unary predicates, which is why they can be used in path expressions without conditionals. Their denotations into logic work identically as well.

For example:

u.course.session.time.startMinute
u.course.session.time.day.monday
u.course.assessment.exam.durationMinutes
u.student.enrolled.code

The first path uses attributes of entity and value types. The second uses an enum attribute. The third uses a variant attribute. The fourth uses the derived attribute Student.enrolled. All of these are ordinary path expressions, and their denotations as frames have the same form.