The simple essence of algebraic subtyping: principal type inference with subtyping made easy (functional pearl)
The simple essence of algebraic subtyping: principal type inference with subtyping made easy (functional pearl)
复制标题
代数子类型的简单本质：使子类型变得简单的主类型推理（功能性珍珠）
DOI：
--
复制
发表时间：
2020
期刊：
影响因子：
--
通讯作者：
L. Parreaux
中科院分区：
文献类型：
--
作者：
L. Parreaux
MLsub扩展了传统的Hindley-Milner类型推理，同时保留了紧凑的主类型，这是一个令人兴奋的新发展。然而，它在双统一方面的规范很难理解，依赖于双替换和极类型的新概念，并利用抽象代数的高级概念。在本文中，我们表明，这些实际上是不必要的了解在MLsub中发挥作用的机制。我们提出了一种称为Simple-sub的替代算法，它可以在500行以下的代码（包括解析，简化和漂亮打印）中有效地实现，看起来更熟悉，更容易理解。我们提出了一个实验评估简单的子对MLsub的一百万个随机生成的良好作用域的表达式，表明这两个系统一致。可变的基于自动机的实现MLsub是相当远的代数规范，留下了很大的空间的错误，事实上，我们的评估发现了几个bug在it. We素描更简单的健全性和完整性参数，基于语法规范的类型系统。这篇论文的目的是为了在形式主义，丰富的见解，易于消费的新型系统和编程语言的未来设计师。特别是，没有抽象代数是强加给读者的。
MLsub extends traditional Hindley-Milner type inference with subtyping while preserving compact principal types, an exciting new development. However, its specification in terms of biunification is difficult to understand, relying on the new concepts of bisubstitution and polar types, and making use of advanced notions from abstract algebra. In this paper, we show that these are in fact not essential to understanding the mechanisms at play in MLsub. We propose an alternative algorithm called Simple-sub, which can be implemented efficiently in under 500 lines of code (including parsing, simplification, and pretty-printing), looks more familiar, and is easier to understand. We present an experimental evaluation of Simple-sub against MLsub on a million randomly-generated well-scoped expressions, showing that the two systems agree. The mutable automaton-based implementation of MLsub is quite far from its algebraic specification, leaving a lot of space for errors; in fact, our evaluation uncovered several bugs in it. We sketch more straightforward soundness and completeness arguments for Simple-sub, based on a syntactic specification of the type system. This paper is meant to be light in formalism, rich in insights, and easy to consume for prospective designers of new type systems and programming languages. In particular, no abstract algebra is inflicted on readers.