Towards Algebraic Subtyping for Extensible Records

TL;DR

This work addresses type inference for extensible records in an ML-like language by extending Simple-sub with row variables and constraint-based solving. The authors present a revised type system and inference algorithm that support record extension while preserving decidability and principal types, integrating row polymorphism with algebraic subtyping. A prototype implementation and a GitHub repository are provided, and the paper outlines ongoing plans for formal proofs of soundness and completeness. The approach enables safer, more expressive extensible records in ML-style languages and informs the integration of row variables into algebraic-subtyping frameworks.

Abstract

MLsub is a minimal language with a type system combining subtyping and parametric polymorphism and a type inference algorithm which infers compact principal types. Simple-sub is an alternative inference algorithm which can be implemented efficiently and is easier to understand. MLsub supports explicitly typed records which are not extensible. Here we extend Simple-sub with extensible records, meaning that we can add new fields to a previously defined record. For this we add row variables to our type language and extend the type constraint solving method of our type inference algorithm accordingly, keeping the decidability of type inference.

Figures (1)

• Figure 1: Tracing of the type inference example