Focusing on Modular Refinement Typing

Abstract

Refinement typing algorithms are hard to design and understand. Liquid Haskell (LH) has powerful features like modular, recursive refinement of inductive data. But Liquid Haskell is relatively hard to understand as it lacks an explicit phase distinction between indices and programs. Index based systems like Dependent ML (DML) tend toward less power but, enjoying an index-program phase distinction, are easier to understand. We apply techniques from logic, type theory, and category theory to design a correct and simple bidirectional typing algorithm for modular recursive index refinements. We use focusing to design logically a call-by-push-value (CBPV) with algebraic datatypes. CBPV is a language known empirically to have good semantic properties even in the presence of computational effects like nontermination and errors. Bidirectional type theories are a reliable way to combine rich type checking and inference. We prove our declarative system is semantically sound for standard mathematical models (domains). We prove our algorithmic system is decidable, sound, complete. Focusing and bidirectional typing combine elegantly with a new concept: value-determined existentials of input types under focus are guaranteed to be solved at the end of focusing stages, clearly outputting constraints decidable by an SMT solver. We believe this work improves our understanding of liquid refinement typing, and we hope it can guide or serve as the foundation for implementations thereof.