Semantically Separating Nominal Wyvern for Usability and Decidability

TL;DR

This paper introduces Nominal Wyvern, a dependent type system that separates semantic and structural aspects to maintain subtype decidability while preserving expressiveness and usability in object-oriented and functional paradigms.

Contribution

It proposes a novel semantic separation approach in a DOT-like system to ensure subtype decidability without losing expressiveness.

Findings

Achieves subtype decidability through semantic separation.

Maintains expressiveness of F-bounded polymorphism and modules.

Provides a familiar syntax for object-oriented users.

Abstract

The Dependent Object Types (DOT) calculus incorporates concepts from functional languages (e.g. modules) with traditional object-oriented features (e.g. objects, subtyping) to achieve greater expressivity (e.g. F-bounded polymorphism). However, this merger of paradigms comes at the cost of subtype decidability. Recent work on bringing decidability to DOT has either sacrificed expressiveness or ease of use. The unrestricted construction of recursive types and type bounds has made subtype decidability a much harder problem than in traditional object-oriented programming. Recognizing this, our paper introduces Nominal Wyvern, a DOT-like dependent type system that takes an alternative approach: instead of having a uniform structural syntax like DOT, Nominal Wyvern is designed around a "semantic separation" between the nominal declaration of recursive types on the one hand, and the structural refinement of those types when they are used on the other. This design naturally guides the user to avoid writing undecidably recursive structural types. From a technical standpoint, this separation also makes guaranteeing decidability possible by allowing for an intuitive adaptation of material/shape separation, a technique for achieving subtype decidability by separating types responsible for subtyping constraints from types that represent concrete data. The result is a type system with syntax and structure familiar to OOP users that achieves decidability without compromising the expressiveness of F-bounded polymorphism and module systems as they are used in practice.