Chapter 19. Typing

LogiQL programs are type checked. The compiler determines a type for every argument of every predicate, every variable and expression. These types are used by the compiler to verify that the types are used consistently, thus helping programmers to avoid making certain kinds of mistakes. Types are also used by the runtime system for performance optimizations.

19.1. Predicate Type Inference

Every predicate that is used in a program must have either a predicate type declaration or at least one rule from which the compiler can infer its type. If the program includes type declarations for a predicate, then those type declarations must specify a type for each argument to the predicate.

For any predicate that has no type declaration, a type will be inferred for it from rules that use that predicate in their right-hand side. Predicate type inference attempts to choose the most specific type for the predicate that will allow the program to be correctly typed. This attempt often succeeds, but not always, and even if it succeeds, it might choose types other than the ones you intended. If you want to be certain, then supply a type declaration.

Example 19.1. 

In the following program, the declaration of predicate parentof specifies each argument to be a person (an entity type). Predicate ancestorof does not have a type declaration, so its type is inferred from the rules. The inferred type in this case is that ancestorof has two arguments, each of which is also a person.

person(x) -> .
parentof(x, y) -> person(x), person(y).

ancestorof(x, y) <- parentof(x, y).
ancestorof(x, z) <- ancestorof(x, y), parentof(y, z).

19.2. Type checking

Once the compiler has determined the entity types and has determined the types of all predicates, it uses those types to apply a variety of checks for common errors in the program's rules and constraints.

One kind of check is type consistency. If a variable appears more than once in a formula, then the types associated with those variable occurrences must bear a subtyping relationship.

Example 19.2. 

In this example, variable b is used both as a person and as an integer. These types are not in a subtyping relationship, so the code has a type consistency error.

person(x) -> .
parentof(x, y) -> person(x), person(y).
likes_number(x, y) -> person(x), int(y).

p(a) <- parentof(a, b), likes_number(a, b). // Type consistency error

Another check the system performs is that the head of a rule (and therefore the tuples generated by the rule) will not violate the type of the head's predicate.

Example 19.3. 

In this example there is an attempt to assert that each each instantiation of variable a is a mother. However, the programmer accidentally mixed up the variables in the body of the rule. Since the motherof predicate is declared to have only females in its first argument, the code has a TYPE_TOO_BIG error.

person(x) -> .
female(x) -> person(x).
parentof(x, y) -> person(x), person(y).
motherof(x, y) -> female(x), person(y).

motherof(a, b) <- parentof(a, b), female(b). // TYPE_TOO_BIG error

This last example illustrates that the compiler's type checking is approximate. The programmer may ensure that all possible values for variable a correspond to females, in which case the program is technically type correct. However, the compiler has no way of knowing this, so it makes a conservative guess that a violation might possibly occur. In this way it can guarantee that all compiled programs are type correct, even if some type correct programs do not compile.