A framework for type inference with subtyping
A framework for type inference with subtyping
复制标题
具有子类型的类型推断框架
DOI：
10.1145/289423.289448
复制
发表时间：
1998
期刊：
影响因子：
--
通讯作者：
F. Pottier
中科院分区：
文献类型：
--
作者：
F. Pottier
在基于子类型的类型系统中，类型相等被子类型取代，子类型是一种限制较少的关系。这个想法是，如果71是~2的子类型，那么类型为~1的值可以透明地提供给任何需要类型为r~的值的地方。子类型已被用作创建面向对象语言的形式类型系统的关键概念。这些系统通常需要用用户提供的类型信息来注释程序。能够省略这些信息--或者至少是其中的一部分--为程序员提供了更大的自由度;因此，出现了在子类型存在的情况下进行类型推断的需求。在过去几年中，对这一问题进行了广泛的研究。已经提出了许多类型系统，具有不同程度的丰富性和复杂性。可能的特征是存在最小类型I和最大类型T，存在逆变类型构造函数（如+），存在联合和交集类型，存在递归类型，用户通过生成类型声明扩展类型语言的能力等。程序中的每个函数应用程序节点都生成一个子类型约束，它要求实际参数的类型是函数参数的类型的子类型。类型推理包括收集这些约束并检查它们是否允许解决方案。我们在这里介绍的类型系统是相当通用的。它有一个固定类型的语言，它是由I，T和--+组成的常规类型的集合。它不像[4，51]那样强大，后者具有更通用的联合和交集类型;尽管如此，它仍然足够通用，可以轻松支持添加广泛的类型构造，例如可扩展记录和变体。类型推断如上所述进行;确定约束的合取是否允许解是通过闭包计算完成的[7]。理论上，这个问题已经解决了。然而，实际上，事情只是从这里开始开始。类型推断所累积的约束数量很大（最好的情况下，程序大小是线性的;最坏的情况下，是指数的，因为让构造复制它们）。这会减慢类型推断（闭包算法需要的时间是类型变量数量的三次方），并使类型难以辨认（约束是提供给用户的类型信息的一部分）。因此，需要算法来简化子类型约束集，而不影响它们的含义。在[14]中，我们介绍了两种这样的方法。一个删除了所谓的不可达约束;另一个使用了逻辑学来提出替代，这些替代可以应用于推断的类型模式，而不会降低它们的能力。Smith和Trifonov [18]将前者改进为一个称为垃圾收集器的概念。此外，他们还描述了一个称为canonizatzon的过程，该过程包括重写类型方案，以便每个变量最多有一个构造较低的变量（分别为。上）界。其他替代方法可以在[1]中找到。因此，在这一点上，各种简化方法是已知的，其中一些是非常有效的，如垃圾收集。然而，这些都不足以获得一个有效的，集成良好的类型推理算法，还有几个问题。第一，替代品本身是低效的。许多可能性都必须尝试，而每一个t.rv都是昂贵的，因为它涉及到证明该替代品是合法的。我们解决这个问题，完全消除了算法，并取代他们与一个非常有效的minimizatl：on算法，一个近亲的“Hopcroft”算法在[9]中介绍。第二，虽然垃圾收集，正如Smith和Trifonov所描述的，工作得很好，但它并没有保留闭包属性。这是一个问题，因为我们希望类型推理算法始终使用封闭约束集，因此它可以进行增量闭包计算。我们通过展示这个来解决它。如果类型推断规则被适当地公式化，则不会生成双极类型变量，这确保了垃圾收集保持闭包。第三，对标准化orb算法进行了形式化描述，并将其与垃圾收集技术相结合，提高了算法的效率。我们还表明。如果需要，可以使用该算法的自然推广来消除双极变量。第四也是最后，wp区分了内部简化方法和外部简化方法。前者有助于提高效率，并且可以在整个类型推断过程中使用;后者有助于提高可读性，并且必须。仅在向用户提交类型信息时使用。前者与后者冲突，这就是为什么区分是重要的;试图同时实现cflicienc，y和可读性是一个设计错误。
In type systems based on subtyping, type equality is replaced with subtyping, which is a less restrictive relationship. The idea is, if 71 is a subtype of ~2, then a value of type ~1 can be transparently supplied wherever a value of type r~ is expected. Subtyping has been used as a key concept to create formal type systems for object-oriented languages. These systems often require the programs to be annotated with user-supplied type information. Being able to omit this information--or at least part of it-provides the programmer with a greater degree of freedom; hence, the desire arises to do type inference in the presence of subtyping. This issue has been extensively studied in the past few years. Many type systems have been proposed, with varying degrees of richness and complexity. Possible features are the existence of a least type I and a greatest type T, the presence of contravariant type constructors such as +, the existence of union and intersection types, the existence of recursive types, the ability for the user to extend the type language through generative type declarations, etc. Virtually all of these systems hare their type inference algorithms upon the same principle. Each function application node in the program generates a subtyping constraint, which requires that the actual argument’s type be a subtype of the funct,ion parameter’s t,ype. Type inference consists in gathering these constraints and checking that they admit a solution. The type system we present here is quite general. It has a fixed type language, which is the set of regular types formed with I, T and --+. It is not as powerful as that of [4, 51, which has much more general union and intersection types; still, it is general enough to easily support the addition of a wide class of type constructs, such as extensible records and variants. Type inference is done as explained above; determining whether a conjunction of constraints admits a solution is done through a closure computation [7]. In theory, the issue is settled. In practice, however, things only begin here. The number of constraints accumulated by type inference is large (at best, linear in the program size; at worst, exponential, because let constructs duplicate them). This slows down type inference (the closure algorithm takes time cubic in the number of type variables) and makes types illegible (constraints are part of the type information given to the user). Therefore, algorithms are needed to simplify sets of subtyping constraints, without affecting their meaning. In [14], we introduced two such methods. One removed so-called unreachable constraints; the other used heuristics to come up with substitutions which could be applied to the inferred type schemes without lessening their power. Smith and Trifonov [18] refine the former into a concept called garbage collectron. Besides, they describe a process called canonizatzon, which consists in rewriting a type scheme so that each variable has at most one constructed lower (resp. upper) bound. Other substitution methods can be found in [l]. So, at this point, various simplification methods are known, some of which are very effective, such as garbage collection. However, these are not sufficient to obtain an efficient, well-integrated type inference algorithm; several problems remain. First, substitut.ion heuristics are inherently ineficient.. Many possibilities have to be tried out, and each t.rv is costly, since it involves proving that the suhstitution”is lrgal. We solve this problem by eliminating heuristics altogether and replacing them with a very efficient minimizatl:on algorithm, a close cousin to the “Hopcroft” algorithm introduced in [9]. Second, although garbage collection, as described by Smith and Trifonov, works well, it does not preserve the closure property. This is a problem, since we would like the type inference algorithm to work with closed constraint sets at all times, so it can do incremental closure computations. We solve it by showing that. if the type inference rules are properly formulated, then no bipolar type variables are generated, which ensures that garbage collection preserves closure. Third, we give a precise formal descript.iou of the canonizatl;orb algorithm, and we combine it with garbage collection, which makes it more efficient. We also show that. a nat.ural generalization of this algorithm can be used, if desired, to eliminate bipolar variables. Fourth and finally, wp draw a distinction between internal and external simplific:ation methods. The former help efficiency, and can be used throughout the type inference process; the latter help readability, and must. be used only when submitting type information to the user. The former conflict with the latter, which is why the distinction is important; trying to achieve cflicienc,y and readability at the same time is a design mistake.