实现类型推断

我在这里看到一些关于静态与动态类型的有趣讨论.我通常更喜欢静态类型,因为编译类型检查,更好的文档代码等.但是,我确实同意,如果像Java那样完成代码,它们会使代码混乱.

所以我即将开始构建自己的功能样式语言,类型推断是我想要实现的事情之一.我确实理解这是一个很大的主题,我并不是想创造一些以前没有做过的东西,只是基本的推理......

什么阅读的任何指针将帮助我这个？优选更实用/实用的东西,而不是更理论的范畴理论/类型理论文本.如果有一个实现讨论文本,使用数据结构/算法,那将是可爱的.

我发现以下资源有助于理解类型推断,以增加难度:

第30章(类型推断)免费提供的书PLAI,编程语言:应用和解释,草拟基于统一的类型推断.

夏季课程将类型解释为抽象值呈现优雅的评估者,类型检查器,类型重构器和使用Haskell作为元语言的推理器.

第7章(类型)EOPL,编程语言要点.

第22章(类型重建)的书TAPL,类型和编程语言,以及相应的OCaml实现recon和fullrecon.

第13章(类型重建)新书DCPL,编程语言中的设计概念.

选择学术论文.

Closure编译器的TypeInference是类型推理的数据流分析方法的一个例子,它更适合Hindler Milner处理的动态语言.

但是,由于最好的学习方法是,我强烈建议通过编写程序语言课程的作业来实现玩具功能语言的类型推断.

我建议在ML中使用这两个可访问的作业,您可以在不到一天的时间内完成:

热身的PCF口译员(解决方案).

PCF类型推断(一种解决方案),用于实现Hindley-Milner类型推理的算法W.

这些作业来自更高级的课程:

实现MiniML

多态,存在,递归类型(PDF)

双向Typechecking(PDF)

子类型和对象(PDF)

不幸的是,关于这个主题的大部分文献非常密集.我也是你的鞋子.我从编程语言:应用程序和解释中首次介绍了该主题

http://www.plai.org/

我将尝试总结抽象的想法,然后是我没有立即发现的细节.首先,类型推断可以被认为是生成然后解决约束.要生成约束,请通过语法树递归并在每个节点上生成一个或多个约束.例如,如果节点是"+"运算符,则操作数和结果必须都是数字.应用函数的节点与函数的结果具有相同的类型,依此类推.

对于没有"let"的语言,您可以通过替换盲目地解决上述约束.例如:

(if (= 1 2) 
    1 
    2)

在这里,我们可以说if语句的条件必须是boolean,并且if语句的类型与其"then"和"else"子句的类型相同.由于我们知道1和2是数字,通过替换,我们知道"if"语句是一个数字.

事情变得令人讨厌,而我暂时无法理解的是处理let:

(let ((id (lambda (x) x)))
    (id id))

在这里,我们将'id'绑定到一个函数,该函数返回您传入的任何内容,也称为身份函数.问题是函数的参数'x'的类型在每次使用id时都是不同的.第二个'id'是a-> a的函数,其中a可以是任何东西.第一个来自(a-> a) - >(a-> a)这被称为let-polymorphism.关键是以特定顺序解决约束:首先解决'id'定义的约束.这将是a-> a.然后可以将id类型的新的,单独的副本替换为用于每个地方'id'的约束,例如a2-> a2和a3-> a3.

这在在线资源中并不容易解释.他们将提到算法W或M,但不提及它们在求解约束方面的工作方式,或者它为什么不对let-polymorphism进行barf:这些算法中的每一个都强制执行解决约束的排序.

我发现这个资源非常有助于将算法W,M和约束生成的一般概念联系在一起.它有点密集,但比许多更好:

http://www.cs.uu.nl/research/techreps/repo/CS-2002/2002-031.pdf

许多其他论文也很好:

http://people.cs.uu.nl/bastiaan/papers.html

我希望这有助于澄清一个有点模糊的世界.

除了函数语言的Hindley Milner之外,另一种流行的动态语言类型推断方法是 abstract interpretation.

抽象解释的想法是为语言编写一个特殊的解释器,而不是保持具体值的环境(1,false,closure),它适用于抽象值,也就是类型(int,bool等).由于它是在抽象值上解释程序,这就是为什么它被称为抽象解释.

Pysonar2是Python的抽象解释的优雅实现.Google使用它来分析Python项目.基本上它用于visitor pattern将评估调用分派给相关的AST节点.visitor函数transform 接受context将评估当前节点的函数,并返回当前节点的类型.