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.

翻译：依赖对象类型（DOT）演算融合了函数式语言概念（如模块）与传统面向对象特性（如对象、子类型化），以实现更强的表达能力（如F-界多态性）。然而，这种范式融合的代价是子类型可判定性的丧失。近期关于恢复DOT可判定性的研究要么牺牲表达力，要么降低易用性。递归类型与类型界的无约束构造使得子类型可判定性问题比传统面向对象编程中更为困难。针对这一问题，本文提出Nominal Wyvern——一种类DOT的依赖类型系统，其采用创新设计思路：不同于DOT采用统一的结构化语法，Nominal Wyvern围绕"语义分离"原则构建，即在名义声明递归类型与使用时的结构化精化之间建立分离机制。该设计能自然引导用户避免编写不可判定的递归结构化类型。从技术视角看，这种分离机制通过适配材料/形状分离技术（一种通过区分子类型约束类型与具体数据类型来实现子类型可判定的方法），为保障可判定性提供了可能。最终形成的类型系统既保持面向对象用户熟悉的语法结构，又能在不牺牲F-界多态性与模块系统实际表达能力的前提下实现可判定性。