Semantically Separating Nominal Wyvern for Usability and Decidability
Yu Xiang Zhu, Amos Robinson, Sophia Roshal, Timothy Mou, Julian Mackay, Jonathan Aldrich, Alex Potanin
TL;DR
Nominal Wyvern addresses the decidability challenges of merging functional and OO features in DOT by instituting a semantic separation between nominal type definitions and structural refinements, augmented with explicit shape/material annotations. This design preserves expressiveness such as F-bounded polymorphism and module-like patterns while ensuring subtype decidability through a material/shape separation framework and a nominal subtyping graph. The paper provides a formal grammar, typing rules, and a decidability proof for subtyping, plus a type-safety proof using a fuel-annotated big-step semantics, and demonstrates expressiveness via practical patterns like ML-like modules and OO patterns. The approach yields a more usable, Java/OO-friendly nominal system that retains DOT's practical expressiveness without sacrificing safety or performance, with clear avenues for tooling support and further integration with existing DOT-like languages.
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.