We present a logically principled foundation for systematizing, in a way that works with any computational effect and evaluation order, SMT constraint generation seen in refinement type systems for functional programming languages. By carefully combining a focalized variant of call-by-push-value, bidirectional typing, and our novel technique of value-determined indexes, our system generates solvable SMT constraints without existential (unification) variables. We design a polarized subtyping relation allowing us to prove our logically focused typing algorithm is sound, complete, and decidable. We prove type soundness of our declarative system with respect to an elementary domain-theoretic denotational semantics. Type soundness implies, relatively simply, the total correctness and logical consistency of our system. The relative ease with which we obtain both algorithmic and semantic results ultimately stems from the proof-theoretic technique of focalization.

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 support features for which inference is undecidable; 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.