效应多态

(Polymorphic Effects)

许多函数的效应都是多态的。例如，map 函数将函数 f 应用于（有限）列表的每个元素。这样，map 的效应就取决于 f 的效应，map 的类型就变成：

map : (xs : list<a>, f : (a) -> e b) -> e list<b>

我们使用单个字母（可能后跟数字）来表示多态类型。这里，map 函数接受一个包含某种类型 a 的元素的列表，以及一个接受类型 a 的元素并返回类型 b 的新元素的函数 f。最终结果是一个包含 b 类型元素的列表。应用函数 e 的效应也被添进了 map 函数本身的效应；事实上，这个函数本身没有其他效应，因为它不会发散，也不会引发异常。

我们可以使用符号 <l|e> 表示 l效应集 与 e效应集 的并集 ，可作为返回类型中效应的允许集（上界），可以l e都有，可以只有l，可以只有e，也可以都没有。

例如，它在 while 函数中使用，其类型为：

while : ( pred : () -> <div|e> bool, action : () -> <div|e> () ) -> <div|e> ()

while 函数接受一个谓词函数（pred）和一个要执行的动作（action），两者都具有效应 <div|e>。事实上，由于 while 可能会根据谓词而发散，因此它的效应必须包括发散。

读者可能会担心 while 的类型会限制谓词和动作必须具有与其完全相同的效应 <div|e> ，而迫使谓词和动作的类型必须标出发散。但其实，在调用方推断效应期间，谓词和动作的效应都会在分析中自动扩展（并不影响谓词、动作本身的效应），直到它们匹配。这确保我们将谓词和动作中的效应结合起来。以下面的循环为例：

fun looptest()
  while { is-odd(srandom-int()) }
    throw("odd")

Koka 推断谓词 odd(srandom-int()) 具有效应 <ndet|e1>，而动作具有效应 <exn|e2>（e1、e2占位指代某些效应）。当应用 while 时，这些效应将统一为类型 <exn,ndet,div|e3>（e3化约前面的e1、e2占位表示某些效应）。