ICFP 2022
Sun 11 - Fri 16 September 2022 Ljubljana, Slovenia
Sun 11 Sep 2022 10:12 - 10:30 at Club CD - TyDe 1 Chair(s): Hsiang-Shang ‘Josh’ Ko

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.

Sun 11 Sep

Displayed time zone: Belgrade, Bratislava, Budapest, Ljubljana, Prague change

09:00 - 10:30
TyDe 1TyDe at Club CD
Chair(s): Hsiang-Shang ‘Josh’ Ko Institute of Information Science, Academia Sinica
09:00
18m
Full-paper
A Hoare-Logic Style Refinement Types FormalisationVirtual
TyDe
Zilin Chen UNSW Sydney
Link to publication DOI
09:18
18m
Full-paper
Computing with Generic Trees in Agda
TyDe
09:36
18m
Short-paper
Contextual Algebraic Theories: Generic Boilerplate beyond Abstraction (Extended Abstract)
TyDe
Andreas Nuyts KU Leuven, Belgium
Link to publication
09:54
18m
Short-paper
Provingly Correct Optimisations on Intrinsically Typed Expressions (Extended Abstract)
TyDe
Matthias Heinzel Utrecht University
Pre-print
10:12
18m
Full-paper
Structural Refinement Types
TyDe
David Binder University of Tübingen, Ingo Skupin University of Tübingen, David Läwen University of Tübingen, Germany, Klaus Ostermann University of Tübingen
Pre-print