Extensible Datasort Refinements

TL;DR

This paper introduces an extension to datasort refinement type systems that enables re-refinement through signature extension, supporting independent, modular type checking without requiring code duplication.

Contribution

It proposes a novel signature extension mechanism for datasort refinements, maintaining inversion principles and enabling separate compilation.

Findings

Supports re-refinement without duplicating type definitions

Ensures well-formedness of extended signatures

Allows independent, modular type checking

Abstract

Refinement types turn typechecking into lightweight verification. The classic form of refinement type is the datasort refinement, in which datasorts identify subclasses of inductive datatypes. Existing type systems for datasort refinements require that all the refinements of a type be specified when the type is declared; multiple refinements of the same type can be obtained only by duplicating type definitions, and consequently, duplicating code. We enrich the traditional notion of a signature, which describes the inhabitants of datasorts, to allow re-refinement via signature extension, without duplicating definitions. Since arbitrary updates to a signature can invalidate the inversion principles used to check case expressions, we develop a definition of signature well-formedness that ensures that extensions maintain existing inversion principles. This definition allows different parts of a program to extend the same signature in different ways, without conflicting with each other. Each part can be type-checked independently, allowing separate compilation.