姬世略译文集

译自 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、总内存比现在的电脑小几百万倍的电脑上，我本应编写和学习一些更吸引人的课程。...

译自 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" 可以生成有六条杠的字符串 "||||||"。该代码还打印了重写过程中触发的所有规则以及对应生成的中间结果，以展示这一巧妙算法的工作原理。...

译自 R-Techonology。除非特殊声明，下文中「我」指原文作者 Oleg Kiselyov。 「R-技术（R-Technology）」是一种设计和图形化表示程序的方法，由 V.M. Glushkov 领导的基辅控制论研究所开发。该技术是自 20 世纪 50 年代末及 60 年代初，苏联弹道导弹和后来的太空火箭的航空电子软件设计中发展起来的。（有趣的是，大约二十年后，David Harel 在担任以色列飞机工业公司航空电子软件工程顾问时，发明了一种相当类似的技术－－Harel 状态图。）Glushkov 研究所大量使用并推广 R-技术 ：据说他们在该领域发表了 600 多篇论文（大部份是俄语的），就这一主题举办了三次全联盟会议和一次国际会议。它们甚至把 R-技术 标准化了－－R-chart，ISO/IEC 8631。 20 世纪 80 年代初，我从控制论研究所研究人员出版的几本书和发表的几篇文章中了解到了 R-技术。Glushkov 研究所出版的所有东西都给人一种和 R-技术 有关的印象。我还记得当时看到了画在一张大纸上的完整 Pascal 编译器的图表（R-图表）。 R-技术 基于一种描绘程序控制流的图表。节点是程序的状态，有向边（弧）代表状态转换。弧的上下方都有文字或图形的注释，上方代表转移条件/守卫（guard），下方则描述了该弧将要执行的动作（action），弧是水平的线条。当程序处于特定状态时，我们从上到下查找对应转移条件为真的弧，并执行弧表示的操作，然后把程序状态更新为弧的目标节点。R-技术 与流程图密切相关，不过流程图中的一个节点在 R-技术 图表中是一条带有注释的弧（在 Harel 的状态图中也是如此）。我们称 R-技术 图表为 R-图表，它所描述的抽象机器/自动机则称为 R-机器 或者 R-tran（RTRAN）。 上面对 R-机器 的描述可能会令人联想到状态机。这种相似性并非偶然：Glushkov 是著名的自动机理论研究者，他第一个提出了把正则表达式转化为非确定性有限自动机的算法，还撰写了《Synthesis of Digital Automata》（该著作为他带来了列宁奖和苏联科学院院士资格）。与有限状态自动机不同的是，R-机器 转换状态的条件可以不只是对输入的测试，可以是任意复杂的。稍后可以看到一个例子：那 R-机器 名义上只有两个状态，但它还有可变状态，其动作会更新可变状态，因此实际状态的数量是无限制的。在我看来，R-机器 看起来总是像图灵机，但 R-机器「控制」实际事物，其动作不仅是读写和移动磁带。 通常把 R-技术 图表绘制成图像，因此也称该技术为可视化编程技术。不过，用（风格化的）纯文本表示图表也是可行的。我记得在某本书中看到表示 R-程序 的表格，看起来有点像 FORTRAN 或 COBOL 程序输入到打孔机上打孔的样子。表格有四列，分别是当前状态标签、转移条件、动作和目标状态标签。可以按以下方法输入 R-程序：...