Focusing on Modular Refinement Typing

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.

Department dc:contributor.department

Computing

Year dc:date.issued

2024

Author dc:creator

• Economou, Dimitrios James

Advisor dc:contributor.supervisor

• Dunfield, Jana

• Type refinement

Statement dc:rights

• Attribution-NonCommercial-ShareAlike 4.0 International

Licence dc:rights.uri

• http://creativecommons.org/licenses/by-nc-sa/4.0/

Language dc:language.iso

eng

Handle dc:identifier.uri

https://hdl.handle.net/1974/33497

OAI identifier oai:identifier

oai:queensu.scholaris.ca:1974/33497