Focusing on Refinement Typing

TL;DR

This paper introduces a new refinement typing system for functional programming that uses a focalized call-by-push-value approach, enabling SMT constraint generation without existential variables, and proves its soundness, completeness, and decidability.

Contribution

It develops a logically grounded refinement type system compatible with any computational effect, utilizing focalization and value-determined indexes for efficient SMT constraint solving.

Findings

The system generates solvable SMT constraints without existential variables.

Proves the type system is sound, complete, and decidable.

Establishes type soundness via domain-theoretic semantics.

Abstract

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.