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.
翻译:在这项工作中,我们开发了一个带有可扩展记录的多形态记录微积分。可扩展记录是能够添加新字段或从中移除先前存在的字段的记录。我们还开发了这种微积分的静态类型系统和一种健全和完整的推断算法。大多数支持可扩展记录的ML型多形态记录微积分都以行变量为基础。我们根据由Ohoori开发的多形态记录微积分提出了一种替代结构。Ohoori以其多形态记录微积分为基础,以种类限制的概念为基础。这使他得以在诸如实地选择和修改等记录上表达多形态操作。加上了可扩展的类型,我们得以将奥霍里原有的微微积分与诸如外地添加和删除等记录上的其他强大动作相扩展。