Towards Algebraic Subtyping for Extensible Records

TL;DR

This paper extends the MLsub language with support for extensible records by introducing row variables, enabling adding new fields to records while maintaining efficient and decidable type inference.

Contribution

It introduces row variables into Simple-sub, allowing extensible records in MLsub with a modified type inference algorithm that remains decidable.

Findings

Successfully extended Simple-sub with extensible records

Maintained decidability of type inference

Enabled adding fields to records dynamically

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.