标题：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...

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

译自 Expressing formal proofs in a computer language: Y Scheme 。除非特殊声明，下文中『我』指原文作者 Oleg Kiselyov 正文 我们发现算法语言不但可以用来实现算法，也可以用来描述算法的复杂性或其他某些属性的命题，并且可以给出这些命题的严格证明。下面引用的两篇 USENET 的文章表明，Scheme 可以用于形式化推理 Scheme 自身写成的代码。 第一篇文章提出了关于某个优先队列的实现的一个猜想，并且形式化证明了该猜想。该文章为下一篇文章奠定了基础，而下一篇文章则对『形式化证明』这一概念进行反思。我认为不可思议的一点是，我们用同一种语言同时做到了： 实现算法 描述『算法在特定情况下将构建出什么形状的树结构』的命题 通过数学归纳法严格证明上述命题 另一篇发布于 2003 年 9 月的文章表明，Scheme 宏展开器是个很好的证明助手。 我们真的可以用 Scheme 进行『思考』。 参考 A USENET article formally proving complexity of one particular implementation of priority queues. 该文章（译文下附）于 1998 年十月 12 日星期一 23:51:39 GMT 以 《Can one prove complexity of priority queues?》为题发布于新闻组 comp.lang.scheme 。 A USENET article reflecting on the one above 该文章（译文下附）于 1998 年十月 18 日星期日 20:58:45 以《Expressing formal proofs in a computer language: Y Scheme》为题发布于新闻组 comp....

译自 Having an Effect。除非特殊说明，下文中的『我』指原文作者 Oleg Kiselyov。 简介 本研究如同一次追寻表象之下草蛇灰线的旅程：Monad，Monad Transformer，Free Monad 以及可扩展副作用（Extensible Effects）的创始论文本质上都是关于所谓『可扩展解释器』问题的研究。一路走来，我们意识到表达式问题（expression problem），稳定指称问题，以及可扩展解释器问题都是同一事物的别称。最终我们找到了组织原则：交互－－客户端与服务器之间的交互、解释器与被解释代码之间的交互、表达式与其上下文之间的交互。 可能用『进程演算（process calculus）』能更好描述交互。而在各种序贯式的演算中，最早的把计算副作用视为交互，并且做出形式化表述的工作则是 Cartwright 与 Felleisen 发表的著作《Extensible Denotation Language Specifications》。 本文用现代的方法重构了 Cartwright 与 Felleisen 方法。得益于 tagless-final 形式，我们重构后的版本更简单，可以直接给计算机运行。 本文也在前人的工作之上做了进一步发展。本文令副作用处理程序变得模块化且可扩展－－它变成程序的一部分，而非永久独立于程序之外。这使得下面的做法成为可能。 尽管整数和一般的一阶子语言不需要变量和环境，Cartwright 与 Felleisen 的方法也必须将变量和环境融入基本语义框架；我们避免特殊对待可变环境和任意高阶编程特性，而是将 Lambda 与 State 一视同仁。动态绑定和词法绑定，以及各种调用约定（按值调用，按需求调用，按名调用）可以视为用不同方式解释副作用『解引用绑定变量』。 对研究领域溯本求源，寻回直达本质的洞见，发掘其沧海遗珠。这一探索过程有助于为我们为程序重新发明副作用。 本演讲稿于 2016 年 8 月 25 日在印第安纳大学信息与计算学院 (SoIC) 计算机科学研讨会上首次发表。我要感谢 Martin Berger 与我进行了许多令人受益匪浅的讨论，特别是解释了进程演算的起源。此外还要感谢穆信成与 Matthias Felleisen 提出的宝贵意见。 版本 当前版本为 2017 年 9 月版 引用资料 EDSLNG.hs 本文所使用的 Haskell 98 代码的完整版 edlsng.ml Cartwright-Felleisen 框架现代重构 OCaml 版本。附带全局状态、动态绑定、按值调用和按需求调 用的词法绑定示例...

译自：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 相关：...

译自 Free and Freer Monads: Put Monad Back into Closet 简介 编写 Monad（现在还包括 Applicative 和 Functor）的实例，并确保实例符合 Monad 定律不但是定义 Monad 的重要部分，同时也是数量正在以指数级膨胀的「Monad 教程」的重要部分。而本文认为所有这些实例都不过是 boilerplate－－可以避免的 boilerplate！或许是因为听起来像拉丁语的名字和其引起的人们对顶尖数学的兴趣，这些琐碎的 boilerplate，琐碎的 Monad 定律，毫无新意的「管道」吸引了过多的关注。如果我们能直接思考副作用本身而非这些管道的工作原理，难道不让人耳目一新吗？ Free Monad，以及我们正要提到的 Freer Monad 将把我们从 boilerplate 中解放出来，从而专注于副作用的本质。有了它，我们就可以将解释器这一在编程语言研究和实践中的大杀器引入到副作用编程中－－为副作用定义解释器。 目前，已经有了许多关于 Free Monad 的精彩解释，这些解释往往援引了幺半群、普适代数和范畴论的观点。但最近流行的 Freer Monad 却给我们带来了困境：它的定位是什么？它能让我们更清晰地思考副作用吗？它也是『自由』的吗？如果是，为什么这些数学上的解释都没有预言 Freer Monad 的存在呢？本文接下来将解决这些问题，但唯独最后一个问题，我只能说，人们几次发现 Free Monad 都不是通过范畴论。（事后来看，范畴论上的联系确实存在，而且确实有洞见性）。与许多已有的解释不同，本文采取了通俗的方法，通过具体的例子而非抽象的代数解释 Free Monad（有关范畴论的内容将仅在括号中提及）。 经典 Monad 我们用耳熟能详的 State Monad 举例，该 Monad 代表『访问或更新一个可变状态』的副作用。常见的实现将这个可变状态作为返回值和参数沿着程序传递，然后通过 get 和 put 两个原语来获取/更新变量。 newtype State s a = State{unState :: s -> (a,s)} get :: State s s get = State $ \s -> (s,s) put :: s -> State s () put s = State $ \_ -> ((),s) runState :: State s a -> s -> (a,s) runState = unState get 和 put 操作，State s 蕴涵的定律以及解释器 runState，没有这三者，State s 就不能够作为真正的可变状态副作用计算使用。然而，为了在 Haskell 程序中方便地使用这些操作，我们要编写以下代码。...

译自 Language for writing text adventure, er, online courses: glimpse into the computer-assisted education of the 1970s and 1980s。除非特殊声明，译文中「我」指原文作者 Oleg Kiselyov。 线上课程现在已经不是什么新奇事物了。一门典型的线上课程包含了一段教学视频和几个课程网页，以及由屏幕上的几道选择题组成的「小测」，完成小测后会显示正确答案并统计得分。然而，「计算机辅助教育」这一概念比互联网还要早几十年出现。那时人们就很快意识到，像上面描述那样的课程是非常枯燥乏味的。 一门引人入胜、富有成效的课程应更具互动性：讲解和提问应交织穿插在课程之中。提问之后当场就要判断学生的回答是否正确，如果回答错误，可以给他们另一次回答的机会或者一些提示。如果学生还是不能回答出正确答案，则启用备用课程，更慢地讲解课程主题。问题应该是多变的，最好具有不确定性。答案的形式也应该是自由的，学生的回答可以是任意数字或字符串，而非是单纯的选择题。总之，一门引人入胜的课程应该看起来像冒险游戏。 人们很早就意识到，编写一门好课程的脚本就像编写一款好游戏的脚本一样，是一种不同于编程的技能。让课程作者用 Fortran 或者汇编语言（当时的计算机编程语言）来写脚本是不合理的，他们需要更好的工具－－用于编写课程脚本的高级语言（游戏行业也意识到了这一点）。伊利诺伊大学在 20 世纪 60 年代末开发的 TUTOR 就是早期的课程脚本语言之一。 在苏联，有一种大型机上的 TUTOR 方言/实现，我在喀山大学学习和工作时就遇到过它。在大型机上学习计算机课程很不方便，因为一般很难接触到大型机。更何况，苏联的大型机经常坏掉。 个人计算机的横空出世为计算机辅助教学提供了更好的平台，至少个人机比大型机便宜得多。这就是当时我在个人机 BK-0010 上写一门 TUTOR 方言解释器的动机。个人机的硬件性能显然不如大型机，但我的实现比大型机上使用的实现还是有一些优势。 在原版 TUTOR 及其方言中，创建演示文稿首先要在屏幕上定位光标，然后再输入文本，而我的实现支持格式化输出文本或绘图。文本格式化模板中可以使用字符串或数字表达式插值，还可以包含用于实现颜色、黑白反转等一系列视觉效果的屏幕控制代码。此外还有一种绘制线条的特殊操作符。 这种脚本语言其实是一种包含了数值和字符串计算，以及字符串转换、编辑和匹配等功能的编程语言。由于学生可以按任意形式回答，为了判断学生回答是否正确，字符串匹配功能是必不可少的。该语言还支持 26 个整数变量以及 8 个字符串变量，以及分支判断、循环和子程序等特性。作为 TUTOR 的一门方言，它有专门的运算符实现下列功能：接受学生输入的答案、基于字符串模式匹配的结果跳转到不同分支、前进到下一课、回溯或切换到另一个教案。可以把几个课程脚本组成套装。课程脚本则用内置的全屏编辑器进行编辑。 解释器使用 PDP-11 汇编（MACRO-11）编写。解释器本身占用 3KB 内存，编辑器占用 1.5KB 内存，简单操作系统占用 2KB 内存。BK-0010 个人机主内存剩余的 9.5KB 空间可用于存放课程脚本和其他东西。用户写完课程后，可以删除掉编辑器以将其内存用于课程。 我现在才意识到，上面所描述的脚本语言足以用来编写文字冒险游戏（事实上不止文字，因为它支持绘图）。可惜当时我和我朋友都不知道「文字冒险游戏」这个概念。 当时我写了几个示例课程，并计划移植一些大学开发的现有 TUTOR 课程，但现在看来好像就剩下了解释器代码了，如下示。 几天前（2018 年 9 月），我参加了大学规定的一门关于个人信息处理的线上课程1，由一段视频和十多道选择题组成。我很遗憾地意识到，在 1988 年，在时钟速度只有 3MHz、总内存比现在的电脑小几百万倍的电脑上，我本应编写和学习一些更吸引人的课程。...