雾雨魔法店

缘起 由于知乎近期（2024 年）对未登录用户访问权限、搜索引擎索引的更改及社区环境的变化， 知乎已经不再适合作为 PL 以及函数式编程知识的公开分享站。为了保证知识的公开和 流通，本站作为雾雨魔法店面向互联网的新站点建立， 同时也作为同名知乎专栏的镜像站点存在。 投稿 除了作为现有专栏的镜像外，本站也接受新文章投稿。 目前提交文章需要向站点 repo 中提交 PR 或者向维护者发送 patch，具体流程请参照 repo 中的 README.md。 未来本站会提供更加便捷的投稿方式。

什么是维稳算法？ 维稳算法(Order Maintenance)是儒家思想君君臣臣的集大成者 - 这个算法使我们可以拿取任意两个事物，然后进行一个全序比较。 换言之，Order Maintenance可以看成一个链表，但是链表的所有元素直接可以快速比较前后。 也就是说，OM带有以下三个api： Head(): OM，取得链表头 Create(before:OM):OM，在before后插入一个节点 <=(lhs: OM, rhs: OM): bool，判断lhs是否在rhs的前面 OM的实现不是这篇文章的重点，就放在Order Maintenance - Google Slide这里了。 最近工作中发现了动态LCA（给予一棵树，处理树上的修改穿插着LCA查询）可以用OM解决。 另外碎碎念：Order Maintenance在Incremental Computing，Persistent Data Structure，跟String Algorithm上面都有应用，已经属于我走到那跟到那的变态跟踪狂了，下头算法！必须告它性骚扰！ 一般来说，这个问题可以用link cut tree解决，两者复杂度一样，但是思路跟工具都不一样。特别是用到了维稳算法！维稳算法解动态LCA也有各种各样的extension，比如魔改一下可以用来增量维护binding in lambda calculus。 具体操作如下： 我们可以给树的每个节点一个OM区间，并且用preorder traversal进出时间维护区间开闭。 具体操作是，给一颗新的树，我们可以维护一个OM timer。此timer在traversal递归进/出的时候会各进行一次自增，并且用自增前的两个值来初始化OM区间。这样，所有OM值都是独一无二的，并且树的区间包含子树的区间。同时，无直系亲属关系的两节点区间不相交。 新加入的叶子节点的区间可以用兄或（如果兄不存在）父的区间右端点连续插入两个值初始化。 我们维护一个装着区间的平衡二叉树。区间的序是左端点的序，而BST每一节点储存"该BST子树的最大右端点"。 这时候，找寻多个节点的LCA，成为了‘找寻最大的（左端点最右），包含所有节点区间的区间’。 这可以分两步完成： 0：去除所有不够左的左端点。由于是暂时的，我们不需维护平衡性，只需维护子树最大右端点，所以是O(log(n)) 1：在所有右端点足够右的子树里，寻找最右的左端点。 具体操作是： 当右子树子树最大右端点足够大的时候，递归进去。 否则，如果当下节点右端点足够大，返回。 否则，左子树子树最大右端点足够大，递归进去。 这是log(n)，跟link cut tree大O一样（但我认为更好懂也更优雅！） 另外顺带一提：Edward Kmett对这个问题的函数式特化版做了一个改进，达到了O(log(height))，见 On-line Lowest Common Ancestor

https://github.com/taimoon/scheme-compiler 关于一个业余如何另辟蹊径，作弊，逆练功法以及一些心得 前传 实际上，在真正写可以自举的编译器之前，我写了至少两个编译器，以及无数个解释器。 第一次，nand2tetris project写hack处理器汇编器，VM汇编器，Jack编译器。当时我还很懵懂，掌握不到其中的办法论。 第二次，IU Compiler课程学写python优化编译器，包括寄存器分配，尾递归，闭包。 这课程对我影响深远，让我找到适合我这种业余的办法论。 某天，看到某博客的编译器教学， https://generalproblem.net/lets_build_a_compiler/01-starting-out/。 得以让我可以不依赖教学提供的工具，写一个“hello world”式编译器来作为开头。誒，万事开头难啊。 可惜，那位博客并没有更新更多内容，不过博客主要参考Abdulaziz Ghuloum的“An Incremental Approach to Compiler Construction”论文，所以我以同样论文作为我主要参考，继续我的开发。 如果读者对其他语言编译器教学实现有兴趣，但又循序渐进式地实现，可以参考可自举C编译器实现 https://github.com/rui314/chibicc。 那位大大也有相关博客 https://www.sigbus.info/how-i-wrote-a-self-hosting-c-compiler-in-40-days。 办法论 前提提要,前文说到IU Compiler课程对我影响深远是因为… 首先，IU Compiler课程设计继承至Abdulaziz Ghuloum的“An Incremental Approach to Compiler Construction”论文。 核心是incremental, 循序渐进式来学习编译器实现。 你的征程始于一个可以打印整数的编译器。 好了，你已经有了一个编译器，然后一点一点扩展你的编译器。 每一次的提交都要确保之前测试都能通过，还有新测试，以保证你的编译器可以work。 换一种说法就是你会写很多个编译器，厉害吧？给自己鼓掌；听懂，掌声！ 其次，IU Compiler课程采用对新手非常友好的nanopass架构。 在nanopass架构下，编译器会同过多个pass一步一步变换源码直到输出最后汇编，而每一个pass只做非常简单的事情。 比如一个pass来做free variable分析, 下一个pass才做闭包变换，然后下一个pass才限制函数参数。 这是一个很好办法论：如果一个编译步骤太难，就拆开成两个步骤。 可能有的同学会说，这不是会造成多次遍历，更长编译时间？ 新手嘛，更何况我一个业余，主打能work就可以，不寒碜。酷炫的东西比如SSA, 输出LLVM IR, 寄存器分配, 优化可以以后再打算。 不过，别灰心，nanopass被认可的工业优化编译器实现方式。 (详见:A nanopass framework for commercial compiler development) nanopass framework的chez scheme编译是可以非常快哒。传说，chez scheme几秒内就可以完成自身编译。 新手嘛，主打一个能work就好。 Parser generator我又不是很会，pratt parser, parser combinator, 就不明觉厉的感觉。 考虑到什么ambiguous grammar, associativity, precendence, 等等等， 让我手写parser可能会要我的命。 解析难的语言比如有layout syntax的haskell, python, 更不要说C++这种怪物， 自然不会是我考虑范围内。...

原文：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....