Under the Hood: Type Inference

The core of the type inference functionality is found in the TypeInferenceTransformer.groovy class. The main steps of the algorithm are the following

1. Gather all explicit type information from declarations of relations and types

2. Validate rules multiple times, until no rules are left to validate in the current iteration. If the rule set for validation does not change between two subsequent iterations report and error. For each rule do the following steps

3. 1. Relations in the rule head that also have an explicit declaration are marked for validation

   2. Relations in the rule head without an explicit declaration are marked for type inference

   3. Relations in the rule body are marked for validation

   4. For each relation in the rule body, if there is inferred type information, associate the appropriate type to each expression used in the relation. E.g. if relation P(x, y) is inferred to have types int and string, associate x with int and y with string

   5. For unary or binary expressions, validate that they have valid types. E.g. both expressions in a multiplication have to be of some numerical type (int or real)

   6. Operator = has dual semantics. If a side is a variable and that variable is not bound in the body by a relation, then it's treated as an assignment (and is associated with the inferred type of the other side). Otherwise, it is treated as an equality check and expressions from both sides are validated for compatibility

   7. Operator + has dual semantics as well. Either, as a string concatenation when at least on operand is of type string, or otherwise, as normal addition

4. During type inference of relations in the rule head, if a relation is still missing type information, the rule is marked for revisit in the next iteration of (2). If a relation has an update to its type information, then all rules that depend on that relation (i.e., refer to it in their bodies) are marked for revisit in the next iteration

5. During validation of relations, if a relation had some previous inferred types, then the expressions used in the relation in the current rule have to be subtypes of those inferred types

Meet and Join Operations

• meet(type1, type2): For inferring a type in a rule body, approximate by assuming all relations are used conjunctively. Therefore, infer the lowest type in the hierarchy (type-lattice) that is present. Since there is no multiple subtyping, either one of the types must be the lowest one

E.g., if the first parameter of relation is typed as Cat, and it used in P(x) with x being of type PersianCat, then meet returns PersianCat. Is x is of type Dog then an error is reported

• join(type1, type2): For inferring a type among different rules of the same relation, treat them as a disjunction. Therefore, infer the lowest, higher common type in the hierarchy (type-lattice). Traverse the type hierarchy from the top and stop at the first branching point

E.g., if relation Q is used in a rule that infers PersianCat as the type of the first parameter, and in another rule that infers Dog as the type of the first parameter, then join returns Animal