效应的语义
(Semantics of Effects)
推断得到的效应并非仅仅被视为函数上附带的额外类型信息。恰恰相反，通过效应推断，Koka 与其指称语义之间建立了极强的联系。具体而言，Koka 函数的完整类型，直接对应于描述其指称语义的那个数学函数的类型签名。例如，用 〚t〛 表示将类型 t 翻译成其对应的数学类型签名，则有：
〚int -> total int〛 | = | \(\mathbb{Z}\to\mathbb{Z}\) |
〚int -> exn int〛 | = | \(\mathbb{Z}\to(\mathbb{Z}+1)\) |
〚int -> pure int〛 | = | \(\mathbb{Z}\to(\mathbb{Z}+1)_{\bot}\) |
〚int -> <st<h>,pure> int〛 | = | \((\mathbb{Z}\times\mathbb{H})\to((\mathbb{Z}+1)\times\mathbb{H})_{\bot}\) |
📌 注意第二行：exn 在数学上对应 \(\mathbb{Z}+1\)，即“ℤ（正常整数）在左，1（异常）在右，”。这是 Koka 论文里的标准约定——ℤ 代表正常的整数结果；1 代表单位类型（只有唯一值 <>），充当“出错了”的标记。两者用 + 连接，构成和类型（Sum Type）。
要读懂这张表，关键是了解两个数学符号：τ 、1，以及它们的和 τ + 1。
τ：普通的结果类型
τ 是一个类型变量，代表函数正常执行时返回的数据类型。在上面的例子里 τ = ℤ（整数），但实际可以是 string、bool、自定义数据结构等等。换句话说，τ 就是“如果没有发生意外，函数会给你什么”。
1：单位类型，在这里充当“异常”标记
在数学和类型论中，1 表示单位类型（Unit Type）——它里面只有一个可能的值（通常记作 <> 或 ()）。因为它不携带任何信息，正好适合用来表示“程序没有返回正常值，而是中途出错了”。
所以在 Koka 的语义翻译中，1 被定义为异常（exception）的标志。一个函数若具有 exn 效应，意味着它可能不返回 τ，而是返回一个 1。
τ + 1：和类型，“要么正常值，要么异常”
在这里是类型论中的和类型（Sum Type，也叫 coproduct）。τ + 1 的含义是：这个值要么是左边的 τ（即正常的返回值），要么是右边的 1（即发生了异常）。
为什么需要“和类型”
关键问题来了：一个 exn 函数执行完后，调用方拿到的到底是什么？
如果函数正常算出了 42，调用方当然希望拿到 42；但如果函数抛出了异常，调用方拿到的就不是整数，而是一个“出错了”的信号。问题在于——单看 42 这个值本身，你无法区分它是“正常结果”还是“某种特殊编码”。
所以数学上不能简单地让函数返回 \(\mathbb{Z}\)，而要让它返回一个更胖的类型 \(\mathbb{Z}+1\)：这个类型的值要么来自左边（正常整数），要么来自右边（异常）。这样一来，“函数是正常返回的还是异常退出的”这个信息就被编码进了类型本身。
如何构造一个 \(\mathbb{Z}+1\) 的值？引入 inl 和 inr
既然 \(\mathbb{Z}+1\) 的值有两种来源，我们就需要两个构造子（constructor）来给值“贴标签”，标明它到底来自哪一支：
inl（inject left）：把左边类型的值包成和类型，意为“我是左支来的”inr（inject right）：把右边类型的值包成和类型，意为“我是右支来的”
Tip
注意Koka语言本身没有 inl / inr 这种固定名字的二元注入构造子，它们在某些别的语言的类型论文献中是标准的数学记号，在这里只是为了阐释方便。inl 和 inr 不是普通函数调用，它们是类型构造子——作用是“包装 + 贴标签”，让一个裸值在类型层面明确归属于和类型的某一支。在 Koka 中，用户可以使用 Alternatives（或者叫做联合类型(Unions)） 自定义类似和类型的构造子。
套用到 \(\mathbb{Z}+1\)：
当函数正常返回 42 时，它返回 inl(42)——把整数 42 用 inr 包起来，贴上“左支/正常”的标签
当函数抛出异常时，它返回 inr(<>)——把单位类型的唯一值 <> 用 inl 包起来，贴上“右支/异常”的标签
举个具体例子，int -> exn int被翻译成 \(\mathbb{Z}\to(\mathbb{Z}+1)\)，意思是：
函数接受一个整数∈ \(\mathbb{Z}\)
返回一个元素∈ \(\mathbb{Z}+1\)：
- 如果一切正常 → 返回左侧注入的 inr(42)（即正常的整数结果）
- 如果抛出了异常 → 返回右侧注入的 inl(<>)（即单位值，表示“出错了”）
这种“用 τ + 1 表示可选值”的用法在类型论里很经典——它等价于其他语言里的 Maybe τ 或 Option τ。
⊥：非终止
下标 ⊥ 来自域理论，表示“函数可能永远计算下去、不返回”。这正是 div（divergence，发散）效应的语义。pure = <exn, div>，所以 int -> pure int 翻译成 \(\mathbb{Z}\to(\mathbb{Z}+1)\)⊥ ，意思是：函数要么发散（对应 ⊥），要么返回一个“整数或异常”。
\(\mathbb{H} × τ\)：积类型，为“有状态”建模
× 是积类型（Product Type），表示“成对出现”。\(\mathbb{H}\) 代表堆（Heap）。
当一个函数有 stint -> <st\<h\>,pure> int 的翻译是：\((\mathbb{Z}\times\mathbb{H})\to((\mathbb{Z}+1)\times\mathbb{H})_{\bot}\)
读起来就是：函数接受一个整数和一个初始堆，然后要么永远算下去（⊥），要么返回一个“新堆 + （整数或异常）”的对。
这张对应表告诉了我们什么
把上面四行放在一起看，会得到几个非常清晰的结论：
total函数在数学意义上是真正的全函数——给什么输入必定得到什么输出，没有任何副作用。exn函数可能在正常结果和异常之间二选一，对应数学上的 \(\mathbb{Z}+1\)。pure函数（Haskell 意义上的“纯”）既可能抛异常，也可能不终止，对应 \((\mathbb{Z}+1)_\bot\)。st<h>函数除了上述可能性，还要读写堆，所以输入输出都要带上堆：\(\mathbb{H}\) 进，\(\mathbb{H}\) 出。
我们相信这种语义对应是完整效应类型的真正力量，它使程序员能够对代码进行有效的等式推理。对于几乎所有其他现有的编程语言，即使是最基本的语义也会立即包含复杂的效应，例如堆操作和发散。相比之下，Koka 允许分层语义，我们可以轻松地分离出行为良好的部分，这对于许多领域至关重要，例如安全 LINQ 查询、并行任务、分层、沙盒移动代码等。