View article

2 BACKGROUND AND STATE OF THE ART We revisit modern methods to implement TC in Sect. 2. 1 and briefly discuss background on the verification of monadic code in Sect. 2.2.

2.1 Implementation Traditional TC algorithms, like algorithms J and W [7] or Morris’ algorithm [8], solve equality constraints as they come up. An important realization, first described by Wand [16], is that TC can be split into two distinct phases. During the first phase (a), the algorithm generates constraints for the entire input program without solving them. Afterwards, in the second phase (b), these constraints are submitted to a solver to produce an output. This phase-separated approach facilitates the re-use of a constraint language and its solver for different object languages and type systems. Central to type inference for many languages is the notion of unification variables (uvars): placeholders for yet unknown types, which a unifier will replace with concrete types during constraint solving. These become necessary when not all type inputs are available for a recursive call, eg the type of a let-bound program variable. During the generation of constraints, these uvars correspond to an existential quantification of a type. Another ubiquitous constraint is equality, eg in a function application the type of the domain of the function must be equal (during solving this means unifiable) with the type of the passed argument. More complex type systems may require more forms of constraints, eg subtyping, which we do not cover here. Practical implementations also perform elaboration, a distinct third phase (c) that performs a compilation or desugaring step during TC that is usually type …