类型论

原文链接：Efficient and Insightful Generalization 作者：Oleg Kiselyov 摘要 Hindley-Milner 类型推导的实现并非只有 W 算法一种。1988 年，Didier Rémy 在研究如何加快 Caml 的类型推导速度时发明了一种优雅的类型泛化算法。这种算法无需扫描类型上下文，因而速度奇快。这种算法还能顺利扩展以捕获逃逸出作用域的局部类型声明，以及应用到支持全称量化类型以及存在量化类型的系统，甚至是 MLꟳ 系统中。 遗憾的是，算法本身以及算法在 OCaml 类型检查器的实现都鲜为人知，而且缺乏文档。本文旨在解释和普及 Rémy 算法，并解密 OCaml 检查器的一部分实现代码。本文还旨在保存 Rémy 算法的发明史。 Rémy 算法的魅力在于：它洞见到了类型泛化与依赖追踪的内在关联——即自动内存管理系统（如区域或分代垃圾收集）中所使用的追踪内存的方式。类型泛化可以视作在「给带有类型注释的抽象语法树中共享类型的节点加上连接边」所组成的图中寻找支配节点的过程。在 Fluet 和 Morrisett 的区域演算中，他们通过「类型变量能否泛化」判断区域中是否包含某资源。无独有偶，Rémy 的算法则通过测试「区域是否包含某类型变量」，从而决定该变量是否可被泛化。 导言 本文最初是为了了解 OCaml 类型检查代码而做的笔记，OCaml 类型检查器的代码庞大、复杂，而且几乎完全没有文档。在挖掘这些代码的过程中，我们发现了真正的宝藏，其中之一就是一种高效而优雅的类型泛化［type generalization］算法，下面将重点介绍。 OCaml 类型检查代码使用的泛化算法基于对类型的所谓等级［level］的追踪。这些「等级」也能避免模块中定义的类型逃逸到更大的范围——对于局部引入的类型构造函数而言，等级机制强制执行了区域封锁。令人感兴趣的一点在于如何统一处理泛化和区域。此外，OCaml 类型检查程序中等级还有更多的应用——如检查多态记录类型和存在量化记录类型。MetaOCaml 也间接依赖等级来跟踪未来阶段的变量绑定范围。 所有这些应用都有一个共同点：需要跟踪依赖关系，或者说需要计算数据依赖关系图中的区域范围或支配节点［dominator］。这令人回想起 Tofte 和 Talpin 提出的基于区域的内存管理技术。正如 Fluet 和 Morrisett 所展示的：我们可以利用全称量化类型［universal type］来静态地防止已分配的数据逃离其区域，因此可以在 F 系统［System F］中编码 Tofte 和 Talpin 提出的区域类型系统。同理，基于等级的类型泛化通过检测类型变量的逃逸位置来确定其区域，以及泛化引入的全称量化的具体位置。 OCaml 中的类型泛化程序（部分）实现了 Didier Rémy 于 1988 年发现的算法。其理念在于：在有类型标注的抽象语法树中显式表达类型共享。类型变量只能在「支配了该变量所有出现过的节点」的节点上量化。类型泛化相当于在增量式计算依赖图的支配节点。Rémy 的 MLꟳ 系统就是这一理念的自然发展。...

译自 Simplistic GADTs in OCaml。除非特殊声明，下文中「我」代指原文作者 Oleg Kiselyov From oleg at http://okmij.org Fri Jul 10 20:05:10 2009 To: caml-list@inria.fr Subject: GADTs in OCaml Message-Id: 20090711030510.49092176DE@Adric.metnet.navy.mil Date: Fri, 10 Jul 20091 20:05:10 -0700 (PDT) Status: RO 本文展示了一种 OCaml 中的简单、无副作用、且不需要魔法的实现 GADTs23 的方法。这种实现足以覆盖 GADTs 的许多常见应用：表达带有不变式（invariant）的数据结构、有类型的 printf/scanf、无标签（tagless）解释器等。本文提出的具体实现只是一个简单的 ML 模块，不需要修改 OCaml 系统本身。由于实现十分简单，理论上可以在任意 ML 系统上运行（不过，就如同嵌套数据类型一样，在不支持多态递归（polymorphic recursion）的 SML 上，GADT 也不是很有用）。 本文的例子涵盖了： 保障数据结构的不变式：静态地保证在一个表示某 HTML 文档的树结构中，一个链接节点不能为另一个链接节点的父节点。 有类型的 printf/scanf 实现，两个实现之间共享相同的格式化描述符。 带有常量和高阶抽象语法（High-Order Abstract Syntax）的简单有类型 $λ$-演算。我们所展示的其实就是奚宏伟等人（Xi et. al）的 POPL 2003 论文4中所展示的例子。 请移步 http://okmij....

虽然说是看看 cedille, 不过主要是因为用 cedille 写这篇內容会比较方便了。这篇主要介紹的是 MLTT 70, 又被稱為 Type : Type，只要用 dependent function type 就可以 encode higher order logic。 首先就是 well known 的 dependent function type 对应 universal qualifier。之前的 LdBeth：NuPRL 中的证明–从一到CTT 中提到的 indexed family of intersection type 也对应 universal qualifier ，不过生成的 witness 会不同。在 Cedille 中 indexed intersection 用 $\forall$ ，dependent function 用 $\Pi$ 表示。 Conjunction 可以表为如下，★ ➔ ★ ➔ ★ 是 kind， $\forall P.(A \rightarrow B \rightarrow P)\rightarrow P$ 意为对任意命題 $P$ 在有 $A \rightarrow B \rightarrow P$ 时 $A \wedge B$ 可以证明 $P$ 。...

MetaPRL 的修理告一段落了。在这篇文章里我来介紹一下它用起來大概是什么感觉的。 MetaPRL 不是像 Agda/Lean 那样直接写 proof script 然后 type check，也不是 HOL 那样完全在 repl 里做 interactive 操作，而是一半一半：proposition 先全写在文件里，编译成 rewrite abstract machine 后，link 到 Toplevel 程序，再用 repl 来进行 interactive proof，或者查阅，也可以 print 到 html 或 latex。 MetaPRL 中 proposition, tactic, inference rule 之间没有分別。primitive inference rule 就是不需要证明的 tactic，proposition 就是具有证明的 inference rule。因为用的是类似 sequent calculus 的 language，所以能定义表现力强于其它 proof assistant 里用 lemma 或 tactic 的 metatheorem。这一点原版的 NuPRL 也只是能自定义 inference rule 而不能给出 conservative extension 的证明。比如 显然易见，对形式为 $\Gamma, x:\mathbb{B}, \Delta[x] \vdash C[x]$ 的 goal 应用这个 tactic，就会生成 $\Gamma, \Delta[True] \vdash C[True]$ 和 $\Gamma, \Delta[False] \vdash C[False]$ 两个 goal。在 Agda 里这要用 dependent pattern match, 在 HOL 要用 primitive inference rule compose tactic，而在 MetaPRL 里这只是个能证明的 theorem，而且做为 tactic 没有 HOL tactic 必須要用 primitive inference rule 的 overhead。...

这一篇开头讲一点 constructive real analysis。 Intuitionistic mathematics 中，实数用一个不断提高近似精度的无穷序列(Cauchy Sequence) 定义。 即 $\mathbb{R} =_{\it def} \{q:\mathbb{N}^+\rightarrow \mathbb{Q}\;|\; \forall n,m:\mathbb{N}^+ .|q_n-q_m|\leq n^{-1}+m^{-1} \}$ 这样的无穷的序列就是 free choice sequence 中的一种，表现出来是个 $\mathbb{N}^+ \rightarrow \alpha$ 的 function type。在这里 $\alpha \simeq \mathbb{N}$ ，即和自然数一一对应，众所周知地，有理数滿足这一性质。1 显然地，引入 choice sequence 的概念时，choice sequence 可以分成三种。 一种为 lawlike，即可以用某个 algorithm 表示的。 第二种为 lawless，是完全无序的。 第三种是由前两种 choice sequence 混合得到的，是为 mix。 注意即使是 lawless sequence，也符合 function 的性质，即 $\forall a. f(a) = f(a)$ ，也就是已经生成的数是不会变更了。 尽管 choice sequence 是无限的，但明显地，任何有限的 sequence 同时是无限个 choice sequence 的初始部分。...

上一篇 LdBeth：NuPRL 中的证明 III–我不做metavariable啦 Part I: Atom type 可能有之前用过 Agda 的人会在开始用 NuPRL 以后觉得，没有 inductive type definition，只有 product 和 disjoint union 但是没有区分 data constructor 的类型，好不习慣啊。 其实这个也不是什么大问题，data constructor 可以用 NuPRL 的 Atom 类型来模拟。 Atom 頋名思义就和 lisp 里的 symbol 类似，可以比较相等。 所以一个 inductive data type definition 的 tree data Tree a = Node (Tree a) (Tree a) | Leaf a 可以表示成个 dependent pair ${\bf DEF\ }Tree(a) = rec(T. \Sigma x : {\tt Atom}. {\tt if}\ x =_A {\tt"...

上一篇 LdBeth：NuPRL 中的证明{x:N|2<x<3}–virtual evidence Constructive proof assistant 有个需求， 千里冰封 你懂吗：dependent type 下的类型推导 (meta variables) 比如 Agda 中 id' : forall (x : Prop) -> x -> x id' _ x = x 的第一个参数是不参与计算的，就可以写成 implicit argument id : forall {x : Prop} -> x -> x id x = x 在用了 implicit argument 以后，id 就是个 polymorphic function。 NuPRL 是如何实现这样的功能的呢。众所周知 universal qualification 是用 dependent function type (Pi type) 实现的。 $\forall x:\mathbb{P}. P(x) == \prod_{x:\mathbb{P}}{P(x)}$...

上一篇 LdBeth：NuPRL 中的证明 (二) – 我从来不写递归的 这篇的主要內容是 Virtual Evidence: A Constructive Semantics for Classical Logics 和 Constructive Reading of Classical Logic 的导读。 也算是第一次展示了下 NuRPL 中的证明，順帯引入 squash type 的概念。 MLTT Agda 中要获得 LEM 得 posutulate （防止你们说 CubicalTT）。众所周知这样 p 出来的 LEM 虽然和 MLTT 相容，但还是沒有 computational meaning 的，这样的 classical logic 是沒有灵魂的。 那 NuPRL 是怎么解決这个的呢？ Recall, refinment type OR subtyping in NuPRL $\{x:A\ |\ P(x) \}$ it is easy to get non dependent form...

图文无关。 上一篇文章 LdBeth：NuPRL 中的证明–从一到CTT 上一篇讲了 CTT 中的一些类型。dependent function, dependent product, dependent record, universe 这些因为和 ITT 的沒什么区別，就默认读者已经会了。CTT 特色的 dependent intersection 和 dependent union 因为应用范围超出了基础，就先不讲了。 General Recursion considered K Also, in some other type systems, general recursion is not expressible, and such structural recursion operations must be built in. 在 Agda 中，众所周知是用写程序來证明的，tc 过了相当于证明过了。然而 NuPRL 因为 undecidable type checking 的性质，除了程序以外，证明还包括了 tc。 比如吧，在 Agda 里要证 $x\leq x!$ ，就要先写 ! (factorial) 的定义，写完了以后，在使用 factorial 的定义之前，还要做两件事: 给它一个能过 tc 的类型声明，并且证明 termination。...

本文假设读者已经装了 NuPRL5 的 VM/要到了帳號并照著 http://nuprl.org/html/02cucs-NuprlManual-02overview.pdf 做基操。 这是向略懂 dependent type 的人的 NuPRL 教程，介紹这一最神/传奇的定理证明器。你不需要会 Haskell，但是至少要能理解 untyped lambda calculus，最好会点 OCaml/SML，最理想是 LCF ML，因为这是 NuPRL 的 Tactic 语言，而且它沒正式的 language report。Lisp 麻，会用 Emacs 程度就可以了，在 NuPRL 里几本用不上。 这文章只能向有 Agda/Coq/HOL/PVS/Metamath 经验的介绍下 NuPRL 了，因为完全 normie 的话像我一样出见 NuPRL 怕是不太可能有过了。 Equality in CTT 我们先来看 equivalence。不好意思让你们失望了，NuPRL 里沒有 ADT。所以 NuPRL 的 $a = b \in T$ 是个 primitive，如果 a 和 b 不等就是个空集，相等则有唯一成员 $*$ ，相当于 unit type。 值得一提的是，在 Agda 用的 ITT 中，一个 value 只能和自己相等，但在 CTT，因为有 quotient type 的概念，你还可以定义一个类型使两个不同的 value 相等。...