Study of the subtyping machine of nominal subtyping with variance
Ori Roth
Abstract
This is a study of the computing power of the subtyping machine behind Kennedy and Pierce's nominal subtyping with variance. We depict the lattice of fragments of Kennedy and Pierce's type system and characterize their computing power in terms of regular, context-free, deterministic, and non-deterministic tree languages. Based on the theory, we present Treetop---a generator of C# implementations of subtyping machines. The software artifact constitutes the first feasible (yet POC) fluent API generator to support context-free API protocols in a decidable type system fragment.
Ask about this paper
Your agent reads all of it.
Lune indexed this paper to the last equation, along with the top-tier papers that cite it. Ask a question and the answer quotes them.
Your agent calls
Luneget_paper_fulltext
Free to start. No credit card required.
Terminal
Install the CLIlune papers fulltext 2ad043d2-0398-4eb9-ba55-41bf8654c766Related papers
- Parametric Subtyping for Structural Parametric PolymorphismHenry DeYoung, Andreia Mordido, Frank Pfenning, Ankush DasPOPL 2024 · 3 citations
- Recursive Subtyping for AllLitao Zhou, Yaoda Zhou, Bruno C. d. S. OliveiraPOPL 2023 · 8 citations
- Local Contextual Type InferenceXu Xue, Chen Cui, Shengyi Jiang, Bruno C. d. S. OliveiraPOPL 2026
- MLstruct: principal type inference in a Boolean algebra of structural typesLionel Parreaux, Chun Yin ChauOOPSLA 2022 · 31 citations
- Decidable subtyping for path dependent typesJulian Mackay, Alex Potanin, Jonathan Aldrich, Lindsay GrovesPOPL 2020 · 13 citations
