by David Binder, Ingo Skupin, David Läwen, and Klaus Ostermann

In Proceedings of the International Workshop on Type-Driven Development. ACM Press, 2022.

Abstract

Static types are a great form of lightweight static analysis. But sometimes a type like List is too coarse; we would also like to work with its refinements like non-empty lists, or lists containing exactly 42 elements. Dependent types allow for this, but they impose a heavy proof burden on the programmer. We want the checking and inference of refinements to be fully automatic. Existing approaches to refinement types support extensive automation, but they make various trade-offs. In the original system of Freeman and Pfenning, the programmer was required to manually specify all refinements they want to use. We only require the user to specify the original data type, but not its refinements, which are discovered automatically. With liquid refinement types, an external solver is used to solve the proof obligations for the programmer. We only use familiar techniques from constraint-based type inference. The system of Jones and Ramsay is very similar in spirit to our system, but the refinements they allow are less expressive. They support refinements which can be expressed as the removal of a constructor from the definition of a type, but require this removal to be hereditary. So they cannot express the type of non-empty lists which require the removal of the Nil constructor only at the toplevel. We support all refinements that can be expressed as a regular sublanguage of the original type. In this article we present a simple refinement type system and inference algorithm which uses only variants of familiar concepts from constraint-based type inference. Concretely, we build on the algebraic subtyping approach and extend it with typing rules which combine properties of nominal and structural type systems in a novel way. Despite the simplicity of the approach, the resulting type system is very expressive and allows to specify and infer non-trivial properties of programs.