关于类型推导的幻灯片
今天下午在IU做了一个讲座,关于类型推导(type inference)。不敢说能让没有一定基础的人看懂,但是我确实放进了很多基本的直觉。这些都是用动画效果演示出来的。我没有想到做一个幻灯片会如此好玩。希望以后多做一些。
这里也提供一个PDF版本。基本的分步显示效果都还在,可是很多动画效果,比如物体的移动,电火花,火焰之类的全都没了。
下面是这个讲座的内容简介:
在这个讲座里,我指出一个简单而统一的思维方式来解释和设计类型推导系统,从最简单的到最复杂的。这些系统包括:
- Hindley-Milner 系统(“HM 系统”,ML 和 Haskell 所用)
- MLF 和它的竞争者们 (一种比 HM 系统更强大的系统)
- Intersection type 系统
- Polar type system 和 bidirectional type checking
我试图回答以下这些问题:
- 设计一个类型系统所需要的主要直觉有哪些?
- ML和Haskell所用的Hindley-Milner系统所提供的"let-polymorphism"有一个重要的问题。如何解决这个问题,而不增加程序员理解的负担?
- 为什么比 Hindley-Milner 系统更强大的类型系统(MLF,intersection types)很少在实际的语言中用到?
- 为什么类型系统的“表达力”跟它的“效率”总是成反比的?如何从中找到一个平衡点?