论文标题
极化亚型
Polarized Subtyping
论文作者
论文摘要
呼叫值中的类型的极化自然会导致归纳定义的可观察值（由正类型分类）的分离，并共同定义的计算（由负类型分类），它们之间介导了它们之间的伴随模式。以这种分离为起点，我们开发了用步骤索引键入的语义表征，以捕获递归计算的观察深度。该语义证明了一系列逐渐呼叫值的等值变体（包括变体和懒惰记录）合理的。我们进一步提出了一个双向句法打字系统，用于值和计算，在存在宽度和深度子类型的情况下，对于变体和懒惰记录的宽度和深度亚型，可以优雅和务实地规避类型推理的困难。我们通过系统地得出（a）同源类型，（b）按名称和（c）逐个通话，通过系统地得出相关的子类型系统来证明系统的灵活性。
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.
