Along with J. Dunfield, I have written a new survey paper on bidirectional typechecking.
Bidirectional typing combines two modes of typing: type checking, which checks that a program satisfies a known type, and type synthesis, which determines a type from the program. Using checking enables bidirectional typing to break the decidability barrier of Damas-Milner approaches; using synthesis enables bidirectional typing to avoid the large annotation burden of explicitly typed languages. In addition, bidirectional typing improves error locality. We highlight the design principles that underlie bidirectional type systems, survey the development of bidirectional typing from the prehistoric period before Pierce and Turner's local type inference to the present day, and provide guidance for future investigations.
This is the first survey paper I've tried to write, and an interesting thing about the process is that it forces you to organize your thinking, and that can lead to you changing your mind. For example, before we started this paper I was convinced that bidirectional typechecking was obviously a manifestation of focalization. When we attempted to make this argument clearly in the survey, that led me to realize I didn't believe it! Now I think that the essence of bidirectional typechecking arises from paying close attention to the mode discipline (in the logic programming sense) of the typechecking relations.
Also, if you think we have overlooked some papers on the subject, please let us know. Bidirectional typechecking is a piece of implementation folklore that is perhaps over three decades old, which makes it very hard for us to feel any certainty about having found all the relevant literature.
When writing code (albeit just toys), I've found it more pleasant to have a single `checkInfer :: Term -> Maybe Type -> Maybe Type` function rather than the usual `check :: Term -> Type -> Bool` and `infer :: Term -> Maybe Type` pair. This allows for both checking and synthesis modes for lets and case-splits without duplicating any code: they can just pass the `Maybe Type` (being the expected type, when we know it) through to the appropriate recursive call directly without even inspecting it. I was hoping to see some discussion of how this fits into the picture -- I suppose you could do the analogous thing at the level of typing judgments as well?
ReplyDeleteThis is very nice, thanks for writing it. I was a bit confused by the remark in section 4.5.2 that "for each type assignment rule, the recipe produces exactly one rule," when in section 4.1 you had explained that a case-statement naturally comes with two bidirectional rules. Is the former remark intended to apply only to the STLC system without sum types?
ReplyDeleteI was extremely fascinated by the appearance of linear logic in sections 6.2 and 6.5. I need to read up about directional logic programming; it seems like it might be a way for a category theorist to finally make sense of logic programming. (-:O Perhaps by interpreting those classical-linear types of the sorts in a Chu construction? Are there references other than Reddy [1993] that I should be reading?
In section 6.5 it wasn't clear to me why this "backwards" bidirectional typing only works for linear type theory. What goes wrong in the nonlinear case? Also, this idea of the type of each variable in the context being an output rather than an input reminds me of the way that contexts are constructed by "joins" in Andromeda (http://www.andromeda-prover.org/v1/type-theory.html); is it related?
The original Pfenning recipe for sums yields only one bidirectional rule: you synthesize a type for the scrutinee, and check the bodies of the branches. In section 4.1, we note that the other one is valid, too -- this is sort of the first hint that there are more possibilities than just the Pfenning recipe.
ReplyDeleteUday remarks in his directional logic programming paper that he was inspired by Abramsky's 1994 paper "Proofs as Processes". As a result, I expect the semantic intuition for process types at play here to be most closely connected to the Int construction of Joyal, Street and Verity.
Basically, you can form a traced monoidal category where the objects are sets and the morphisms S : I → O are transducers or Mealy machines. That is, a Mealy machine is a (small) set S, an initial state s ∈ S, and a (partial) transition function I × S → O × S, representing a state machine which takes in a stream of inputs drawn from I and emits a stream of outputs drawn from O. These machines are then equated up to bisimulation. (Abramsky's "Retracing Some Paths in Process Algebra" works out the construction in detail.)
The Int construction then gives you a new (star-autonomous, if memory serves) category where the types are pairs (X+, Y-) describing an interface with both outputs X+ and inputs Y-. Then negation flips the input and output, and then (likely with some additional conditions) you could get initial algebras and final coalgebras for polynomial functors, which would interpret the sorts.
Thanks! The Int-construction actually gives you a compact closed category, with a resulting degenerate sort of linear logic in which tensor=par. So I'd be a little surprised if it's the right thing, but of course I don't know anything about this stuff yet. The idea of "the types are pairs (X+, Y-) describing an interface with both outputs X+ and inputs Y-, where negation flips the input and output" of course also applies to the Chu construction, although the precise relationship between the two is a bit unclear (e.g. https://mathoverflow.net/q/284152/49).
DeleteCan you say anything about why backwards bidirectional typing fails in the nonlinear case?
It's not at all clear to me whether Int(C) ever has finite products and coproducts, so as to model the additive operations of linear logic. So I don't even know what it would mean for it to have a list object LA such that LA = 1 ⊕ (A ⊗ LA) as in Reddy's paper.
DeleteThe Chu construction does inherit finite products and coproducts from the original category; but at the moment I can't see such a list object existing there. (Since Chu constructions are almost never locally presentable categories, the usual methods of constructing initial algebras of polynomial functors don't apply.)
I guess one compact closed category in which such a fixed-point exists is Rel, since ⊗ and ⊕ in Rel coincide with the categorical product and coproduct, respectively, in Set, where LA is actually an initial algebra. And on reading Reddy's paper more closely I see that the compact-closed degeneration of tensor=par and plus=with is in fact what we have in mind semantically -- perhaps one might even say that Rel is the/an intended semantics -- with the *-autonomous discipline a syntactic way of keeping track of modes. But it would still be more satisfying to have a *-autonomous, non-compact-closed, category that can give "semantics to the modes" in some nontrivial way.
DeleteYou may have already seen this, but David Christiansen's tutorial is the most straightforward introduction to bidirectional typing that I have seen.
ReplyDeletehttp://www.davidchristiansen.dk/tutorials/bidirectional.pdf