Strict bidirectional type checking
Strict bidirectional type checking
复制标题
严格的双向类型检查
DOI：
--
复制
发表时间：
2005
期刊：
影响因子：
--
通讯作者：
R. Harper
中科院分区：
文献类型：
--
作者：
A. Chlipala;Leaf Petersen;R. Harper
完全注释的lambda术语（例如，通过系统f的各种类型的直接编码到达）包含许多冗余类型信息。因此，在实践中几乎从未使用过完全注释的形式，因为可以定义部分注释的表格，这仍然允许语法有向类型的检查。在某些证明和类型系统中使用的另一种优化是利用术语出现的上下文，使用双向类型检查规则进一步弹性。尽管该技术通常是有效的，但我们表明存在双向术语，这些术语在将其类型装饰的大小显示为命名形式的计算（汇编的常见第一步）时，会显示出渐近的尺寸。在本文中，我们基于严格的逻辑介绍了双向类型系统的改进，该系统允许消除其他类型的装饰，并表明它在顺序化下表现得很好。
Completely annotated lambda terms (such as are arrived at via the straightforward encodings of various types from System F) contain much redundant type information. Consequently, the completely annotated forms are almost never used in practice, since partially annotated forms can be defined which still allow syntax directed type checking. An additional optimization that is used in some proof and type systems is to take advantage of the context of occurrence of terms to further elide type information using bidirectional type checking rules. While this technique is generally effective, we show that there exist bidirectional terms which exhibit asymptotic increases in the size of their type decorations when sequentialized into a named-form calculus (a common first step in compilation). In this paper, we introduce a refinement of the bidirectional type system based on strict logic which allows additional type decorations to be eliminated, and show that it is well-behaved under sequentialization.