Polymorphic Records for Dynamic Languages
arxiv(2024)
摘要
We define and study "row polymorphism" for a type system with set-theoretic
types, specifically union, intersection, and negation types. We consider record
types that embed row variables and define a subtyping relation by interpreting
types into sets of record values and by defining subtyping as the containment
of interpretations. We define a functional calculus equipped with operations
for field extension, selection, and deletion, its operational semantics, and a
type system that we prove to be sound. We provide algorithms for deciding the
typing and subtyping relations.
This research is motivated by the current trend of defining static type
system for dynamic languages and, in our case, by an ongoing effort of endowing
the Elixir programming language with a gradual type system.
更多查看译文
AI 理解论文
溯源树
样例
生成溯源树,研究论文发展脉络
Chat Paper
正在生成论文摘要