Polarized Subtyping

TL;DR

This paper develops a semantic and syntactic framework for subtyping in call-by-push-value languages, addressing recursive types, variants, and lazy records with a focus on polarization and observation depth.

Contribution

It introduces a semantic step-indexed model and a bidirectional typing system for subtyping in call-by-push-value, accommodating recursive, variant, and lazy record types.

Findings

Semantic model justifies subtyping rules for recursive types.

Syntactic system effectively handles type inference with subtyping.

Framework applies to call-by-name, call-by-value, and isorecursive types.

Abstract

Polarization of types in call-by-push-value naturally leads to the separation of inductively defined observable values (classified by positive types), and coinductively defined computations (classified by negative types), with adjoint modalities mediating between them. Taking this separation as a starting point, we develop a semantic characterization of typing with step indexing to capture observation depth of recursive computations. This semantics justifies a rich set of subtyping rules for an equirecursive variant of call-by-push-value, including variant and lazy records. We further present a bidirectional syntactic typing system for both values and computations that elegantly and pragmatically circumvents difficulties of type inference in the presence of width and depth subtyping for variant and lazy records. We demonstrate the flexibility of our system by systematically deriving related systems of subtyping for (a) isorecursive types, (b) call-by-name, and (c) call-by-value, all using a structural rather than a nominal interpretation of types.