Gradual Typing for Extensibility by Rows
This work studies gradual typing for row types and row polymorphism. Key ingredients in this work are the \emph{dynamic row type}, which represents a statically unknown part of a row, and \emph{consistency for row types}, which allows injecting static row types into the dynamic row type and, conversely, projecting the dynamic row type to any static row type. While consistency captures the behavior of the dynamic row type statically, it makes the semantics of a gradually typed language incoherent when combined with row equivalence which identifies row types up to field reordering. To solve this problem, we develop \emph{consistent equivalence}, which characterizes composition of consistency and row equivalence. Using consistent equivalence, we propose a polymorphic blame calculus $\text{F}^\rho_\text{C}$ for row types and row polymorphism. In $\text{F}^\rho_\text{C}$, casts perform not only run-time checking with the dynamic row type but also field reordering in row types. To simplify our technical development for row polymorphism, we adopt \emph{scoped} labels, which are employed by the language Koka and are also emerging in the context of effect systems. We give the formal definition of $\text{F}^\rho_\text{C}$ with these technical developments and prove its type soundness. We also sketch the gradually typed surface language $\text{F}^\rho_\text{G}$ and type-preserving translation from $\text{F}^\rho_\text{G}$ to $\text{F}^\rho_\text{C}$ and discuss conservativity of $\text{F}^\rho_\text{G}$ over typing of a statically typed language with row types and row polymorphism.
Sat 25 JanDisplayed time zone: Saskatchewan, Central America change
10:30 - 12:30 | |||
10:30 30mTalk | Gradual Algebraic Data Types WGT Michael Greenberg Pomona College, Stefan Malewski University of Santiago de Chile, Éric Tanter University of Chile Pre-print File Attached | ||
11:00 30mTalk | Gradual Typing for Extensibility by Rows WGT Pre-print | ||
11:30 30mTalk | Foreign Function Typing: Semantic Type Soundness for FFIs WGT Pre-print | ||
12:00 30mTalk | Space-Efficient Monotonic References WGT Pre-print |