An ML-style Record Calculus with Extensible Records

TL;DR

This paper introduces a new polymorphic record calculus supporting extensible records with a static type system and inference, extending Ohori's calculus with record extension and removal capabilities.

Contribution

It presents a novel construction for an ML-style polymorphic record calculus with extensible records, including a sound and complete type inference algorithm.

Findings

Developed a static type system for extensible records

Extended Ohori's calculus with record addition and removal

Provided a sound and complete type inference algorithm

Abstract

In this work, we develop a polymorphic record calculus with extensible records. Extensible records are records that can have new fields added to them, or preexisting fields removed from them. We also develop a static type system for this calculus and a sound and complete type inference algorithm. Most ML-style polymorphic record calculi that support extensible records are based on row variables. We present an alternative construction based on the polymorphic record calculus developed by Ohori. Ohori based his polymorphic record calculus on the idea of kind restrictions. This allowed him to express polymorphic operations on records such as field selection and modification. With the addition of extensible types, we were able to extend Ohori's original calculus with other powerful operations on records such as field addition and removal.