A Theory of Higher-Order Subtyping with Type Intervals (Extended Version)
Abstract
The calculus of Dependent Object Types (DOT) has enabled a more principled and robust implementation of Scala, but its support for type-level computation has proven insufficient. As a remedy, we propose , a rigorous theoretical foundation for Scala's higher-kinded types. extends with interval kinds, which afford a unified treatment of important type- and kind-level abstraction mechanisms found in Scala, such as bounded quantification, bounded operator abstractions, translucent type definitions and first-class subtyping constraints. The result is a flexible and general theory of higher-order subtyping. We prove type and kind safety of , as well as weak normalization of types and undecidability of subtyping. All our proofs are mechanized in Agda using a fully syntactic approach based on hereditary substitution.
Keywords
Cite
@article{arxiv.2107.01883,
title = {A Theory of Higher-Order Subtyping with Type Intervals (Extended Version)},
author = {Sandro Stucki and Paolo G. Giarrusso},
journal= {arXiv preprint arXiv:2107.01883},
year = {2021}
}
Comments
73 pages; to be presented at the 26th ACM SIGPLAN International Conference on Functional Programming (ICFP 2021), 22-27 August 2021