Abstract

Refinement typing algorithms are hard to design and understand. Liquid Haskell has practical and powerful features like modular, recursive refinements of inductive data that are nonetheless guaranteed to generate SMT -decidable typing constraints. But Liquid Haskell is relatively hard to understand because it lacks an explicit phase distinction between indices and programs. Index-based systems like Dependent ML tend to be less practical, especially since they aren’t guaranteed to create SMT -decidable constraints, but are easier to understand due to their index/program phase distinction.

In this talk we discuss how to apply techniques from logic, type theory, and category theory to design a correct and straightforward bidirectional typing algorithm for modular, recursive index refinements. We use focusing to design logically a call-by-push-value (CBPV) system with measures on inductive data. CBPV has good semantic properties even in the presence of computational effects. Bidirectional type systems are a reliable way to combine type checking and inference, with a straightforward initial recipe in sequent calculus. We prove that our declarative system is operationally sound, operationally complete (adequacy), and sound with respect to a standard denotational semantics, all of which taken together imply logical consistency, as well as total correctness both operationally and denotationally. We design an algorithmic system and prove it is decidable, sound, and complete. Focusing and bidirectional typing combine nicely with a new concept that seems to be exploited in liquid type systems: value-determined existential indices of input types under focus are guaranteed to be solvable at the end of focusing, outputting existential-free types and constraints decidable by an SMT solver.