OCaml

原文链接：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ꟳ 系统就是这一理念的自然发展。...

原文标题：Safe and Efficient, Now 作者：Oleg Kiselyov 原文地址：Lightweight Static Guarantees 本文确立了一种严谨的编程风格（事实上，十多年前就有人确立过）。这一风格通过利用成熟的、实用的语言（如 OCaml、Scala、Haskell 等，某种程度上 Java 和 C++ 也可纳入这一范畴）中的现有类型系统，从而静态地保障一系列广泛的安全性质。 永远不会对空指针解引用，或取空列表的头部元素。 始终对用户提供的输入进行消毒。 只使用数组界内的索引值访问（动态分配的）数组，且数组大小不需要静态可知。 这一技术与模块化开发、分离编译、命令式编程、原生的可变数组、间接索引以及一般递归等编程语言特性兼容。使用这种技术编写的程序所需的运行时检查更少，因此不但更可靠，而且更高效。这一技术并非旨在取代基础的代码形式化验证方法，而是补充并结构化了这种方法：我们可以用形式化方法证明（小而简单的）安全内核的正确性，然后用这一技术将安全内核的静态保障从内核扩展到整个程序。 在研究的过程中，我们发现有两个点令人惊讶：首先，我们上面所列举的内容居然是可行的；其次，这些技术是如此古老（可追溯到 Morris 1973 年的论文），如此简单，但却鲜为人知。 导言 OpenSSL 的心血［Heartbleed］漏洞给人们带来的惨痛回忆已逐渐淡去——毕竟，可被利用的安全漏洞常常都有。但心血漏洞仍然令人瞩目，因为漏洞本身是如此的微不足道，人们却花费了大量精力来修复它的影响。 与许多其他的此类性质的漏洞一样，心血漏洞的出现并未经过太多的酝酿——正如 SSL 的心跳［heartbeat］功能开发者所解释：「我当时正在改进 OpenSSL，提交了大量的漏洞修复，并添加了一些新功能。不幸的是，在其中一个新功能中，我漏了验证某带长度的变量的长度。」而 OpenSSL 的代码审核——「显然也没有注意到这一遗漏。」这位开发者又补充道：「因此这个漏洞从开发分支进入了发布版本。」最终在发布版本中潜藏了两年，一直未被（公开）发现。 最终修复这一漏洞的 OpenSSL 补丁证明：这一漏洞本身确实微不足道，不过是一条语句 memcpy(bp, pl, payload); 这条语句从输入数据包（自指针 pl 开始）中拷贝 payload 大小的数据载荷，然后将拷贝出来的内容放入输出数据包缓冲（自指针 bp 开始）。payload 值是从之前的输入数据包中读取的，当恶意攻击者发送的数据包声明它的载荷量是最大有效值，但实际却没有携带任何数据载荷时，问题就来了：在这种情况下 memcpy 没法从接受到的数据包中拷贝（因为已经结束），反而是从 OpenSSL 输入缓冲区的剩余垃圾中拷贝数据。这些「垃圾」实际上是之前剩余的数据，通常包含密码等敏感信息。 另一个令人不安的点在于：如果禁止程序员直接使用 memcpy 这样的低级函数，而是强制其通过一些封装（例如强制检查 pl + payload 地址是否仍在输入数据包内）来调用，像心血漏洞这样的问题本来很容易避免（因为输入数据包的边界很容易获得）。这种调用限制可以在任何具有模块［module］或命名空间［namespace］抽象机制的语言（C++ 等）中实现，甚至也可以在 C 语言中实现： 「抽象」就是关键所在：通过对内部数据和函数的抽象，迫使程序员使用带有安全检查的公开 API。抽象还能通过「避免外部程序污染内部状态」，从而确保一些已经通过安全检查验证的不变式［invariant］在任何情况下都成立——这样，就不必反复地进行某些安全检查了，甚至可以完全不需要检查。因此我们的口号是：「安全和高效，我全都要。」 这编程风格背后的思想其实稀松平常，甚至可以追溯到计算机的洪荒年代：由硬件保障的内存和设备的访问限制。硬件保护层将计算系统分为（受信任的）内核（在特权模式下运行，可执行底层操作）和用户态［user-level］程序，后者只能通过内核公开的 API（系统调用）访问设备，而内核 API（系统调用）会检查正确性和访问权限。譬如，用户态程序不能随意写入磁盘，它们只能执行 open 系统调用；在经过权限和一系列检查后，系统调用返回一个不透明的标记，即文件描述符［file descriptor］。这一描述符代表了「执行规定的的操作的能力［capability］」，还代表了一种「授权成功」的事实，在进一步的操作中就无需重复验证授权。Jame Morris 1973 年发表的论文 «Protection in Programming Language» 首次将操作系统中的部分理念应用到软件开发中，这些理念包括内存保护、身份验证、整理、作用域控制等等。该论文还展示了软件/语言的保护层是如何帮助我们对程序进行本地化、模块化的推理。而自 1973 年以来，编程语言中的抽象设施变得更加广泛和普及，现在是时候充分利用 Morris 的这一洞见了。...

原文标题：Higher-kinded bounded polymorphism 作者：Oleg Kiselyov 原文链接：Higher-kinded Bounded Polymorphism 为了表达数据集合上的泛型操作，或嵌入有类型的 DSL（尤其是在 tagless-final 方法中），经常需要对类型构造器［type constructor］进行抽象，然后在之后才为类型构造器提供参数。通常情况下，被抽象的类型构造函数不是任意的，而必须是实现了特定的接口（比如抽象序列）——这就是所谓有界多态［bounded polymorphism］。 OCaml 并不直接支持高种类多态［High-Kinded Polymorphism］：OCaml 的类型变量只能包含类型，不能包含类型构造函数；如果不给类型构造函数应用正确数量的参数，它就无法出现在类型表达式中。尽管如此，OCaml 还是可以表达高种类多态的——事实上，有几种或多或少比较麻烦的方式，其中的不那么麻烦的方式尤其鲜为人知，却又不断被重新发现。本文总结了表达（有些时候，是避免）高种类多态的不同方法。这些方法收集自多年以来的学术论文和 Caml-list 邮件列表上的信息，并根据文章的需要进行了调整和重新解释。 导言 Polymorphism abstracts types, just as functions abstract values. Higher-kinded polymorphism takes things a step further, abstracting both types and types constructors, just as higher-order functions abstract both first-order values and functions. 译：多态是类型的抽象，正如函数是值的抽象。而高种类多态则更进一步，它同时抽象了类型和类型构造函数——正如同高阶函数同时抽象了一阶值和函数。——Yallop 与 White（FLOPS 2014） 我们将进一步阐述这一非常精炼的总结，从而说明（有界的）高种类多态是如何产生的。这里介绍的例子将贯穿全文所有章节。 在实践中，经常会出现「对某些数字求和」的情况，对具体的数字类型进行抽象，就可以得到能在任意一个数字集合（列表）上执行的函数： let rec sumi : int list -> int = function [] -> 0 | h :: t -> h + sumi t 我们可以进一步抽象 0 和 + 运算，由于它们本身就是函数（也可以说是一个带参数的值），结果就会得到一个高阶函数：...

原文标题：Algebra 作者：Oleg Kiselyov 原文链接：Algebra 代数式副作用（algebraic effects）和代数数据类型（algebraic data type）中的「代数」究竟是什么？哪些模块/对象的签名是「代数」的？「代数」到底是什么？自由代数（free algebra）的「自由」在哪里？初始代数（initial algebra）是什么，它有什么用，我们如何证明一个代数具有「初始性」？我们能准确地描述 tagless-final 式 DSL 嵌入，及其解释器的正确性吗？如果能描述，如何证明这种正确性？ 本文以讲义的形式展示了一些泛代数（Universal Algebra）领域的标准入门材料，旨在解答这一类问题。不过，这些材料是专门为程序员，尤其是那些对 tagless-final 方法感兴趣的程序员所挑选和安排的。我们只使用编程中遇到的例子，并尽可能使用具体的编程语言中的符号，而非数学符号。 导言 什么是代数（Algebra）？Garet Birkhoff 被现在的人们誉为「泛代数」领域的创始人，他是这么说的： By an `abstract algebra’ is meant, loosely speaking, any system of elements and operations such as a ring, a field, a group, or a Boolean algebra. 译：「抽象代数」泛指那些由元素和运算组成的系统：如环、域、群和布尔代数。（Birkhoff，1935） 随后，他又提出了一个「临时用的形式定义」，这一定义现在仍被人们使用（稍后会回顾这些形式定义）。 泛代数是数学的一个领域——关于泛代数的课程和教科书的很大一部分内容是格论（Lattice theory）和组合数学（Combinatorics）。看起来，这似乎与常见的编程任务没有太大联系。但世事无常，造化弄人，自动机（Automata）理论（有限状态机、Kleene 代数、正则表达式）是代数在计算机科学的最早应用之一。根据 Gougen 等人（1977）的说法：Burstall 和 Landin 共著的《Programs and their proofs: An algbraic approach》（1969）首次在编程语言语义学研究中使用了泛代数和（隐含的）代数初始性。F. L. Morris（《Correctness of translations of programming languages》斯坦福大学博士论文，1972 年）则引入了编程语言中最为常见的多类别代数。而在计算机科学中全面引入代数和范畴论技术，应归功于 ADJ 四人帮（J....

译自 A Time-Travel Story。除非特殊声明，下文中「我」指原文作者凤凰院██ Oleg Kiselyov。 导言 这是一个真实的故事，有据可查，我也被卷入其中。故事讲述了有关回到过去然后做出不同选择的经历。但出乎意料的是，一件隐私，一件被认为绝对安全的秘密被曝光了。 时间旅行的故事通常以「改变过去最终了造成预料之外的结果」为题，这个故事也不例外：穿越时空意外地揭露了一个肮脏的诡计，一项瞒天过海的暗箱操作，然而……言归正传，我们开始吧。 某天，我收到了来自一位 Hansei 用户的消息：这位用户的概率程序给出了明显错误的结果。Hansei 是一个 OCaml 语言编写的概率编程库，它的工作原理是：通过不断地回到过去做出不同选择从而创造新的世界线，并统计潜在的世界线的历史记录。这位用户最终发现库函数 List.map 是罪魁祸首：当他使用自己写的 map 函数时，问题就消失了。我感到很困惑，列表的 map 函数应该很简单，不可能出错。用户还提到了他用了 Batteries1，这是一种 OCaml 标准库的替代品。我亲自查看 Batteries 库源码之后发现了这个…… 版本 当前版本为 2014 年 9 月版 引用资料 Why List.map does not be implemented 2014 年 9 月 29 日至 10 月 1 日间在 Caml-list 邮件列表上讨论的主题 HANSEI: Embedded Probabilistic Programming Hayo Thielecke: Using a Continuation Twice and Its Implications for the Expressive Power of call/cc...

译自 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....

译自：What are denotations, exactly? 。除非特殊声明，文中「我」指原文作者 Oleg Kiselyov。 指称语义通常被描述为：利用数学对象解释表达式（语法对象）。那么，所谓『数学对象』究竟是什么？OCaml 代码可以是数学对象吗？花些时间去思考到底什么是指称语义是值得的。 在最早一批的诸多『指称语义』的定义中，Landin 指出（Landin 1966，第 8 节） The commonplace expressions of arithmetic and algebra have a certain simplicity that most communications to computers lack. In particular, (a) each expression has a nesting subexpression structure, (b) each subexpression denotes something (usually a number, truth value or numerical function), (c) the thing an expression denotes, i.e., its `value’, depends only on the values of its subexpressions, not on other properties of them....

译自：Type inference and the undead code。除非特殊声明，下文『我』指原文作者 Oleg Kiselyov。 类型推导算法通常依赖于代码上下文，因而不具有组合性。Hindley-Milner 风格的类型推导的设计中，明确允许了『蒐集类型约束并求解』的过程中上下文影响/确定表达式（如变量）的类型。不过，类型推导算法的非组合性质有时也会给人们带来『惊喜』。例如，类型良好的『明显死代码』会影响整片代码的可赋类型性（typeability），甚至会影响其运行结果。本文的写作动机源于我与 Andreas Abel 自 2012 年 7 月始在 Haskell Cafe 邮件列表的进行的一系列讨论，他希望把讨论期间提出的各种示例记录下来。本文就是为了完成这一愿望－－收集，扩展和完善这些示例并建立它们内在的联系。 『死代码』通常指没有数据流和控制流流过的表达式。本文使用该术语专门表示无关的变量定义：即类型良好且无副作用，也没有数据流和控制流流过的变量定义，这些定义的标识符甚至不能出现在相关的表达式中。 首先从最简单，最广为人知的例子开始。在例子中，无关的定义导致了表达式无法被赋予类型。读者肯定在任何使用 Hindley-Milner 风格的类型推导的语言中都见过这样的例子。下面用 OCaml 的一个简单子集具体展示： let exp = let id = fun u -> u in let f = id id in let z = fun () -> f true in f 1 这段代码无法通过类型检查，检查器报告表达式 f 1 的类型错误。但是，如果我们删除 z 的定义（f 1 中显然没有出现 z），修改后的程序突然就变成类型良好的了。 练习：是否存在其他合法（从动态语义的角度）的代码转换能使 exp 的类型正确？ 在 Haskell 98 及以上版本中，类似的问题常常与臭名昭著的 MonomorphismRestriction 相关：...

译自 Markov Algorithm。除非特殊声明，下文中「我」指原文作者 Oleg Kiselyov。 如果问一个人知道什么计算模型，得到的常见答案可能是「图灵机」和「λ-演算」。也许有的人会说「寄存器机」，但应该不会有人说「Post 系统（Post System）」1或「Markov 算法（Markov Algorithm）」 。这洵为一件憾事，因为逻辑学和理论计算机科学中常见的推理规则就是 Post 系统的一种表现形式，模板引擎、EBNF 规则、XSLT 或宏也是如此。仔细研究这些系统及其令人惊讶的表现力或许会令人有所启发，毕竟，Chomsky 就受到了 Post 系统启发，他的上下文无关生成文法以及其他一些生成文法都受到了 Post 系统的影响。除了作为计算模型的理论意义外，Markov 算法的思想也启发了一种真正的编程语言：Refal。在模式匹配被推广到普通的编程语言之前，Refal 就已经基于模式匹配。「窥孔优化（peephole optimizer）」也是一种 Markov 算法。 Post 系统（试想生成文法）基于重复的，甚至可能是上下文相关的字符串替换，即用新的字符串替换一个原有字符串的子串。替换规则由一组有限的规则序列（文法生成规则）组成，可以用任意顺序应用替换规则。而「正规 Markov 算法（Normal Markov Algorithm）」，顾名思义，是这种基于规则的替换系统的一种受限的「正规」形式。在正规 Markov 算法中，替换是上下文无关的，同时按照严格定义的顺序进行。因此整个字符串替换过程具有确定性，可以通过一种简单的机制（即「机器」）完成。正规 Markov 算法才能称之为「算法」2（这其实是一个俄语中的文字游戏，「算法」在俄语中是「алгоритм」，而 Markov 称他的系统为「алгорифм」）。 由上可知，正规 Markov 算法是一种机器，根据一串重写规则序列，通过按顺序反复应用规则重写输入字符串。规则由源 src 和替换目标 rplc 一对字符串组成，两者都可为空字符串。有的规则被标记为「终止规则」。机器的工作循环是：按重写规则序列的顺序，依次尝试用每条规则的 src 匹配输入字符。如果有匹配的，那么就用对应的 rplc 替换输入字符串中最左侧匹配到的 src 。匹配结束后，如果这条规则是一条终止规则，那么就停机。否则把改写后的字符串作为新的输入，然后重新开始循环。当没有可用的规则时也停机。 举个例子，下面是一个 OCaml 数组形式编写的规则序列。它可以把一个大端序二进制数字（由 0 和 1 组成的字符串）转换为由 | 组成的一进制数字字符串。 let bin_to_unary = [| rule "1" "0|"; rule "|0" "0||"; rule "0" ""; |] 使用本文随附的代码运行 run bin_to_unary "110" 可以生成有六条杠的字符串 "||||||"。该代码还打印了重写过程中触发的所有规则以及对应生成的中间结果，以展示这一巧妙算法的工作原理。...