Andrej Bauer 的 Lecture 2 的笔记。

视频和资料: https://www.cs.uoregon.edu/research/summerschool/summer18/topics.php#Bauer

简介：本次讲座介绍数学（Algebraic theories），可参考文章 What is algebraic about algebraic effects and handlers?

Q1: artiy 是什么

在 Algebraic effects 里，**arity（元数）**指的是：
👉 一个 effect operation 接受多少“输入参数”，以及这些参数的结构是什么。

但它比普通函数的“几个参数”要稍微多一层含义。

1️⃣ 最直观的理解（像函数参数个数）

在最简单的情况下，arity 就是：

一个操作接受几个参数

比如：

read : unit → string
👉 arity = 0（不需要输入）
write : string → unit
👉 arity = 1（需要一个字符串）

这和普通函数的 arity 是一样的。

2️⃣ 在 algebraic effects 里的“完整版含义”

在 algebraic effects 中，一个 operation 通常写成：

op : A → B

这里：

A = 参数类型（input）
B = continuation 的返回类型

👉 所以 arity 本质上是 A 的结构

也就是说：

arity = operation 接受的“参数形状”（type signature 的输入部分）

3️⃣ 更关键的一点：它隐含 continuation

在 effect 理论里，一个 operation 实际上是：

op(a, k)

a : A（参数）
k : B → ...（continuation）

👉 所以更完整地说：

arity 描述的是 operation 在触发时，传入的“参数部分”，不包括 continuation

4️⃣ 举个更贴近 effect 的例子

比如 nondeterminism：

choose : unit → bool

看起来 arity 是 0，但实际运行时：

choose((), k)

handler 可能这样用：

k(true)
k(false)

👉 所以：

arity = unit
continuation 是隐含的，不算在 arity 里

5️⃣ 在代数理论（algebraic theory）里的本源定义

从更数学的角度（universal algebra）：

arity = operation symbol 对应的参数个数（或参数类型）

例如：

+ 是二元（arity 2）
0 是零元（arity 0）

而 algebraic effects 只是把它推广到了：

👉 typed + 带 continuation 的版本

✔️ 一句话总结

在 algebraic effects 中，arity 指的是一个 effect operation 的输入参数类型（不包含 continuation），也就是它“需要多少、什么样的输入”。

如果你是在看 PL 课（比如 algebraic effects + handlers），我可以帮你把：

arity
signature
handler clause

三者之间的关系画一张结构图，这样会更清晰。

带参数的 op：


op: P × |I|^A -> |I|

其中 P 是参数，A 是元数 （arity)

signature $\Sigma$ = { op_i : P ~> A_i }

The free model $Free_T(V)$ is the set of compitations with effects described by theory T and returing values from set V

这是在用 代数理论（algebraic theory）/ 自由模型（free model） 的语言，形式化地定义一个 algebraic effect handler。

你看到的：

一个操作解释 [ [![\mathrm{op}]!]_M ]
和一个返回子句 [ r : V \to |Free_{T’}(V’)| ]

本质上是在说：

“一个 handler 如何处理 effect operation，以及如何处理普通 return 值。”

我一步一步拆开。

1. 整个背景

通常：

(T) 是源 effect signature/theory
(T’) 是目标 theory

handler 会把：

[ Free_T(V) ]

中的 computation，转换成：

[ Free_{T’}(V’) ]

中的 computation。

也就是：

带有效果 T 的程序
        ↓ handler
带有效果 T' 的程序

例如：

State effect
   ↓ handler
纯 computation

或者：

NonDet
   ↓ handler
List effect

2. Free_T(V) 是什么

它表示：

“使用 effect theory (T) 构造的自由 computation”

里面可以有：

return value
effect operations
continuation

比如：

return 3

或者：

choose(x,y)

或者：

get()

等等。

3. handler 需要定义两件事

handler 要告诉我们：

（1）return 怎么处理

这就是：

[ r : V \to |Free_{T’}(V’)| ]

意思：

一个纯返回值 (v \in V)，应该被变成什么 computation。

例如：

return x  ↦  return x

那对应：

[ r(v)=\eta(v) ]

这里 (\eta) 是 monad unit。

例如 state handler 可能：

return x ↦ return (x,s)

于是：

[ r(v)=\text{return }(v,s) ]

4. operation 怎么处理

这是：

[ [![\mathrm{op}]!]_M ]

这里最容易迷糊。

先看 operation 的一般形式：

在 algebraic effects 里，一个 operation 通常长这样：

[ \mathrm{op}: P \rightsquigarrow A ]

意思：

参数集 (P)
返回值集合 (A)

例如：

choose : 1 → Bool

没有参数，返回 bool。

或者：

read : 1 → String

而 operation 在 free model 中，会被解释成：

[ [![\mathrm{op}]!]_M : P \times |M|^A \to |M| ]

这里：

(M) 是某个 model
(|M|) 是底层 carrier set

5. 为什么有 continuation

这最关键。

effect operation 不只是：

op(arg)

它还有：

之后要做什么

也就是 continuation。

因此：

[ |M|^A ]

表示：

operation 的每个可能返回值
↦ 后续 computation

即：

[ k : A \to |M| ]

例如：

x <- choose();
k(x)

continuation 是：

Bool → computation

6. 所以 handler 的 operation clause 是什么

handler 必须告诉你：

当遇到 op 时，如何处理它和 continuation。

即：

[ [![\mathrm{op}]!]_M ]

实际上是在定义：

[ P \times |Free_{T’}(V’)|^A \to |Free_{T’}(V’)| ]

也就是：

给定：

operation 参数
continuation

产生：

新 computation

7. 举个 nondeterminism handler 例子

operation：

[ choose : 1 \rightsquigarrow Bool ]

handler：

choose(k) ↦
  append(k(true), k(false))

这里：

continuation: [ k : Bool \to Free_{T’}(V’) ]

handler 手动调用 continuation 两次：

(k(true))
(k(false))

再组合。

8. 数学上整体是什么意思

所以：

return clause

[ r : V \to |Free_{T’}(V’)| ]

定义：

return value 如何翻译

operation clause

[ [![op]!]_M ]

定义：

effect operation 如何翻译

包括：

operation 参数
continuation 的控制方式

9. 为什么只定义这些就够了

这是自由模型（free model）的 universal property。

因为：

[ Free_T(V) ]

是“由”

return
operations

自由生成的。

所以：

只要定义 generators 如何映射，整个 homomorphism 自动唯一扩展。