Study of the Subtyping Machine of Nominal Subtyping with Variance
summary
Class fragments of Kennedy and Pierce’s nominal subtyping map to concrete tree-language classes: the lattice of fragments is characterized as non-expansive = regular, no-contravariance = context-free (Greibach) and other restraints yield deterministic or non-deterministic tree languages; undecidability of the full system is reaffirmed via PCP reduction. A working proof-of-concept tool, Treetop generates C# fluent APIs, emits subtyping-machine-based code that enforces context-free protocols at compile time and fails compilation when a protocol is violated.
AI-written summary · about
chapters (10)
- 0:00Overview
- 2:20Variance
- 3:20Decidability of Subtyping (Kennedy and Pierce 2007)
- 4:11Types Are Trees
- 4:39Tree Grammars
- 5:22Subtyping Machines Subtyping programs that recognize tree languages
- 6:43Results
- 11:16Subtyping Metaprogramming
- 12:28Treetop
- 13:35In Conclusion
related talks
21mSeamless Scope-Safe Metaprogramming Through Polymorphic Subtype Inference (Short Paper)
32mTyped Program Analysis Without Encodings
48mA History of Subtyping
15mThe Simple Essence of Algebraic Subtyping: Principal Type Inference with Subtyping Ma...
24mChoice Trees: Representing Nondeterministic, Recursive, and Impure Programs in C...
21mPolymorphic Type Inference for Dynamic Languages
30mComputation-Tree Semantics: An Algorithmic Approach to Structurally Defined Relations
19mExtensible Metatheory Mechanization via Family Polymorphism