编程语言理论

我们在上一篇文章中，描述了一个通用的优化技术： 找到时间差，把数据分成已知跟未知，并且用代码表示后者。 但是，这种做法有两个问题： 0 - 你需要费时费力去整这个东东，而且不是所有时候都能刚刚好复用代码。 1 - 如果我们预先不知道应该怎么区分呢？甚至，如果这是动态的呢？假设我们先接受一半的数据，等一会，然后接受另一半，那我们如何用上述的技巧？难不成把所有可能的分法都预先写一遍？ 所以，我们希望把上述技术，staging，自动化掉，使得程序员不再需要去关心之。 我们应该怎么做呢? 我们先从最基本的开始，先决定要操作的语言吧： type expr = | Var of string | Int of int | Add of (expr * expr) | Mult of (expr * expr) 这个语言，简单到了极点，只剩下+跟*两个操作了。别担心，我们会一步步扩展这个语言。 module ENV = Map.Make(String) let rec eval (e : int ENV.t) : expr -> int = function | Var v -> ENV.find v e | Int i -> i | Add (x, y) -> eval e x + eval e y | Mult (x, y) -> eval e x * eval e y 这是一个标准的definitional interpreter实现，中规中矩，并没任何出彩的地方。...

我们先从一个很简单的算法，快速幂，开始看起吧： let rec quick_mod x y m = if y = 0 then 1 else if y mod 2 = 1 then (x * (quick_mod x (y - 1) m) mod m) else quick_mod ((x * x) mod m) (y / 2) m let example_0 = quick_mod 10 1000 3 显而易见，10的n次方除3都会余1： utop # example_0;; - : int = 1 这个算法试图在y很大的时候，算(x^y) mod m。 很明显，这个算法只会进行log y次’*然后mod’的操作 - 我们把这个操作定义为⊕吧。 我们去深入思考一下 - 为什么本来要进行y次⊕，现在，我们只需要进行log y次⊕？...

有趣的CS已经很久没动了。有外因跟内因。 外因是一直在忙，忙着准备OOPSLA的talk，忙着给talk，OOPSLA过后忙着做下一个project，就慢慢把这个忘了 内因是因为知识消耗得差不多了 - 有趣有用而且没基础本科生又能听懂的接近PL的内容。。。实在不怎么多 但是最近要给一些关于Partial Evaluation的talk，所以就随便写点吧。

别急！ 别急！ 我们先别急着切入正文，而是先看看一道算法题： 圆角骑士魔理沙：数组多次取第X大元素 大家在评论区可以看到，这道题有一定的难度：不少人给出了错误，或者超时的答案。 尽管最高赞给出的答案的确是正确的，其实有一个简单很多的做法： 对N生成二叉搜索树，然后用M索引之。 等下，这不是O(n log n)的吗？ 所以才说别急！我们想一想，当M < N的时候，这个二叉树，并不是所有节点，都会被索引。 那，我们为什么要去把不会被用的二叉树部分构建出来捏？ 但是，我们怎么知道‘树的那一部分会被用上’？ 答案是，我们可以同时交叉构建树跟索引树的过程 - 默认情况下，树是没构建的。当我们索引没被构建过的树，我们会构建这里的最小一部分，然后保存下结果，再进行构建。 class LazyBST: def __init__(self, arr): self.constructed = False self.arr = arr self.size = len(arr) def idx(self, index): if not self.constructed: self.constructed = True self.head = self.arr[0] self.left = LazyBST([x for x in self.arr[1:] if x <= self.head]) self.right = LazyBST([x for x in self.arr[1:] if x > self.head]) if index < self....

最近都在参加Splash/OOPSLA，就暂停了有趣的CS系列。 再过几天就回盐湖城了，今天也有点空，于是就写一写一些感想。 这某种意义上是我的第0个conference - 我以前参加过一次PLDI，但那是本科，也没给报告，也参加过一次ICLR，但那是virtual，而且给了报告，poster没啥人听，就相当于傻站了一个小时 我觉得最大感想，就是累 - 从离开盐湖城，到大概几天后回到盐湖城，我参加了几乎整整两周的会议+traveling。 travel的时候在飞机上或者在机场或者在车上，难以休息，到了会议早上要听报告听到黄昏，途中还穿插着社交 - 而社交很多时候都是一对一或者多对一交流工作跟idea，往往比单纯听报告还劳累。 不得不感叹，体力还是很重要的，而由于我太宅，体力好差，甚至怀疑比不上我认识的一个50多岁的教授，衰，希望可以慢慢锻炼改善。 另一个发现的短板是，口才不行。由于New Zeland（OOPSLA举行的地方）旁边就是ANU/Google Sydney，他们做的东东刚刚好也跟我做的有交集，所以我也过去宣传了一下我的工作。一般来说，我导师都会跟着去，跟其他人connect，也会帮忙回答各种问题。今天在Google Sydney宣传的时候导师在坐飞机，而且得到了一些关键问题，于是我就当机了，进入对对对模式，也可能会对后续落地有影响。如果有导师在解围，估计会好很多，但是这并不是知识差距 - 在project相关知识上我们俩知道的基本上一样，甚至我应该还多一些。这就是我没这个随机应变的能力。这就有点头疼，毕竟体力差可以去运动场找回来，但这样的报告机会差不多一年才有一次。 不过说点更正面的！我去了动物园！看到了kiwi！还有emu，摸起来毛茸茸的，也不知道躲！还摸了鳗鱼，很冷，所以就是冻鳗了！我从今以后，就是冻鳗高手了！！！ OK，说回正事，talk好像挺可以的，有很多人喜欢，而且结识了很多圈内人，好像都觉得工作挺有价值的。甚至，在visit ANU的时候，我们pair program成功在mmtk里面弄出了工作的hacky prototype。也跟做memory allocator的人讨论讨论了，可能可以用在这些地方。不得不说Steve的眼光真是毒辣，他arrange了一个跟allocator maintainer的meeting，说了下可能用得上，还真猜中了。 另一个重要的事情是，超人也会流血。在oopsla/澳大利亚，我近距离接触了一些以前只能在教科书跟经典paper上看到的人物，而这过程中我认为它们更像走在前面的前辈，是普普通通的人，而不是一种‘神话生物’。诚然，我能力跟各种做教授年龄比我存在年龄还大的人对比，有很大差距，但我认为这差距可以随时间缩小甚至填补。 甚至，我还看了一个著名教授做了一个。。。烂活。如果你挡着名字跟会议，我还会以为是各种奇怪workshop的新人论文。某种意义上，这反而很有价值（笑）。（当然，请大家别猜是谁，我还想活） 另外，跟各种教授还有工业界的人聊了聊以后，再去了次Google以后，对做教授或者去工业界的抗拒度降低了，其实还行，挺好的。当然，如果能被富婆包养就最好了，这样就可以一心做research，不考虑什么教书什么grant，也比工业界有更多自由，想做什么做什么。如果大家认识富婆，可以介绍介绍给我！ 至于看了什么talk? 跟人闲聊的时候学到了probabilistic separation logic，很漂亮。在普通的分离逻辑里面，magic wand代表的是两段内存没有交集，而在probabilistic separation logic里面，表示的是两个概率分布独立！ 而我认为最有意思的talk，是Deciding program properties via complete abstractions on bounded domains。简单的说，就是在一定条件下，有loop, ifelse, assignment的语言里面抽象解释可以是complete的，而且这个completeness是composable的 - 就是说只要对ifelse/assignment complete，也会自动对loop complete。以前没怎么见过这样的工作。 明天还有meeting跟socialize，睡觉。

“Show me your flowchart and conceal your tables, and I shall continue to be mystified. Show me your tables, and I won’t usually need your flowchart; it’ll be obvious.” – Fred Brooks, The Mythical Man Month (1975) 吐槽一下，最近手指好疼，怀疑打字打太多了，等下有空看看医生，orz 我们先看这一个著名的笑话： 三个程序员被要求穿过一片田地，到达另一侧的房子。 菜鸟程序员目测了一下之间很短的距离，说：“不远！我只要十分钟。” 资深程序员看了一眼田地，想了一会，说：“我应该能在一天内过去。”菜鸟程序员很惊讶。 大神程序员看了一眼田地，说：“看起来要十分钟，但我觉得十五分钟应该够了。” 资深程序员冷笑了一声。 菜鸟程序员出发了，但只过了一会，地雷爆炸了，炸出了巨大的洞。这下他必须偏移预定的路线，原路返回，反复尝试穿过田地。最后他花了两天到达目的地，到的时候颤颤发抖，还受了伤。 资深程序员一出发就匍匐前进，仔细地拍打地面，寻找地雷，只有在安全的时候才前进。他在一天的时间内小心谨慎地缓慢爬过了这片地，只触发了几个地雷。 大神程序员出发之后径直穿过了田地，十分果断。他只用了十分钟就到了另一边。 “你是怎么做到的？”另外两个人问道，“那些地雷怎么没有伤到你？” “很简单，”他回答道，“我最初就没有埋地雷。” 一般来说，我们写程序，都是这样的步骤： 0：写出程序 1：写测试 2：通过测试查找错误，回到0修补，如果没发生问题就假装程序写好了 这时候有一个很大的问题：debug是一个很麻烦的过程，而且debug后不代表程序没有问题，只代表了程序在这些测试上没有问题（所以你还要牢费心力找测试）。更严重的问题是，在多线程或者分布式系统里面，同一段代码同一段输入，问题是概率性的：有可能会发生，也有可能不会发生。更更糟糕的一点 - 这些分布式代码，比如paxos的实现，往往是最核心的代码，当这些代码发生问题后，会带垮整个服务器集群，造成巨大的损失。 但是，为什么我们要劳心劳力的去debug？我们不把错误放进程序，不就好了？ 或者，我们更进一步，为什么要写程序？把程序种子埋土里，然后过几天等程序长大了，就收掉，不就行了？ 你先别笑，这的确是编写复杂程序的一个方法。 更具体的说，当我们程序运行到一半，假设我们随机修改一下变量的值，很明显程序不会没问题的继续运行下去。 比如说，如果我们在写一个二叉搜索树，当我们运行的时候，把一颗树的最左节点跟最右节点交换了，那接下来可能会找不到需要的值。 也就是说，我们的程序需要遵守一定的规则(invariant)。对于上面的例子来说，我们需要遵守的invariant是，一个二叉树的左边的所有节点小于等于自身，自身小于等于右边的所有节点。 所以，我们写程序的时候，要保证这些invariant的正确性。但是，我们可以反过来，从这些invariant，推导出一个程序！ 更具体的说，我们 0 - 写下程序输入跟输出符合的条件，一般来说，输入的条件并不等价于输出的条件，所以这时候，这两个条件之间，是有一个空缺的 1 - 根据这些规则，猜出一小段代码，这些代码会把这些空缺变得更小，然后我们不停进行这个操作，直到空缺消失。这时候，程序就编写完成了。...

想了想，最后还是觉得应该用这篇paper开头。 什么是Defunctionalization? 简单的来说，Defunctionalization是一个程序变换。更具体的说，Defunctionalization接受一个高阶编程语言的程序，输出一个一阶编程语言的程序。这通过一下变换完成。 创建一个代数数据类型，lam，跟创建一个函数apply: (lam * Any) -> Any（是的，naive的Defunctionalization并不类型安全） 对于所有a -> b类型作为一等公民（不是直接调用）出现的地方，把类型a -> b变换成lam。 对于所有构建闭包的地方，创建一个新的lam构造子。这个构造子的成员就是这个闭包捕获的变量。 同时，在apply函数内，给出该lam构造子的实现 - 而这实现照抄原closure的body。 对所有调用闭包f x的地方，改为apply (f, x)。 举个例子，假如我们有以下代码， (* aux : int * (int -> int) -> int *) fun aux (i, f) = f i (* main = fn : int * int list -> int list *) fun main (i, js) = let fun walk nil = nil | walk (j :: js) = (aux (i, fn i => i + j)) :: (walk js) in walk js end Defunctionalize后，会成为...

第二节： Spore：【译】shift/reset 编程入门 (2)：应用 3 Delimited Continuation 操作符的理论基础 本节对 delimited continuation 操作符 shift/reset 的理论基础进行概述。我们使用的语言是一个从左到右求值1的 call-by-value λ 演算，并加入了多态的 let 和 shift/reset 操作符。 3.1 语法 $$\begin{alignat}{1} \text{(value)}& \quad V& \quad::=&\quad x \ | \ \lambda x. M \\ \text{(term)}& \quad M& \quad::=&\quad V \ | \ M~M \ | \ \mathsf{let}~x = M~\mathsf{in}~M \ | \ \mathcal{S}k.M \ | \ \langle M \rangle \\ \text{(pure evaluation context)}& \quad F& \quad::=&\quad [~] \ | \ F~M \ | \ V~F \ | \ \mathsf{let}~x = F~\mathsf{in}~M \\ \text{(evaluation context)}& \quad E& \quad::= &\quad [~] \ | \ E~M \ | \ V~E \ | \ \mathsf{let}~x = E~\mathsf{in}~M \ | \ \langle E \rangle \end{alignat} \\$$其中，shift (fun k -> M) 记作 $\mathcal{S}k....

0 译者前言 本文译自浅井健一先生的《shift/reset プログラミング入門（Introduction to Programming with Shift and Reset）》。找了一圈之后发现整个知乎上都没人教怎么使用 delimited continuation，遂翻译。 一些说明： 虽然文中说有任意函数式编程语言的经验即可，但例子和练习题用的是一个 Caml 变体，所以想要获得最佳阅读体验还是要了解 OCaml 或其他 ML 系编程语言的基础语法。 Rust 不算。 译文同时参考日语和英语版本，两版本如有不同则以正确/易懂一方为准。 部分译者的评论或解释用〔〕标注。原文的引用和注释则尽量还原（但由于知乎的限制只能混在一起了）。 译者翻译相关文献的经验并不丰富，如有任何错漏或可改进处请务必指出。 接下来开始正文内容。 摘要 Continuation 是在各种编程语言中都普遍存在的概念。条件语句是根据条件从两个 continuation（未来）中选择一个的操作，异常则可看作是丢弃一部分 continuation 的操作。还有，尾调用（goto 语句）就是执行 continuation 的操作。尽管 continuation 是这样一个无处不在的、十分自然的概念，目前为止，显式地使用 continuation 编程仍然一直被认为是困难的。 本教程使用 delimited continuation 操作符 shift 和 reset 来演示如何显式地使用 continuation，从零开始讲解关于 continuation 的基础知识，并在过程中指导读者实现简单的协程和非确定性搜索。本教程同时也能作为 CW 2011 演讲内容的引子。 本教程需要读者熟悉 OCaml、Standard ML、Scheme 或 Haskell 等函数式编程语言，但不需要读者在阅读本文前有任何有关 continuation 的知识。教程中穿插了各种练习问题，推荐读者随读随做。 1 引言 Continuation 就是表示「之后的计算」的概念。它可以看作是异常处理的一种推广，但远比异常处理要强力。实现复杂的计算时，实现者有时会发现需要使用在通常的程序结构中难以写出的控制结构。如果能操作 continuation，则可以在不影响程序整体可读性的前提下实现它们。 想要显式地使用 continuation，一种传统的方式是对整个程序进行 CPS1变换〔continuation passing style，指把 continuation 作为参数显式传递的编程风格〕，但这样就不能保留程序的原有结构。为了在引入 continuation 的同时保持程序的正常结构，我们就需要使用 continuation 操作符。...

第一节： Spore：【译】shift/reset 编程入门 (0)&(1)：前言和概述 2 shift/reset 编程 2.1 什么是 Continuation Continuation，简而言之就是「之后的计算」。程序的执行过程就是选出要执行的部分（称作 redex〔reducible expression，可归约表达式〕），对它求值，再使用它的结果来进行之后的计算。这里的「之后的计算」就是指 continuation。因此，continuation 是任何程序执行时都存在的基本概念。 为了展示 continuation 具体是什么，我们用 $[\,... ]$（称作 hole）来表示一段程序接下来要执行的部分。比如 $3 + 5 * 2 - 1$ 这一算式中，如果接下来要执行的部分是 $5 * 2$ 的话就可以写作 $3 + [5 * 2] - 1$，而这时的 continuation 就是 $3 + [~\cdot~] - 1$。总之，得到 $[~\cdot~]$ 的值（$5 * 2$ 的结果 $10$）之后，「给这个得到的结果加上 $3$ 减去 $1$」就是整个式子当前的 continuation。从「接受 hole 的值之后用它进行计算」这方面来看，continuation 和函数是相似的。 也可以用「抛出异常时扔掉的那部分程序」来看待 continuation。例如，把上述例子中 $[~\cdot~]$ 的部分换成 raise Abort，让它抛出异常，这时候被抛弃的部分 $3 + [~\cdot~] - 1$ 就是 continuation。...