极化子类型
Polarized Subtyping
摘要：
按推值调用中类型的极化自然导致归纳定义的可观察值（按正类型分类）和共归纳定义的计算（按负类型分类）的分离，伴随模态在它们之间进行调解。以这种分离为出发点，我们开发了一个语义特征的类型与步骤索引捕捉观察深度的递归计算。这种语义为推值调用的等递归变体（包括变体和惰性记录）提供了丰富的子类型规则集。我们进一步提出了一个双向的语法类型化系统的值和计算，优雅和务实地规避困难的类型推断的宽度和深度的子类型的变体和懒惰的记录。我们展示了我们的系统的灵活性，系统地派生相关系统的子类型（a）isorecursive类型，（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.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
