Study of the Subtyping Machine of Nominal Subtyping with Variance (full version)

TL;DR

This paper analyzes the computational capabilities of the subtyping machine in Kennedy and Pierce's nominal subtyping with variance, characterizes its power using formal language theory, and introduces Treetop, a tool for generating C# subtyping implementations.

Contribution

It provides a formal characterization of the subtyping machine’s computational power and presents Treetop, the first tool to generate C# code for context-free API protocols in a decidable type system.

Findings

The subtyping machine's power ranges from regular to non-deterministic tree languages.

Treetop enables automated generation of C# subtyping implementations.

The approach supports context-free API protocols within a decidable fragment.

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.