Unifying Function- and Argument-First Bidirectional Type Systems

Abstract

Bidirectional typing mixes type synthesis and type checking into a single process. Existing bidirectional type systems can be classified into two styles based on whether, given a function application, a bidirectional typing algorithm synthesizes the function's type first and typechecks the argument against the synthesized argument type, or it synthesizes the arguments' types first and typechecks the function against the synthesized arguments' types. We call the former _function-first_ and the latter _argument-first_. Not only do the two styles significantly differ in how the type systems and typing algorithms are formalized, but also they lead to incompatible typeabilities, forcing a language designer to select one style and to give up the other's typeabilities. In this paper, we unify the two styles and develop \lang with a new bidirectional type system for higher-rank polymorphism. Key ideas of the unification are twofold. Each function application is annotated with a bit of information to represent whether function- or argument-first typing is used, to allow a language designer (or even a programmer) to switch between the two styles at their discretion. We reformulate the function- and argument-first type systems by using ideas from colored types and boxy types, which can specify which part of a type should be synthesized or used for checking in a flexible manner. We also develop a typing algorithm based on the worklist approach by Zhao et al. The (declarative) type system of $λ^{BH}$ is shown to be sound and to subsume two representative function- and argument-first systems. Our typing algorithm is shown to be sound with respect to the type system of $λ^{BH}$ and complete with respect to representative function- and argument-first systems. We mechanically prove the metatheorems using the Abella theorem prover.