Polymorphic Record Types for Dynamic Languages

Core Concepts

This work defines and studies a first-order polymorphic type system with row polymorphism and set-theoretic types, including union, intersection, and negation types. It provides a semantic interpretation of types, a decidable subtyping relation, and algorithms for typing and subtyping.

Abstract

The content presents the following key points:

Motivation: There is a growing effort to develop type systems for dynamic languages, which often include union and intersection types. Some dynamic languages, such as Luau and Elixir, have adopted set-theoretic types as defined in the semantic subtyping framework. The authors aim to study adding row polymorphism to such type systems.

Need for row polymorphism: The authors argue that the current approaches to row polymorphism cannot be directly reused in the presence of set-theoretic types, and an original theory must be developed. They provide examples to illustrate the limitations of using only intersection types and type variables to capture the behavior of record operations.

Type system definition: The authors define the syntax of types, including record types that can be closed, open, or specify a row variable. They provide a set-theoretic interpretation of types and define the subtyping relation as containment of interpretations.

Subtyping algorithm: The authors define an algorithm to decide the subtyping relation, extending the subtyping algorithm of the CDuce language to handle polymorphic record types.

Language with record operations: The authors define a language with record extension, selection, and deletion operations, provide an operational semantics and a declarative type system, and prove the type system to be sound.

Tallying problem: The authors tackle the tallying problem, which is the problem of deciding whether there exists a type substitution that makes one type a subtype of another. They define a tallying algorithm for row polymorphic types and prove its soundness, but not its completeness.

The authors conclude by discussing related work and future research directions.

Stats

None.

Quotes

None.

Key Insights Distilled From

Polymorphic Records for Dynamic Languages

by Gius... at arxiv.org 04-02-2024

https://arxiv.org/pdf/2404.00338.pdf

Deeper Inquiries

Question 1

To extend the proposed type system to support first-class labels, which are commonly used in dynamic languages, we can introduce a new syntactic category for labels. This category would allow labels to be computed and manipulated as values during the program execution. By incorporating first-class labels, the type system can provide more flexibility and expressiveness in handling record operations. Additionally, the interpretation domain can be expanded to include labels as part of the domain elements, enabling the type system to interpret and reason about labels dynamically. This extension would involve updating the syntax of types to include label variables and modifying the interpretation rules to accommodate the dynamic nature of labels within the type system.

Question 2

The current tallying algorithm in the context of the proposed type system is sound but not complete. One limitation is that the algorithm does not guarantee completeness in all cases, particularly when dealing with row variables that are expanded into Boolean combinations of rows. To improve the completeness of the tallying algorithm, one approach could be to refine the algorithm to handle the expansion of row variables more effectively. This could involve developing a more sophisticated algorithm that can accurately determine the appropriate substitutions for row variables to achieve completeness in type inference. By enhancing the algorithm's handling of row variables and their substitutions, the completeness of the tallying process can be improved.

Question 3

The research on polymorphic records and set-theoretic types has broader implications beyond the Elixir programming language. This work can benefit other dynamic languages that utilize set-theoretic types by providing a foundation for incorporating row polymorphism and advanced type systems. Some potential applications of this research include enhancing type inference and type checking capabilities in dynamic languages, enabling more precise and flexible typing of data structures and functions. Additionally, the concepts and algorithms developed in this work can be applied to other programming languages seeking to integrate static type systems with dynamic language features, facilitating the development of more robust and reliable software systems. The insights from this research can contribute to the advancement of type systems in various programming paradigms, leading to improved code quality, maintainability, and developer productivity.