Structure of the TypeChecker

An object of the class ilog.language.design.types.TypeChecker is a backtracking prover that establishes various kinds of goals. The most common goal kind established by a type checker is a typing goal--but there are others.^4.2 A TypingGoal object is a pair consisting of an expression and a type. Proving a typing goal amounts to unifying its expression component's type with its type component. Such goals are spawned by the type checking method of expressions as per their type checking rules. Some globally defined symbols having multiple types, it is necessary to keep choices of these and backtrack to alternative types upon failure. Thus, a TypeChecker object maintains all the necessary structures for undoing the effects that happened since the last choice point. These effects are:

1. type variable binding,
2. function type currying,^4.3
3. application expression currying.

In addition, it is also necessary to remember all Goal objects that were proven since the last choice point in order to prove them anew upon backtracking to an alternative choice. This is necessary because the goals are spawned by calls to the typeCheck method of expressions that may be exited long before a failure occurs. Then, all the original typing goals that were spawned in the mean time since the current choice point's goal must be reestablished. In order for this to work, any choice points that were associated to these original goals must also be recovered. To enable this, when a choice point is created for a Global symbol, choices are linked in the reverse order (i.e., ending in the original goal) to enable reinstating all choices that were tried for this goal.

In order to coordinate type proving, a typechecker object is passed to all type checking and unification methods as an argument in order to record any effect in the appropriate trail.

To recapitulate, the structures of a TypeChecker object are:

• a goal stack containing goal objects (e.g., TypingGoal) that are yet to be proven;
• a binding trail stack containing type variables and boxing masks to reset to "unbound" upon backtracking;
• a function type currying trail containing 4-tuples of the form (function type, previous domains, previous range, previous boxing mask) for resetting the function type to the recorded domains, range, and mask upon backtracking;
• an application currying trail containing triples of the form (application type, previous function, previous arguments) for resetting the application to the recorded function and arguments upon backtracking;
• a goal trail containing TypingGoal objects that have been proven since the last choice point, and must be reproven upon backtracking;
• a choice-point stack whose entries consists of:
  • a queue of TypingGoalEntry objects wherefrom to constructs new TypingGoal objects to try upon failure;
  • pointers to all trails up to which to undo effects.