姬世略译文集

原文：Folding in Parallel 作者：Oleg Kiselyov 本文描述了一种有趣的方法，用 map 和幺半群 reduce 来表述顺序执行的 fold。这样一来，某些看似有顺序的算法不仅可以并行运行，甚至还拥有美妙的并行性质：我们可以将输入序列任意分割给工作单元（如有必要，甚至可以递归地分割出子部分），并让工作单元并行运行——没有竞态条件、数据依赖，甚至不会有内存 bank 冲突。这种美妙的并行性质是多核、GPU 或分布式计算的理想选择。 这种方法的内在原理早已人尽皆知，但同样众所周知的是：将原理应用到具体案例需要独创性。 导言：fold vs. 幺半群 reduce Guy Style 在二〇〇九年的 ICFP 会议上发表了一篇题为 «foldl and foldr considered slightly harmful» 的主题演讲1。在演讲中，他提倡用 (map)reduce 取代 fold。 回想一下，序列上的 fold 本质上是一种带状态的按顺序累加；为具体起见，我们在列表上定义 fold_left : ('z -> 'a -> 'z) -> 'z -> 'a list -> 'z fold_right : ('a -> 'z -> 'z) -> 'a list -> 'z -> 'z 有一说一，现在我们有两种 fold：左 fold 与右 fold。下面的例子应该可以清楚地看出它们对应的语义...

原文链接：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 的这一洞见了。...

原文标题：Similarity between instruction scheduling and imperative functional programming 作者：Oleg Kiselyov 原文链接：https://okmij.org/ftp/Haskell/fp-arrays-assembly.txt 将「典型的命令式编程代码」转换为函数式编程代码的过程，似乎有些类似于现代 CPU 编译器中使用的数据流和控制流依赖分析——所谓典型命令式代码，就是涉及了嵌套循环和可变数组的「典型数值计算」代码。下面将考虑三个此类转换的例子。 第一个例子在本主题之前的回帖中就已经讨论过，为了使该代码的内循环更有意义，这里对其稍作修改。该示例的命令式形式为 for(int i=1; i<=zx; i++) for(int j=1, a=i+1, b=i*j; j<=zx; j+=1, a+=1, b+=1) for(z=j; z<=zu; z+=2) array[z] = a, array[z+1] = b; 这个例子其实很简单。我们注意到代码只会写入 array，而不会读取 array，也没有控制流分支，唯一需要担心的就是更新 array 操作的顺序性问题。那么，解决方案就呼之欲出了——首先生成一个「更新列表」，这个列表告诉我们应该将数组的某个元素设置为某个值；生成列表之后，我们再按列表执行更新。我们可以用函数式编程生成这样的列表，然后用命令式编程——Monad 来执行。而且由于 Haskell 的惰性求值特性，我们可以一边生成更新列表的元素，一边执行。 下面是对应的 Haskell 代码 import ST -- 提取代码中所有更新数组的操作 ex1_update_list zx zu = concat $ [ [(z,a), (z+1,b)] | i <- [1..zx], (j,a,b) <- takeWhile (\(j,_,_) -> j<=zx) $ iterate (\(j,a,b) -> (j+1,a+1,b+1)) (1,i+1,i*i), z <- [j,j+2....

原文标题：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 和 + 运算，由于它们本身就是函数（也可以说是一个带参数的值），结果就会得到一个高阶函数：...

原文标题：How fundamental is information? 作者：Oleg Kiselyov 原文链接：Doubts about the concept of information 本文是一篇批判性文章，探讨了信息概念的定义和基础。这篇文章的灵感源自 David Berlinski 的《What Brings a World into Being?》 [Berlinski]。 Berlinski 文章的主旨正是告诫人们不要以信息中心的视角来看待世界。正如文章所说，「把信息视为万事万物的本质」已经成为了一种流行的观点： The thesis that the human mind is nothing more than an information-processing device is now widely regarded as a fact. ‘Viewed at the most abstract level,’ the science writer George Johnson remarked recently in the New York Times, ‘both brains and computers operate the same way by translating phenomena – sounds, images, and so forth – into a code that can be stored and manipulated’ ....

原文标题：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 Dream of an Ultimate OS 作者：Oleg Kiselyov 原文：A Dream of an Ultimate OS 摘要 这是一场梦，梦由现实的碎片拼凑而成，有时会以奇异的组合方式重新排列。这个梦已经酝酿了十多年，滥觞于对许多主流现代操作系统的不满。 一个显而易见的事实是：用户在系统终端上所做的事情不过请求、读取、修改排列在表格或可滚动的列表中的文本信息。然而，用户往往需要使用完全不同而且毫无关联的命令进行完全相同的修改。如从列表中删除某项（行） 删除文本文件中的一行 删除文件 杀死进程（即从活动进程列表中移除之） 取消打印任务 此外，尽管操作系统中充斥着各种各样的表： 关于文件的层次数据库 电话号码表（黄页） 关于二进制对象归档（程序库）的哈希表 关于 IP 路由、当前进程、用户以及代码修订版本的，相对扁平的数据库 操作系统的核心服务中却明显缺乏常见的数据库功能：如用哈希键将一条记录 inserting 进入「表」中，使用简单或组合的键来 retrieving 一条记录或其字段，以及表间的 linking。 当用户在某些事物中查询「foo」一词，然后删除/关闭/停止查询出来的结果。无论这些结果是一段文字、一个网络连接、一个订阅的新闻组还是一个进程，用户都只需要大致相同的鼠标点击或按键顺序，且操作系统会以同样的精神来理解和解释。本文正是试图想象这样的操作系统会是什么样的，它又将如何工作。 必须强调的是，本文写于 1995 年春。文中讨论的一些观点，如：包含所有信息的数据库（注册表）、桌面作为主页等，在后来都成了老掉牙的想法。然而，直到那年秋天，网景（Netscape）公司才公开提出了活动桌面（Active Desktop）1的概念。在 1995 年，微软（Microsoft）甚至还不认为自己是一家互联网公司。此外，本文是在 BeBox2（用一个自定义的数据库作为文件系统）发布之前写的。 导言 人们看待操作系统的角度通常有两种：一种是管理计算资源；另一种则是隐藏硬件特性，同时为用户提供友好的界面。后者似乎是操作系统的主要职责，毕竟中央处理器并不关心正在运行的是什么系统，也不关心它当前要处理的代码是系统级还是用户级的。然而，除 MacOS、MagicCap 和 Newton OS 外，操作系统一直向用户提供大量不同的界面、命令和操作，而这些操作的目的基本上都是填写某种列表或表格。此外，操作系统的每个主要组件——文件系统、网络服务、用户管理、终端管理等等，都在实现和管理着自己独有的简单数据库。 由此看来，数据库服务和文本/列表编辑显然是操作系统中的一种核心活动，应当在非常基础的层面上进行支持。论文中附带了一些图片，展示了如何实现这种统合，以及如何使用这种统合的具体案例，以下是预览： MacOS 已经把 TextEdit3 提升为标准的系统（工具箱）服务——这正有力地证明了：操作系统的任务不只是管理文件和进程。此外，虽然删除一段文本、一个文件、一个目录，甚至是一个文件服务器连接都可以通过相同的操作完成：选中并拖拽进入回收站。但这一理念仍有改进的余地：例如，进程列表在概念上和文件列表并无太大区别，我们可以想象 Finder 所管理（即排列、获取信息、复制和丢弃）的文件和文件不一定是普通的文件和文件夹，它们可以是进程、打开的 TCP 连接、新闻组、活动的和待处理的打印任务，以及待办任务等。 从本质上说，操作系统不过是许多数据库的管理器。事实上，无论是文件系统、进程表、路由表，还是已知 AppleShare 服务器的列表、版本控制系统（Projector）数据和 Think C 项目，这些东西都是数据库。为什么我们不用一个设计良好的分布式数据库，来统一这些数量众多的「自定义」数据库呢？ 传统的数据库通常是在文件系统之上实现的。然而，文件系统本身就是一个数据库。Mac 的 HFS 和 Novell 的文件系统甚至也使用 B-树数据结构，以及一些其他「真正的」数据库使用的高级索引方案。在数据库中查询「1994 年一月的销售额」和依次点击文件夹「1994 年」，「一月」，「销售额」其实是两种密切相关的活动。为什么不能用「真正的」数据库完全取代文件系统？现代数据库具有存储图像文件、声音文件、电影文件和各种大小的文件对象的所有功能，并提供了灵活的链接和查询记录的接口，我不禁要问：「我们还需要『文件』做什么？」...

译自 Elementary Tutorial on Normalization-by-Evaluation。除非特殊声明，下文中「我」指原文作者 Oleg Kiselyov。 导言 本教程的初衷是为本科生提供一个五分钟快速入门通过求值进行归一（Normalization by Evaluation, NbE）技术的教程。因为是入门教程，所以只要求读者拥有小学或以上的数学背景知识，也无需拥有任何编程经验，读者可以一边在海边玩贝壳游戏一边进行学习。游戏的规则很基础，但游戏本身并不总是简单。在海边玩贝壳游戏可能是一个很好的契机，让你认识到：计算、规约、归一，以及证明游戏规则具有推进性和保持性的过程，都不过是一种玩弄符号的游戏。 但总有人试图超越符号的表象，将其视为真实事物的投影；在看似随意的规则背后寻找直觉，试图把握无脑游戏的意义。这样的人无疑会发现 NbE——就像人们在历史上多次重复发现的那样，本教程就是要指导读者重新发现 NbE。 游戏设置 让我们从一个游戏/谜题开始，它是许多小学练习的简化版本。玩这个游戏需要用到袋子、贝壳和橡皮筋。 袋子可以是空的，也可能内装有一个或多个贝壳 贝壳是一种游戏代币，彼此之间不作区别 「束」可以单指一个袋子，也可以通过用橡皮筋把另外两「束」扎起来作为一个新的束 我们将贝壳记作 #。在游戏中，两个「装有三个贝壳的袋子」可以视作同一个事物，并统一记作 [###]。而束的记法则是：把组成的两个束并排写在一起，中间用逗号隔开，然后两边加上圆括号。[##]，([##],[])，([##],([###],[#])) 都是合法的束，另外第一个例子也可以视为一个袋子。让我们较真一点：其他任何形式的记号都不是束（或者袋） ，像 [[]] 以及 (#, [&]) 就不是束，因为他们不是由方括号所包围的零个或多个 # 组成，也不是由圆括号包围的成对的方括号组成。 游戏的玩法是：给定一个束，找出一个「等价」或者说「相等」但更「简单」的束，并最终找到最简单的束——许多游戏甚至是学校里的练习题本质上都如此。例如，我们会得到一个形如 $5x-3=3x+7$ 的束，然后被要求找出与其等价且最简单的（在本例中，这样的束是 $x=5$）。 在开始游戏前，我们必须搞清楚两个束怎么才算「相等」，以及什么是「更简单」。 引用资料 我们的游戏实际上是 B. Pierce 所著的《Types and Programming Languages》中第 3 章内容的变体。这本书的本质是一些逐渐复杂化的玩弄符号的游戏的集合——尽管它自己没有如此声称。 相等 如何制定游戏规则，即定义束的「同一性」或者说「相等」完全取决于我们自己。我们可以一手指一个束然后声明它们相等，也可以把两个束分列 ~ 符号的两侧然后声明它们相等，如：([#],([##],[###])) ~ ([##],([#],[###]))。我们可能会声明很多类似这样的相等性，因此需要一种更简洁的写法。比如下面这样 首先，声明 ([], [S]) 等于 [S]，其中 S 代表包括 0 在内的任意数量的贝壳。 其次声明 ([#S],([T],[U])) ~ ([S],([#T],[U]))，其中 S、T 和 U 均代表任意数量的贝壳，而 #S 代表比 S 再多一个（#T 同理）。...

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