19 Inference
So far in PLFA we have essentially computed types by hand. It’s natural to ask if this can be automated, especially after seeing most of it done with refining in Agda (and the rest pretty obvious). The identity function \(\la x . x\) does not have a unique type in the type system we have been working with, so there are further questions about metrics for "a good answer" or "the best answer".
19.1 Inference rules as algorithms
To motivate the topic, PLFA starts with a minimal version of STLC (cut back from the presentation in Lambda to just variables, abstractions, and applications) in which the variable on each lambda is annotated with a type. (This is how STLC is first presented in TaPL.) This suffices to determine the type of any term (or to conclude that it cannot be typed). This isn’t obvious (we are used to also seeing result type annotations in languages such as C or Java). But it’s not hard to figure out the typing rules, and they suggest an algorithm that is structurally recursive in the term being typed.
19.2 Synthesizing and inheriting types
The algorithm of the previous section infers the type of a term. Without the annotations, our previous algorithms checked the provided type of a term. Can we make do with fewer annotations, perhaps with a mix of these two strategies? That is the subject of this chapter, which has become known as bidirectional typing, after the two directional arrows used to differentiate the two possibilities above. The approach arose informally in practice, and only later did researchers provide theoretical underpinnings. A detailed overview can be found in the recent survey paper by Dunfield and Krishnaswami (draft available on arXiv).
PLFA uses an up arrow for inference or synthesis, and a down arrow for checking or inheritance. This is consistent with earlier papers, but more recent work uses right and left arrows, which are easier to remember. One possible mnemonic is that synthesis is a loftier, more aspirational goal than inheritance.
Going back to the minimal STLC, it seems clear that the type of a lambda (without an annotation on its variable) cannot be synthesized; it must be inherited. On the other hand, the type of a variable can be synthesized, because we can just look it up in the context kept during typechecking. What about an application? If we synthesize the type of the term in function position, we can then confirm that the term in argument position inherits the domain of that function type, and together these synthesize the type of the application (the range of the function type).
We could also do it the other way around, which highlights an issue with formalizing bidirectional typing: there are a lot of possible choices. PLFA follows a recipe developed by Dunfield and Pfenning to regularize the process and improve desirable characteristics of the result. In this recipe, constructors are typed using inheritance (as with lambda) and the principal term of a destructor is typed using synthesis (as with the function term of an application) while side terms are typed using inheritance (as with the argument term of an application).
The recipe makes deriving the rest of the rules (for naturals and fixpoint) straightforward. In putting a term together, there may be points where there is a mismatch: a subterm needs to be synthesized, but it requires inheritance, or the other way around. In the first case, a type annotation is required; in the second case, since synthesis is a stronger requirement than inheritance, we can simply forget that we have more than we need.
The resulting rules may seem a little odd in places. The constructor zero is typed using inheritance, but we know perfectly well how to synthesize its type! In practice this is not an issue, since a top-level annotation (such as the type signature which forms part of an Agda definition) can usually provide what is needed for subterms. A term which is a destructor applied to a constructor will not be able to be typed, but such a term can be simplified. There are legitimate reasons to write such a term: the implementation of let using lambda in More, for example. This can be handled by leaving let in place during typechecking, but rewriting it for evaluation, since types play no role in evaluation.
When we formalize bidirectional typing in Agda, we want to write a function that, say, consumes a term and produces its synthesized type. But this function is partial. The way PLFA deals with this is to abandon a single Term datatype and instead introduce two datatypes Term⁺ (synthesized) and Term⁻ (inherited). The synthesize function is still not total, since a value of type Term⁺ could be well-formed but ill-typed. But we can write a decision procedure and have something valid to provide for "no" instances.
The alternative is to write a Synth datatype indexed by Term that provides evidence that a term meets the criteria for synthesis (though it may still be ill-typed). I have added some material to the end of 747Inference that explores this option. The mutually-recursive definitions of Term⁺ and Term⁻ include a down arrow for annotation and an up arrow for "forgetting synthesis". In the examples in this chapter, you will see that the up arrows are more intrusive than one might like, providing further motivation for the alternative representation.
The design of the datatypes Term⁺ and Term⁻ follows the recipe described above and in the informal first section to the Inference chapter. It uses named variables as in Lambda, rather than inherently-typed terms as in DeBruijn. Given the recipe and informal description, the typing rules are mostly a straightforward adaptation of the ones in Lambda. There is one major change from PLFA in the local file: I have included from 747Lambda the "smart constructor" S′ for lookup judgments that hides string inequality proofs using the proof reflection technique from 747Decidable. Previously S′ was used in type judgments that we wrote by hand, so it could just be a function that used S in its implementation. But we want Agda to use it in computing types here, so it has to be an actual constructor. I have put in the smart definition and dropped the prime on the name.
The resulting savings in 747Lambda was minor; here it is considerable. The reason is that Agda’s decision procedure for strings converts the string to a list of characters, then compares the characters pointwise. Character comparison is done by converting the character to a natural number and then using the decision procedure for natural numbers. You can see how long a "no" answer gets, even for the single-character identifiers we are using, by evaluating "x" ≟ "y". If we are converting to the inherently-typed representation in DeBruijn, as is done later in Inference, these parts of the proof go away. But we still have to look at them for debugging and unit testing.
19.3 Soundness and completeness
The goal of the chapter is the mutually-recursive decision procedures synthesize and inherit. inherit consumes a Context, a Term⁻, and a Type, and produces either a typing judgment or a reason why the term cannot have that type. The helper functions that precede these two in the code are all needed in the construction of evidence for "no" instances. synthesize consumes a Context and a Term⁺, and produces either a type and associated typing judgement (these are wrapped up using ∃ syntax) or a reason why the type cannot be synthesized. The code for both of these is structurally recursive on the term.
The exercises I have added at the end bring the Agda development closer to the literature, by using plain terms in the style of Lambda together with type annotation, and Synth/Inherit datatypes as described earlier. You have to write decision functions for these, decorate functions which take plain terms together with appropriate evidence to Term⁺ and Term⁻ respectively, and finally toTerm functions which compute and hide the evidence using the proof by reflection ideas.
We could keep going, rewrite the synthesize and inherit functions to work on plain terms, and get rid of Term⁺ and Term⁻ entirely. That would bring us closer to how bidirectional typing is used in practice, and is reminiscent of the earlier decision to use natural binary notation and deal with the complications of canonicity. But the choice PLFA makes in this chapter to use a less natural notation for terms to which bidirectional typing will be applied helps the reader understand the concepts involved.