arXiv:2108.06296cs.LO
An ML-style Record Calculus with Extensible Records
Early discovery. Linked by one identifiable commenter. This paper is outside the main ranking; a mention is not an endorsement.
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.
I think what you describe is called "extensible records". Elm had them in a prior version. You can implement them in a language with an expressive enough type system (e.g. Haskell or Scala) without special support, but the syntax can be a bit unwieldy. Here's three recent papers…
noelwelshView on HNParent context