站点显示的日期为最后更新日期（是的，我的预期是可以持续更新v）；这篇博文的构成为一些零零散散的想法. 因为没有试图组织成完整严肃的文章，所以会比较措辞上随意一些.

2025.07.03

Monad bind 与 CPS

如何理解 Monad，一种角度是看类型签名，Haskell 中的 Monad type class 定义如下，意思是：属于 Applicative type class 并且提供以下三个函数（>>=, >>, return）实现的 Concrete type m 即属于 Monad type class：

class Applicative m => Monad m where
    (>>=)  :: m a -> (a -> m b) -> m b   
    (>>)   :: m a -> m b -> m b          
    return :: a -> m a                   

今天忽然发现 CPS 和 bind 有隐约的相似性，假设目前我们关心的程序是 $\lambda x. \ x: A \to A$，对 $\lambda x. \ x: A \to A$ 进行 CPS 变换：

$$ [\lambda x. \ x] = \lambda k.\ k (\lambda x.\ \lambda k’.\ \textcolor{blue}{[x]}\ k’) = \lambda k.\ k (\lambda x.\ \lambda k’.\ \textcolor{blue}{(\lambda k_x. k_x\ x)} k’) = \lambda k.\ k (\lambda x.\ \lambda k’.\ k’\ x)$$

假设这个 CPS 变换后的程序的续体（continuation）是 ID 函数（$\lambda x. \ x$），那么我们向程序传递这个续体（正所谓 Continuation Passing Style）：

$$ [\lambda x. \ x] (\lambda x. \ x) = \lambda k.\ k (\lambda x.\ \lambda k’.\ k’\ x) (\lambda x. \ x) = \lambda x.\ \lambda k’.\ k’\ x : \textcolor{red}{A \to (A \to R) \to R}$$

我想说的相似性就在这里了：$A \to (A \to R) \to R$ 和 bind 的类型签名 m a -> (a -> m b) -> m b，他们的共性在于“期待一个结果 $a$ 和一个施加在该结果上的后继操作 $f$，若等待到了此二者，那么把 $f$ 应用到 $a$ 上，计算得到最终结果 $f\ a$”；两者的区别在于 bind 需要做解封装和封装，即将结果从 m （Functor）中提取出来，且最终结果也需要放到 m 中. 根据上述的共性，不妨说 bind 也不失为一种 CPS.

定理证明与解谜游戏的共同点

以“交互”为重要特质；以“顿悟”为爽点（尤里卡时刻）；谜题 $\mapsto$ 命题，解法 $\mapsto$ 证明. 我甚至在想基于定理证明器（+DSL？）设计出某种游戏性是不是可行的，听起来怪怪的，不过类似实践并不少见，比如基于电路电子学的图灵完备（Turing Complete）、基于微积分的微积历险记（Variant: Limits），不禁想问，这究竟是游戏还是考试.

PL & Game

PL 与游戏交叉路口的一些趣闻：(1) The Witness / Braid 制作人 Jonathan Blow 正在开发为游戏开发而设计的语言 JAI；（2）虚幻引擎开发方 Epic 公司的高层 Tim Sweeney 对编程语言很感兴趣，过去许多年都在设计一款自己的语言，后来请了 Haskell 语言的核心设计者 Simon Peyton Jones 来给自己的语言做形式化，相关成果 Verse Calculus 发表在 ICFP'23 上.

2025.06.25

解谜游戏与 Figure

近半年玩了两款解谜游戏，巴别塔圣歌（Chants of Sennaar）和见证者（The Witness），这两个游戏的共性在于玩家需要在图里找规律，我发现这种经验是可以迁移到论文阅读上的，比如浏览到 “As shown in Figure X/Table X, …” 的时候陈述一个字不看直接点击超链接跳转到图标上来就是猜，猜出一个自洽的解释的时候，图表可能也差不多看懂了，不清晰的地方再看看相关陈述.

2025.06.19

CPS: 一个有关承诺的故事

一些参考资料：

1. CMU CS15-150: Lecture 11 Continuation-Passing Style | CMU Principles of Functional Programming M23，讲师：Bradon Wu，语言：SML，概述：CPS 的直觉、如何流程化地对普通递归函数进行CPS变换、有趣的课堂小互动
2. Cornell CS6110 Lecture 13 Continuation-passing style，语言：(Pure) Untyped Lambda Calculus，概述：对最初最简单的 LC 做 CPS 变换
3. Harvard CS152 Lecture 11 References; Continuation passing style，语言：(Applied) Untyped Lambda Calculus，概述：在原始 LC 基础上加了若干新构造子，我觉得更好理解一些
4. SICP §4.3 Variations on a Scheme - Nondeterministic Computing，语言：Scheme，概述：虽然原文没有说 CPS，但内核是 CPS，用 amb 实现非确定编程，可以跟着用 Scheme 自己动手实现一下，我觉得蛮酷的！
5. POPL'25 - The Duality of λ-Abstraction，语言：Simply Typed Lambda Calculus，概述：今年的新文章，驱动我回过头来重新学习 CPS 的动力，这篇文章用 CPS 来描述加入了 co-abstraction 构造子的新 Lambda Calculus 的语义.

• 如果把 CPS 变换看作是从源语言到目标语言的一种翻译，那么 2,3,5 中的源语言是渐次复杂的，5 尤其复杂，因为引入了 co-abstrction，但是 5 描述的是有类型的系统，类型标注解千愁；在 Google 上搜索 “Continuation-Passing Style note” 可以搜到很多名校讲义，选看得懂的看.

CPS (Continuation Passing Style) 是一种编程风格，它的存在宣告了所有的递归函数都可以改造成尾递归的形式（所以可以成为编译器优化的一部分，即尾递归优化）. 我觉得 CPS 变换不是特别好理解，即使它除了基本的 Lambda Calculus 和 Currying，没有引入任何新概念（事实上用已有的工具呈现新思维正是难点所在）.我对 CPS 的理解是，做角色扮演——“假设我是 $\lambda$-term $e$ CPS 进行变换后的结果 ，我接收一个续体 $k$，我向你承诺，我会对 $e$ 进行求值，并且把 $k$ 应用到求值结果上.” 就像递归一样，可以用（递归基+）递归步来正规地理解，但有时候你总是需要一些信念，所谓 recursion leap of faith. 当你有了这个信念之后，你还需要想清楚这个信念的全部细节：(1) 求值 → 什么是值？或者说，你所探讨的系统里，语法规定了哪些表达式可以为值？对于 Pure Lambda Calculus，一般规定 variable 和 abstraction 是值；(2) 求值 → 如何在 CPS 变换中求值？尤其是对于 application ($e_1 e_2$) 的情况.

$$[x] = \lambda k. k\ x$$ $$[\lambda x. e] = \lambda k.\ k\ (\lambda a.\ \lambda k_B. [e]\ k_B)$$ $$[e_1\ e_2] = \lambda k.\ [e_2] (\lambda v.\ [e_1] (\lambda f. f\ v\ k)) $$

“所以，代价是什么？” No Free Lunch.

当你在阅读一篇提出的方法 M 的文章，作者对 M 带来的各种性质的增量会详细描述，你读完可能依然存在一些说不清的疑惑，此刻可以考虑的一个问题是：M 带来了这些好处，那么代价是什么，因为带来某方面的提高，往往意味着让渡其他方面的优越（trade-off，而作者往往不会花太多笔墨在"让渡"的方面），从这个角度思考可以带来一些新的理解. 一些例子：

• LET (Logical Execution Time): 这是实时系统领域的一种编程模型，旨在明确实时任务的逻辑起止时间，规定任务只能在逻辑起点 $S$ 进行输入的读取，在逻辑结束点 E 之后，后继任务可以对前驱任务的输出进行读取，至于 S~E 这段时间里，任务实际上用了多少时间进行计算，我们不关心，它增强了系统的可预测性，因为在这样的设计下，任务（尤其针对周期性任务）的 IO 时机不会抖动（假设 IO 都是瞬时完成的）. 这里可预测性的代价是时间消耗，因为设计 $S$ 和 $E$ 的时候要考虑任务的预估执行时间 $T’$ (WCET, worst-case execution time)，设定 $E, S\ s.t.\ E - S \ge T’$，

• 抽象与性能：这两天群友正好在讨论 Python 的抽象泄露问题，说“现在的高级语言都把指针抽象掉了，但又得让人刻意去记值类型和引用类型的概念，但说到底又还是指针，然而你还是不能直接控制内存”，最彻底的抽象是让程序员完完全全看不到（更不提控制）底下的硬件的，高级语言程序设计初学者往往会被问“知道指针是什么吗”，这个问题很别扭，最彻底的高级语言应该让人看不到指针，如果学的是汇编——那这个问题是合理的，指针不好懂的根本原因在于这个概念穿梭在计算机系统抽象层的界面之间，所以容易造成困惑. 汇编是低级语言；Haskell 这样完全抛弃了指针的是高级语言；C、Rust 这样有明确指针的语言应该叫做中级语言（其实应该是系统编程语言）；那么 Python 这样疑似没指针，又依赖指针的应该叫做中高级语言. 回到 trade-off 的讨论上，因为把硬件抽象掉了，获得了安全，被牺牲的是细粒度的控制，那么性能就降低了. Rust 的零成本抽象，听起来很美好，兼顾了抽象和性能，那代价是什么呢——需要编译器对代码进行优化，即我们需要设计出更好更复杂的编译器.