Keyboard shortcuts

Press ← or → to navigate between chapters

Press S or / to search in the book

Press ? to show this help

Press Esc to hide this help

引入

该教程基于Koka语言官方英文文档

Koka version v3.2.3

基础知识

(Basics)

Hello world!

函数定义

函数用fun关键字声明，声明的同时必须写出函数体，进行完整定义

以 main函数 为 程序入口，打印输出 Hello world!：

fun main() {
  println("Hello world!") // println output
}

这是使用 显式大括号 的写法

由于 “大括号省略” (brace elision) 规则，
当下一行有 更深缩进 时，
编译器预处理会 自动用花括号包裹 下一行所在的整个缩进块。
也就是说，以上示例也可以写为

fun main()
  println("Hello world!") // println output

koka编译器 不关心 缩进所用具体空格数，只看 是否比上一行深。
你可以使用 任意数量空格 完成 更深的缩进，需保证 对应逻辑行同深度缩进。

不论用 7个空格 还是 1个空格 进行缩进，在以下位置都是合法的，且不影响编译器的分析：

fun main()
       println("Hello world!") // 7空格缩进
fun foo()
 println("bar") // 1空格缩进

函数的参数、返回值用 :T 标明类型

fun main()
  println(add1(1,2))
fun add1(a:int,b:int):int
  add2(a,b) // 语句
fun add2(a:int,b:int):int
  a+b // 表达式

在 Koka 里，函数定义通常不分前后——你可以在 main 里调用一个在后面才定义的函数，编译器不会报错。Koka 把一个 .kk 文件看作一个模块，模块内所有顶层 fun 声明在类型检查阶段对整个模块可见。编译器先做声明收集，把所有函数名及其类型签名登记到符号表，然后再做类型推断与检查。所以无论书写顺序如何，调用方都能找到被调用方。
在函数体内部，用 fun 定义的局部函数遵循“先定义后使用“的顺序——因为局部作用域是语句序列，按顺序执行。如果你在局部作用域里前向引用一个局部 fun，通常会报错。

部分语法产生式：

funbody   → funparam blockexpr
blockexpr → expr (块(block)被解释为一系列语句(statements))
expr      → withexpr 	
              block (被解释为空参匿名函数fn(){...})
              returnexpr
              valexpr
              basicexpr
block     → [{] semis { statement semi } [}]
...

函数里的 最后一个表达式的值 可作为 函数的返回值
语句在语法上可规约到表达式，所以
函数里的 最后一个语句的结果 可作为 函数的返回值
你也可以显式地使用 return 关键字来返回

变量定义

val a=foo+bar()
val foo=123
fun bar()
  var baz:=100
  baz
fun main()
  val bar=456
  var baz:=789
  baz:=0
  println(a+bar+baz)

Koka的变量都必须在声明的同时绑定一个初值——没有“先声明、后赋值“这种写法。
顶层只能使用 val 定义静态值，是一种不可变绑定，整个模块可见，右值不要求是“编译期可计算“的常量表达式，使用与定义的行顺序无关。

代码块内既可以 使用 val 定义静态值：val [value_name]=[expr]
也可以 用 var 定义有可变引用的变量：var [variable_name]:=[expr]
但是先定义后使用，具有块级作用域
变量通过 [variable_name]:=[expr] 赋值

点表示法

(Dot Notation)

区别于面向对象语言，函数和数据是Koka的核心。

点表示法很直观，方便将多个函数调用链接在一起形成链式调用：

fun showit( s : string )
  s.encode(3).count.println

s.encode(3)并不是选择了对象下的encode方法，而是encode(s,3)的语法糖，后者将s写为第一个显式参数。
类似地，c.int 等效于 int(c)，将一个字符转换成整型。

println(count(encode(s,3)))

这是s.encode(3).count.println的脱糖写法。

将点表示法设计为函数调用的语法糖有一优点：

链式调用风格不需要通过修改某种类型定义本身来实现，只需编写一个将该类型作为其第一个显式参数的新函数即可。

在大多数面向对象语言中，设计链式调用风格需要将方法添加到类定义本身中。如果类定义在库中，则直接添加并不总是可能的。

类型推断

(Type Inference)

Koka是强类型的。它使用强大的类型推断引擎来推断大多数类型。 你始终可以在任何局部变量声明时省略其类型标注：

fun main()
  var a:=10 // 类型推断为int，等效于var a:int:=10
  println(a)

你也可以省略函数参数和结果的类型标注：

import std/num/int32
fun rotl(a)
  rotl(a,10) // 对形参a能使用i32的rotl则将a类型推断为i32
  // int 是平台相关整数——在 32 位平台上等同于 int32，在 64 位平台上等同于 int64，宽度由编译目标决定
fun main()
  rotl(100.i32) // int不会被隐式转换成int32，必须显式转换

但一般来说，为函数参数和函数结果编写类型标注是一种很好的做法，因为它既有助于类型推断，又提供有用的文档以及来自编译器的更好的反馈。

示例代码：

//移位变换加密
fun encode(s : string, shift : int)
  fun encode-char(c)
    if c < 'a' || c > 'z' then return c
    val base = (c - 'a').int
    val rot  = (base + shift) % 26
    (rot.char + 'a')
  s.map(encode-char)
//恺撒密码加密代换
fun caesar( s : string ) : string
  s.encode( 3 )
fun main()
  caesar("foobarbaz")

对于此处的 encode 函数，不能省略 s 参数的类型：因为 map 函数是为列表和字符串类型定义的，没有类型标注不能确定 s 是列表还是字符串，从而编译时无法确定用哪一个签名的函数。
尝试在编辑器中示例的删除 s 的类型标注后运行以查看Koka编译器会报什么错误。

匿名函数和尾随Lambda

(Anonymous Functions and Trailing Lambdas)

Koka 还允许使用 fn 关键字的匿名函数表达式。例如，我们也可以不声明 encode-char 函数，而是将其作为函数表达式直接传递给 map 函数：

fun encode2( s : string, shift : int )
  s.map( fn(c)
    if c < 'a' || c > 'z' then return c
    val base = (c - 'a').int
    val rot  = (base + shift) % 26
    (rot.char + 'a')
  )

在上一个示例中，我们必须将最后一个右小括号放在最后一个大括号（fn关键字定义的匿名函数的函数体大括号，这里通过缩进省略了让编译器自己加）后面，这有点烦人。为了方便起见，Koka 允许匿名函数跟随函数调用——这也称为尾随 lambda。例如，下面是我们如何打印数字 1 到 10：

fun print10()
  for(1,10) fn(i)
    println(i)

脱糖为

for( 1, 10, fn(i){ println(i) } )

（事实上​​，由于我们将 i 参数直接传递给 println，我们也可以直接传递函数本身，如for(1,10,println)。）

例二、

fun printhi10()
  repeat(10)
    println("hi")

其中函数体脱糖为

repeat( 10, { println(hi) } )

进一步脱糖为

repeat( 10, fn(){ println(hi)} )

这对于 while 循环特别方便，因为这不是内置的控制流结构，而只是一个常规函数：

fun print11()
  var i := 10
  while { i >= 0 }
    println(i)
    i := i - 1

请注意 while 的第一个参数是如何用大括号而不是通常的小括号括起来的。在 Koka 中，小括号之间的表达式始终在函数调用之前求值，而大括号之间的表达式被挂起，并且可能永远不会被求值，也可能被多次求值（如我们的示例中）。

with语句

(With Statements)

据我所知，Koka 是第一个把尾随 Lambda 作为通用语法特性并与缩进布局深度整合的语言。它也是最早拥有点表示法的语言之一（这是独立开发的，但事实证明 D 语言具有类似的功能（称为 UFCS），它早于点表示法）。

另一个新颖的语法是 with 语句。由于可以轻松地将函数块（多行同层代码形成一个块，整个可被包起来采用为匿名函数）作为参数传递，它们通常会被嵌套使用。
先看一段代码：

fun twice(f)
  f()
  f()

fun test-twice()
  twice
    twice
      println("hi")

其中“hi“被打印四次（注意：这脱糖为

twice( fn(){ twice( fn(){ println("hi") }) })

）。使用 with 语句我们可以同缩进地写为：

pub fun test-with1()
  with twice
  with twice
  println("hi")

with 语句本质上将其后面的所有语句放入匿名函数中，并将该匿名函数作为最后一个参数传递。一般来说：

with f(e1,...,eN)
<body>
可被翻译为
f(e1,...,eN, fn(){ <body> })

此外，with 语句还可以绑定变量参数，如下所示：

with x <- f(e1,...,eN)
<body>
可被翻译为
f(e1,...,eN, fn(x){ <body> })

下面是一个使用 foreach 跨越函数体其余部分的示例：

pub fun test-with2() {
  with x <- list(1,10).foreach
  println(x)
}

其中函数体脱糖为

list(1,10).foreach( fn(x){ println(x) } )

这让人想起 Haskell do 表示法。以这种方式使用 with 语句一开始可能看起来有点奇怪，但在实践中非常方便 - 它有助于将 with 视为词法范围统摄当前块下方其余部分代码的闭包。

with finally

finally 函数将匿名函数采用为其第一个参数，离开作用域时回调这个函数，无论正常退出或通过“exception”（即当效应操作未恢复时）退出。with 与其配合很好：

fun test-finally()
  with finally{ println("exiting..") }
  println("entering..")
  throw("oops") + 42

脱糖为

finally(fn(){ println(...) }, fn(){ println("entering"); throw("oops") + 42 })

打印为

entering..
exiting..
uncaught exception: oops

这是 最小生成原则（min-gen principle） 的一个例子：许多语言对这种模式都有特殊的内置支持，比如 defer 语句，但在 Koka 中，这只是一种简朴的函数的语法糖的应用。

with‌ handler

with 语句与效应处理器（effect handler）结合使用特别有用。效应描述了一组抽象操作，其具体实现可以由处理器动态绑定。以下是用于发出消息的效应处理程序的示例：

操作（operation）就是你自定义的一种“效应原语“——它声明了“程序可能会做某件事“，但不规定这件事具体怎么做；具体怎么做由后面的 处理器（handler）​ 来提供。

// 生命一个抽象的操作: emit, 它如何发出消息由处理器动态定义。
effect fun emit(msg : string) : ()

// 发出一个标准的问候
fun hello() : emit ()
  emit("hello world!")

// 发出一个标准的问候到终端
pub fun hello-console1() : console ()
  with handler
    fun emit(msg) println(msg)
  hello()

在此示例中，with 表达式脱糖为

(handler{ fun emit(msg){ println(msg) } })( fn(){ hello() } )

通常，handler{ <ops> }表达式将一个函数块采用为其最后一个参数，因此可以直接与 with 一起使用。

此外，为了方便起见，对于仅定义一个操作的效应（比如 emit），我们可以省略 handler 关键字：

with val op = <expr>
with fun op(x){ <body> }
with ctl op(x){ <body> }
可被翻译为
with handler{ val op = <expr> }
with handler{ fun op(x){ <body> } }
with handler{ ctl op(x){ <body> } }

利用这种便利，我们可以将前面的示例更简洁地编写为：

pub fun hello-console2()
  with fun emit(msg) println(msg)
  hello()

直观地，我们可以将处理器with fun emit的作用视为给作用域内剩余内容动态绑定了一个对 emit 函数的定义

可选形参与具名形参

(Optional Parameters and Named Parameters)

作为一个面向函数的语言，Koka给有可选形参与具名形参的函数调用提供了强大的支持。
比如，replace-all函数要传入一个原string，一个模式（形参名：pattern）和一个替换者string（形参名：repl）。

fun world()
  replace-all("hi there", "there", "world")  // 返回 "hi world"

利用具名形参，我们也可以这样写这个函数调用：

fun world2()
  "hi there".replace-all( repl="world", pattern="there" )

可选参数这一语法允许您为形参指定默认值，从而不必在调用方填实参。
我们定义一个函数 sublist，它接收一个列表、起始位置和所需子列表的长度 len。我们可以将 len 参数设置为可选，并默认使用输入列表的长度来返回起始位置之后的所有元素：

fun sublist( xs : list<a>, start : int, len : int = xs.length ) : list<a>
  if start <= 0 return xs.take(len)
  match xs
    Nil        -> Nil
    Cons(_,xx) -> xx.sublist(start - 1, len)

其中 len 参数实际已获得由问号表示的可选 int 类型，len: ? int。

更大的例子：破解凯撒编码

(A larger example: cracking Caesar encoding)

这是一个稍大的程序，灵感来自 Graham Hutton 最优秀的“Programming in Haskell”书中的一个示例：

import std/num/float64
// 英语字母频率表
val english = [8.2,1.5,2.8,4.3,12.7,2.2,
               2.0,6.1,7.0,0.2,0.8,4.0,2.4,
               6.7,7.5,1.9,0.1, 6.0,6.3,9.1,
               2.8,1.0,2.4,0.2,2.0,0.1]

// 小辅助函数
fun percent( n : int, m : int )
  100.0 * (n.float64 / m.float64)

fun rotate( xs : list<a>, n : int ) : list<a>
  xs.drop(n) ++ xs.take(n)

// 计算字符串的字母频率表
fun freqs( s : string ) : list<float64>
  val lowers = list('a','z')
  val occurs = lowers.map( fn(c) s.count(c.string) )
  val total  = occurs.sum
  occurs.map( fn(i) percent(i,total) )

// 根据卡方分布统计计算两个频率表的匹配程度
fun chisqr( xs : list<float64>, ys : list<float64> ) : float64
  zipwith(xs,ys, fn(x,y) ((x - y)^2.0)/y ).foldr(0.0,(+))

// 破解凯撒编码的字符串
fun uncaesar( s : string ) : string
  val table  = freqs(s)                   // 为s建一个频率表
  val chitab = list(0,25).map fn(n)       // 为0到25每种移位构建卡方数字列表
                 chisqr( table.rotate(n), english )

  val min    = chitab.minimum()           // 找到最小元素
  // 找到最小卡方值的位置 n，取负得到解码所需的反向移位
  val shift  = chitab.index-of( fn(f) f == min ).negate
  s.encode( shift )

fun test-uncaesar()
  println( uncaesar( "nrnd lv d ixq odqjxdjh" ) )

val 关键字声明一个静态值。在示例中，值 english 是浮点数（float64 类型）列表，表示每个字母的平均频率。函数 freqs 为特定字符串构建频率表，而函数 chisqr 计算两个频率表的匹配程度。在函数crack中，这些函数用于查找一个移位值，该值产生一个频率表与英语频率表最接近的字符串——我们用它来解码该字符串。

效应类型

(Effect Types)

Koka 的一个新颖之处在于：它会自动推断出函数中发生的所有副作用。没有任何副作用的情形记为 total（或 <>），对应纯数学函数。若函数可能抛出异常，其效应为 exn；若函数可能不停机，其效应为 div（divergence，发散）。exn 与 div 的组合称为 pure，直接对应 Haskell 的“纯度“概念。

Koka 里 pure = <exn, div> 这个定义，本质是把 Haskell 的“纯度“概念显式化为一个类型标签：它表示函数可能抛异常或不停机（这两者在 Haskell 语义里被 ⊥ 吸收，不影响引用透明），但没有状态变更、非确定性、IO 等更显式的副作用。Koka 借此既保持了和 Haskell 理论体系的对应，又把“纯度“这件事从 Haskell 的隐式约定变成了 Koka 类型系统里的显式、可检查、可推断的一等公民。

在编程语言理论中，一个构造若是“一等的（first-class）“，它就能像普通值一样被全面操纵。Wellesley CS251（Principles of Programming Languages）课程讲义中指出，一等值“can be used or created wherever we use or create any other values”——具体包括：可作为函数调用的实参、可作为函数体的结果、可存入数据结构、可被变量绑定命名等 。

非确定性函数具有 ndet 效应。所谓“最坏“的效应是 io，意味着程序可以抛出异常、不停机、具有非确定性、读写堆内存，并执行任意输入/输出操作。以下是一些带效应的函数示例：

fun square1( x : int ) : total int   { x*x }
fun square2( x : int ) : console int { println( "a not so secret side-effect" ); x*x }
fun square3( x : int ) : div int     { x * square3( x ) }
fun square4( x : int ) : exn int     { throw( "oops" ); x*x }

当效应为 total 时，我们通常将其省略不写在类型标注中。例如，当我们写下：

fun square5( x : int ) : int
  x*x

此时假定效应为 total。有时候我们写了一个带效应的函数，但不想显式写出它的效应类型。这种情况下，可以使用通配类型来表示某个被推断出来的类型。通配类型的写法是：用一个下划线作为前缀的标识符，或者干脆只写一个下划线：

fun square6( x : int ) : _e int
  println("I did not want to write down the \"console\" effect")
  x*x

编辑器中将鼠标悬停在 square6 上，即可看到 _e 被推断出的效应，即 console。

效应的语义

(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）。
当一个函数有 st 效应时（即它会读写堆上的可变状态），语义上它相当于隐式地接收一个堆、并返回一个更新后的堆。所以 int -> <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 查询、并行任务、分层、沙盒移动代码等。

效应组合

(Combining Effects)

一个函数时常包含多个效益，例如：

fun combine-effects()
  val i = srandom-int() // 非确定性 → ndet
  throw("oops")         // 抛出异常 → exn
  combine-effects()     // 非终止 → div(发散)

分配给效应组合的效应是 ndet、div 和 exn，可以组合写成一行效应 <div,exn,ndet>。给combine-effects推断出的返回的类型实际上是 <pure,ndet>，其中 pure 是类型别名：

alias pure = <div,exn>

效应多态

(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占位表示某些效应）。

局部可变变量

(Local Mutable Variables)

斐波那契数列中，每个后续斐波那契数都是前两个斐波那契数之和，其中 fib(0) == 0 且 fib(1) == 1。我们可以使用递归函数轻松计算斐波那契数：

fun fib(n : int) : div int
  if n <= 0   then 0
  elif n == 1 then 1
  else fib(n - 1) + fib(n - 2)

请注意，类型推断引擎目前还不够强大，无法证明此递归函数总是终止，这导致结果类型中包含发散效应 div。

以下是斐波那契函数的另一个版本，但这次使用局部可变变量实现。我们使用 repeat 函数来迭代n次：

fun fib2(n)
  var x := 0
  var y := 1
  repeat(n)
    val y0 = y
    y := x+y
    x := y0
  x

handler 内部隐式绑定了一个 resume 函数，调用 resume(v) 会让计算在被效应操作打断的地方继续下去，并把 v 作为该操作的返回值。

与绑定不可变值的 val 声明（如 val y0 = y）相反，var 声明声明可变变量，其中 := 运算符可以为该变量分配新值。在内部，var 声明使用一个状态效应处理器，确保即使多次 恢复（resume），状态也具有正确的语义。

然而，这也意味着可变局部变量并不是一等的，我们不能将它们作为参数传递给其他函数（因为它们总是被解引用）。可变局部变量的生命周期不能超出其词法作用域。例如，如果局部变量通过函数表达式逃逸，则会出现类型错误：

fun wrong() : (() -> console ())
  var x := 1
  (fn(){ x := x + 1; println(x) })
fun main()
  wrong()
/*
type error: abstract type(s) escape(s) into the context
  term         :   var x := 1
                   (fn(){ x := x + 1; println(x) })
  inferred type: () -> <local<$h>|_e> (() -> <console/console,local<$h>|_e1> ())
  hint         : give a higher-rank type annotation to a function parameter?
*/

这一限制使得语义更加清晰，同时也为（目前尚未完全实现但理论上可行的）优化留下了空间——而这些优化对于通用的 可变引用单元格(mutable reference cell) 来说是无法实现的。

通常更推荐使用 var 声明，因为它们在多次恢复（multiple resumptions）的场景下表现更好，而且在语法上更简洁，无需解引用运算符。（不过，我们仍然需要引用单元格，因为它们是一等的，而 var变量 无法传递给其他函数。）

引用单元格、状态隔离

(Reference Cells and Isolated State)

Koka 同样具备一等公民、堆分配的可变引用单元格。可以通过 val r = ref(0) 来分配一个整数的引用（因为引用本身就是一个值！），并使用 bang 运算符 !r 进行解引用。我们可以使用**引用单元格（reference cells）**编写斐波那契函数：

fun fib3(n)
  val x = ref(0)
  val y = ref(1)
  repeat(n)
    val y0 = !y
    y := !x + !y
    x := y0
  !x

正如我们所看到的，使用 var 声明通常是更受青睐的，因为它们在多次恢复（multiple resumptions）情况下表现更好，而且在语法上也更为简洁，因为它们不需要解引用运算符。（尽管如此，我们仍然需要引用单元格（reference cells），因为它们是一等的，而 var 变量不能传递给其他函数。）

在编辑器内查看为这些引用推断出的类型时，我们看到x和y的类型为 ref<h,int>，这表示在某个堆 h 中对一个 int 类型可变值的引用。在堆上产生的效应包括：分配堆 h 为 alloc<h>，从堆 h 中读取为 read<h>，以及向堆 h 中写入为 write<h>。这些效应组合起来被称为 有状态的（stateful），并使用别名 st<h> 来表示。

显然，fib3 函数体的效应是 st<h>；但当我们在编辑器内悬停在 fib3 上时，会发现推断出的类型实际上是 total 效应：(n:int) -> int。这意味着，尽管 fib3 内部是有状态的，但其副作用却永远不会被观察到。

实际上可以证明，只要堆类型 h 无法在此函数外部被引用，即它不是参数或返回类型的一部分，外界既无法修改也无法观察到堆 h，我们就可以安全地丢弃 st<h> 效应，隔离掉状态。

更正式地说，Koka 编译器通过证明 函数对堆类型 h 是 完全多态的
（或称 全称量化的：
\(fib:∀h. int→st⟨h⟩ int\)
也就是不依赖具体的某个堆，对任意堆 h 都成立）来证明这一点，并应用 run 函数（对应于 Haskell 中的 runST）来丢弃 st<h> 效应。（详见Koka的论文）

数据类型

(Data Types)

结构体

(Structs)

面向函数语言的一个重要方面是能够定义丰富的数据类型，函数在这些类型之上工作。一种常见的数据类型是 结构体(struct) 或 记录(record)。下面是一个包含个人信息的结构体示例：

struct person
  age : int
  name : string
  realname : string = name

val brian = Person( 29, "Brian" )

使用构造子为结构体（以及其他数据类型）创建实例，例如 Person(19,"Brian")。此外，这些构造子可以使用命名参数，因此我们也可以这样调用构造子：Person( name = "Brian", age = 19, realname = "Brian H. Griffin" )，这非常接近常规的记录语法，但没有任何特殊规则——它只是层层嵌套的函数而已！

此外，Koka会自动为结构体（或其他数据类型）中的每个字段生成访问器函数，我们可以用 brian.age 来访问一个人的年龄（这当然只是 age(brian) 的语法糖）。

拷贝

(Copying)

默认情况下，所有结构体（以及其他数据类型）都是不可变的。我们通常不会直接修改结构体中的字段，而是返回一个新的结构体，其中字段已更新。例如，下面是一个生日函数，它会增加年龄字段的值：

fun birthday( p : person ) : person
  p( age = p.age + 1 )

此处，birthday 返回一个新的 person类型的数据，该 person类型的数据 与 p 相等，但年龄已增加。语法p(...)是调用person复制构造函数的语法糖。该构造函数也会为每种数据类型自动生成，其内部生成形式如下：

fun copy( p, age = p.age, name = p.name, realname = p.realname )
  Person(age, name, realname)

当实参跟随数据值出现时，如 p( age = p.age + 1)（此处p就是数据值，p.age+1是实参），它会被展开为调用这个复制函数，即 p.copy( age = p.age + 1)。遵循最小生成原则，记录更新没有特殊的规则，而是使用带有可选形参和具名形参的普通函数调用。

替选类型（或称联合类型）

(Alternatives (or Unions))

可用Koka的替选类型表示代数数据类型（algebraic data types，ADT）中的和类型（sum types）。例如，下面是一个枚举：

type color
  Red
  Green
  Blue

它有三个替选：Red、Green、Blue

这些枚举类型的特殊情况包括：void 类型，它没有任何替选（因此不存在具有该类型的值）；单位元类型 unit ，它只有一个构造子 Unit（因此，只存在一个具有 unit 类型的值，即 Unit）；以及布尔类型 bool，它有两个构造子 True 和 False。作为简写，我们也可以将 unit 类型写作 ()，并将 Unit 构造子写作 ()。

type void

type ()
  ()

type bool
  False
  True

构造子可以带有形参。例如，以下是如何创建一个既可以是整数也可以是无穷值的 number 类型：

type number
  Infinity
  Integer( i : int )

我们可以通过写出 Integer(1) 或 Infinity 来创建这样的number。此外，数据类型可以是多态的和递归的。以下是 列表（list） 类型的定义，它要么为空（Nil），要么是 Cons ：一个头元素（head）后跟一个尾列表（tail）：

type list<a>
  Nil
  Cons{ head : a; tail : list<a> }

Koka会自动为每个命名形参生成访问器函数。例如，对于列表，我们可以通过 Cons(1, Nil).head 来访问列表的头部。

我们现在还可以看到，结构体类型不过是带有同名单一构造子的一个寻常类型的语法糖。

struct tp { <fields> }
可被翻译为
type tp {
  Tp { <fields> }
}

例如原先 person结构体 是这样定义的：

struct person{ age : int; name : string; realname : string = name }

可脱糖为

type person
  Person{ age : int; name : string; realname : string = name }

或者省略大括号：

type person
  Person
    age : int
    name : string
    realname : string = name

模式匹配

(Matching)

Koka 使用模式匹配（match 表达式）来解构代数数据类型。保留字 match 表示模式匹配——它根据一个值的实际构造分支，将控制权分发到对应的处理分支 。

基本语法

match 表达式的形式如下：

match <表达式>
  <模式1> -> <分支1>
  <模式2> -> <分支2>
  ...

match 会依次尝试每个模式，第一个匹配成功的模式对应的分支被执行。每个模式可以是：

  • 构造子模式：匹配某个具体的构造分支（如 Nil、Cons(x, xx)）
  • 变量模式：绑定到一个变量，匹配任意值
  • 通配模式 _：匹配任意值且不绑定
  • 字面量模式：匹配具体的常量值

解构列表

Koka 的 list 类型有两个构造子：Nil（空列表）和 Cons(head, tail)（非空列表，头部是 head，尾部是 tail）。我们可以用 match 来遍历它：

// 遍历列表并打印元素
effect yield<a>
  fun yield(x : a) : ()

pub fun traverse(xs : list<a>) : yield<a> ()
  match xs
    Cons(x, xx) -> { yield(x); traverse(xx) }
    Nil         -> ()
pub fun main()
  with handler
    fun yield(x : int)
      println(x)
  val b = [1,2,3,4]
  traverse(b)

这里 match xs 检查 xs 是 Cons 还是 Nil：

  • 如果是 Cons(x, xx)，则将头部绑定到 x、尾部绑定到 xx，然后先 yield(x) 处理头部，再递归处理尾部 xx
  • 如果是 Nil，则什么都不做，返回 ()

一个标准库的例子：map

标准库的 map 函数用 match 实现列表转换 ：

pub fip fun map(xs : list<a>, ^f : a -> e b) : e list<b>
  match xs
    Cons(x,xx) -> Cons(f(x), xx.map(f))
    Nil        -> Nil

注意 map 的形参的类型签名：^f : a -> e b：^ 表示 f 只是被借用，不需要转移所有权，也无需修改引用计数。f 可以带有任意效应 e，而 map 本身也返回 e list<b>——效应被透明地传递。这是 Koka 效应多态的体现。

Koka 编译器保证 map 的这种递归实现会被优化成常数栈空间——相关的优化（tail recursion modulo cons）虽然早在 1970 年代就已为人所知，但令人惊讶的是很少有语言真正实现它 。

替选类型与模式匹配

对于任意用 type 定义的替选类型，match 同样适用。例如 number 类型 ：

type number
  Infinity
  Integer(i: int)

fun to-int(n : number) : int
  match n
    Infinity   -> 0
    Integer(i) -> i

这里 Integer(i) 模式不仅匹配 Integer 构造子，还把内部的 i 绑定到变量 i，供分支体使用。

模式里的变量绑定与嵌套

模式可以嵌套，且能同时绑定多个变量。例如解构一个二叉树 ：

type tree
  Leaf(value : int)
  Node(left : tree, value : int, right : tree)

fun tree-size(t : tree) : int
  match t
    Leaf(v)       -> v
    Node(l, v, r) -> v + tree-size(l) + tree-size(r)

Node(l, v, r) 一次性把三个字段分别绑定到 l、v、r。

通配与兜底

如果只关心部分模式，可以用 _ 忽略不关心的部分 ：

fun is-empty(xs : list<a>) : bool
  match xs
    Nil -> True
    _   -> False

_ 匹配任意值且不绑定变量名。

模式匹配的穷尽性

Koka 编译器会检查 match 表达式是否穷尽了所有可能的构造分支。如果有遗漏，编译器会报错——这保证了你不会忘记处理某个构造子，是代数数据类型模式匹配的一大安全优势。 例如，如果上面的 to-int 漏掉了 Infinity 分支，编译器会拒绝该程序，提示模式匹配不穷尽。

为什么模式匹配重要

模式匹配让“解构数据“这件事变得：

  • 安全：编译器检查穷尽性，杜绝漏处理
  • 简洁：一个 match 同时完成“判断构造子 + 绑定内部字段“两件事
  • 可读：数据的形状直接体现在代码结构里
  • 可组合：与递归、效应多态天然配合

Tip

在 Koka 中，match 是处理代数数据类型的主要方式。结合前面讲的alternatives，你可以定义丰富的数据模型，然后用 match 优雅地消费它们。

可扩展数据类型

(Extensible Data Types)

普通的 type 声明定义的代数数据类型，其构造分支在声明时就固定了——后续无法在不修改原定义的情况下添加新的构造子。Koka 还提供了一种可扩展的数据类型：open type。它允许你先声明一个“开放的“类型，然后在程序的任何其他地方（在同一个模块或任何其他模块中）通过 extend type 为它追加新的构造分支。

open type openvar
  A
  B

extend type openvar
  C

fun do-it-try-it(v : openvar) : console ()
  match v
    A -> println("got an A")
    B -> println("got a B")
    C -> println("got a C")
    // 注意：我们可以在代码里匹配 D，尽管它还没被声明
    D -> println("got a D")
    // 兜底
    _ -> println("got something else")

extend type openvar
  D

fun main() : console ()
  do-it-try-it(C)   // 输出: got a C
  do-it-try-it(D)   // 输出: got a D

Tip

由于 openvar 是开放的，理论上任何下游代码都可能继续 extend type openvar 添加新分支。因此，在对 open type 做模式匹配时，编译器无法在编译期保证穷尽性——你可能没有处理未来新增的构造子。所以在实际使用中，通常以通配模式 _​ 收尾，或者只匹配你已知的那些分支。

open type 适用于以下场景：

  • 跨模块的类型演进：基础库定义一个开放类型，各业务模块往里添加自己的构造分支，而不需要修改基础库源码
  • 插件架构：宿主程序定义 open type PluginEvent，各插件通过 extend type PluginEvent 声明自己的事件类型
  • AST / 中间表示的扩展：语言前端定义 open type Expr，各优化 pass 或后端可以扩展新的节点类型

极性与变性

(Polarity and Variance)

下一节归纳类型、余归纳类型与递归类型将用到“正位置（positive position）“和“负位置（negative position）”，并出现“负 × 负 = 正“这样的判断。这套极性（polarity）规则背后的概念，就是类型论中的变性（variance）——更具体地说，其中，我们只讨论协变（covariance）与逆变（contravariance）。本节先用嵌套函数参数把它们讲清楚。

变性：什么时候替换是安全的

Koka 的值类型是名义的（后面会澄清），写不出子类型替换的例子，所以本节的示例改用 TypeScript 联合类型来演示——联合类型的成员天然就是子类型：

type Dog = { kind: "dog" }
type Cat = { kind: "cat" }
type Animal = Dog | Cat   // 联合类型：Dog、Cat 都是 Animal 的子类型

返回位置：协变（正位置）

先看“产生动物“的场景——我们需要一个返回 Animal 的函数：

function adoptOne(f: () => Animal): string {
  return "领养了 " + f().kind
}

adoptOne 只会把 f 的返回值当作 Animal 使用，所以返回类型可以比 Animal 更“窄“：

  • 提供 () => Dog（返回更“窄“）：Dog 本身就是 Animal，一切消费 Animal 的代码都成立——安全
  • 提供返回类型比 Animal 更“宽“的函数：返回值未必是 Animal，kind 属性可能不存在——不安全

输出位置要求“宁窄勿宽“：更窄的值类型仍然能安全替换更宽的，子类型关系的方向保持不变（同向），这种替换称为协变（covariant），对应正位置。

参数位置：逆变（负位置）

再看“消费动物“的场景——我们需要一个“描述任意动物“的函数作为参数：

const dog: Dog = { kind: "dog" }
const cat: Cat = { kind: "cat" }

function describeAll(f: (a: Animal) => string): string {
  return f(dog) + ", " + f(cat)
}

describeAll 在内部会把 Dog 和 Cat 都传给 f，所以 f 的参数类型必须至少能接受 Animal：

  • 提供 (a: Dog) => string（参数更“窄“）：f(cat) 时崩溃——不安全
  • 提供参数类型更“宽“的函数：任何调用都成立——安全

输入位置要求“宁宽勿窄“：更窄的参数类型反而不能替换更宽的，能站上来的必须是更宽的类型——子类型关系的方向发生反转（反向），这种替换称为逆变（contravariant），对应负位置。

一句话记忆：返回协变、参数逆变。输出位置可以收窄（协变），输入位置必须放宽（逆变）。

嵌套函数参数：极性翻转

(Flipping under nesting)

单个函数类型 a -> b 的规则很简单：参数 a 负位、返回 b 正位。但类型可以层层嵌套，比如 (a -> b) -> c。逐层拆解：

  1. 外层是一个函数：它的参数是 (a -> b) 这个整体——所以 (a -> b) 位于负位置；它的返回 c 位于正位置。
  2. 内层 (a -> b) 又是一个函数：参数 a 位于内层的负位置，返回 b 位于内层的正位置。

现在数一数 a 的总极性：它先被外层当作参数（乘一个“负“），又在内层被当作参数（再乘一个“负“）：

负 × 负 = 正

为什么这里是“乘法“而不是别的运算？
因为极性可以编码成：正位置 = +1，负位置 = −1；穿过一层“函数参数“就乘一个 −1（翻转），穿过“返回/字段“就乘 +1（不变）。于是嵌套后，一个类型变量最终的极性 = 沿途所有层的符号相乘——负 × 负 = 正 就是 (−1) × (−1) = +1，本质是两次翻转等于不翻转。乘法恰好刻画“翻转奇偶次“的奇偶性，且对任意深度可结合；数学上，极性就是从类型树到乘法群 {+1, −1} 的一个同态。

所以 a 最终处于正位置——尽管它字面上写在“参数里“，但整体上对 a 而言是协变的。这正是下一节中 Foo(f: (foo -> int) -> int) 能通过检查的原因。

一般规则：每穿过一层函数参数，极性翻转一次。用表格概括：

位置极性变性
记录字段 / 函数返回正协变（covariant）
函数参数负逆变（contravariant）
参数的参数正负 × 负 = 正
参数的返回负负 × 正 = 负
返回的参数负正 × 负 = 负
返回的返回正正 × 正 = 正

练手：下面这个类型里，a、b、c、d 各处于什么极性？

type ex3
  con F(g : (a -> b) -> c -> d)

g 的类型 (a -> b) -> (c -> d) 解析：外层参数 (a -> b) 负位，外层返回 (c -> d) 正位。于是：

  • a：负（外层参数）× 负（内层参数）= 正
  • b：负（外层参数）× 正（内层返回）= 负
  • c：正（外层返回）× 负（内层参数）= 负
  • d：正（外层返回）× 正（内层返回）= 正

澄清：Koka 用的是 替选类型，不是继承

(Koka uses alternatives, not inheritance)

上面的例子用 TypeScript 联合类型展示子类型替换：type Animal = Dog | Cat 里，联合成员 Dog、Cat 是独立的类型，并且是 Animal 的子类型（Dog <: Animal），所以函数类型在参数/返回位置上的协变、逆变可以实际赋值验证（strictFunctionTypes 下，独立声明的函数类型参数逆变、返回协变）。

strictFunctionTypes 是 TypeScript 2.6 引入的编译选项，用于对‌函数类型参数‌启用‌逆变（contravariant）‌检查而非默认的双变（bivariant）检查，防止不安全的函数赋值，属于 strict 严格模式子集 。‌‌

Koka 没有继承，也没有这种子类型关系：type animal 配合 con Dog、con Cat 声明的是一个替选类型，Dog、Cat 只是它的两个构造子，本身并不是独立的类型，彼此之间不存在 <: 子类型关系；int 与 float 之间、函数类型之间同样没有子类型关系。因此上面 TypeScript 的“用更宽参数的函数替换“在 Koka 中写不出来——编译器会直接报类型不匹配。

那么极性在 Koka 里有什么用？答案是：变性的价值在子类型语言里是“替换“，而在 Koka 里是“良构性与终止性分析“。编译器遍历类型声明，计算每个类型变量的极性，据此：

  • 判定 type 声明的递归是否合法（只允许正位置）→ 归纳类型的良构性（下一章会详细展开）
  • 结合递归结构分析，推断函数是 total 还是 div → 终止性检查
  • 为 co type（协归纳）与 div type（任意递归）的放宽提供理论基础

变性（variance） 描述的是：复合类型的子类型与其组成部分的子类型之间的关系。 极性（polarity） 描述的是：类型变量在语法树中出现的位置——正位置（输出）协变，负位置（输入）逆变。

  • 嵌套函数参数让极性不断翻转（负 × 负 = 正），这是理解“类型藏在参数里为什么有时反而合法“的关键。

在 Koka 这样没有子类型的语言里，我们关心的不是“能否替换“，而是“递归是否良构、函数是否终止“——极性正是这两项检查的底层语言。

归纳类型、余归纳类型与发散类型

(Inductive, Co-inductive, and Recursive Types)

Koka 的 type 关键字用于声明归纳类型（inductive types）——例如 list。为了实现等式推理（equational reasoning）和终止性检查（termination checking），Koka 对普通 type 声明做了严格限制：类型本身不能出现在负位置（negative position）。这一限制保证了归纳类型的良构性，使得编译器可以对操作这类数据的递归函数做终止性分析。

除了 type，Koka 还提供另外两种类型声明：co type（余归纳类型，co-inductive types）和 div type（任意递归类型，arbitrary recursive types）。它们分别放宽了 type 的不同限制，以适应不同的编程需求。

归纳类型（type）：有限、正向递归、终止性

普通的 type 声明要求递归是正向的（positive）——即类型自身只能出现在构造子的“输出“位置，而不能出现在“输入“（负）位置。经典的例子是标准库的列表：

pub type list<a>
  con Nil
  con Cons(head:a, tail : list<a> )

在 Koka 里，con 是用于显式声明“构造子（constructor）“的关键字。PLDB 的 Koka 关键字表明确把 con 列为语言关键字之一 。现代 Koka 在 type 定义体内默认把每个顶级声明当作构造子，所以 con 可以省略。 这里 list<a> 出现在 Cons 的 tail 字段里——这是正位置，合法。这种限制保证了：

  • 可终止性：对任何在 list 上做结构递归的函数，编译器可以做终止性检查
  • 等式推理：归纳类型满足归纳法原理，支持等式推理 以下这种 type 声明中 bad 出现在 bad -> int 的参数位置——负位置，编辑器诊断会报错、编译会报错
type bad
  Bad(f: bad -> int)

Koka 的终止性检查器会分析递归函数：如果每次递归调用都减小了归纳类型参数的大小，则该函数被判定为 total，否则 div。 标准库的 length 实现：

pub fun length(xs)
  fun len(ys,acc)
    match ys
      Cons(_,yy) -> yy.len(acc+1)
      Nil        -> acc
  xs.len(0)

length 在每个递归调用中都处理更短的列表，因此被判定为 total：fun length : forall<a> (xs : list<a>) -> int

余归纳类型（co type）：潜在无穷、生产性

有些数据结构本质上是潜在的无穷——例如惰性流（stream）、无限序列、响应式事件流等。这些结构不能用普通的 type 声明，因为 type 要求有限归纳。针对潜在的无穷，Koka 提供 co type​ 来声明余归纳类型，比如标准库的 stream：

pub co type stream<a>
  con Next(head:a, tail: stream<a> )

stream 在数学上就是余归纳类型——它的元素是“通过观察逐步揭示“的，可能无穷（如 repeat(1) 产生的流）。标准库选择 co type 是为了在语义层面精确标记这种“潜在无穷“的性质，语法上不存在“必须用 co type 才能声明“。实际上 type 也可以用于其声明，但是缺少了“潜在无穷“标记，所以在你自定义一个 stream 时，即使去掉co只用type也能通过编译检查。

但实际上是会有产生无穷 stream 的情况的：

// 1. 延迟计算单元：thunk
type thunk<a>
  Delay(f: () -> div a)      // 未求值
  Memo(v: a)             // 已求值（用于记忆化，可选）

// 强迫求值
fun force(t: thunk<a>): div a
  match t
    Delay(f) -> f()      // 这里简单地直接调用；生产代码可做 memoization
    Memo(v)   -> v

// 2. 流类型：tail 是 thunk<stream<a>>
//    用 co type 标记"潜在无穷"的余归纳语义
co type stream<a> //实际上去掉 co 也能通过编译而且不会有任何影响
  con SCons(head: a, tail: thunk<stream<a>>)

// 3. 重复单一元素 → 潜在无穷流
//    关键：tail 用 Delay(fn() my-repeat(x)) 包裹，构造时不立即求值
pub fun my-repeat(x: a): <div|_e> stream<a>
  SCons(x, Delay(fn() my-repeat(x)))

// 4. 取前 n 个元素，转成 list
pub fun take(s: stream<a>, n: int): <div|_e> list<a>
  match n
    0 -> Nil
    _ -> match s
          SCons(h, t) -> Cons(h, take(force(t), n - 1))

// 5. 从初始值迭代：f(x), f(f(x)), f(f(f(x))), ...
pub fun iterate(f: a -> a, x: a): <div|_e> stream<a>
  SCons(x, Delay(fn() iterate(f, f(x))))

// 6. main：只操作有限前缀，程序正常终止
pub fun main()
  println(take(my-repeat(1), 100)) // 将100改成任何数字n都可以打印出n个1

极性翻转（polarity flipping）

type 和 co type 都要求自身类型不能在负位置

type foo
  Foo(f: (foo -> int) -> int)
co type bar
  Bar(f: (bar -> int) -> int)

foo、bar位于内层箭头的左侧（负位），而该箭头整体又位于外层箭头的左侧（负位） 负 × 负 = 正 检查通过。

发散类型（div type）：放开、放弃自动终止性

如果需要任意的递归类型——包括类型出现在负位置（如函数参数位置），Koka 提供 div type：

div type foo
  Foo(recur: foo -> int)

div type 允许类型以任意方式递归，包括出现在负位置。这使得可以利用 Koka 允许的命名函数 + 递归数据类型，构造出了一个自引用的不动点，表达能力等效于 Y 组合子：

div type foo
  Foo(recur: foo -> int)

fun upsilon(x: foo): int
  match x
    Foo(recur) -> recur(x)

fun do_upsilon(): int
  upsilon(Foo(upsilon))

这段代码执行会导致无限递归，导致栈溢出， exit code -11 即 SIGSEGV（段错误）。 任何对 div type 做模式匹配的函数，都被假定为可能发散（potentially divergent），因此自动带上 div 效应。这是一个保守但安全的设计——因为 div type 赋予了编码 Y 组合子的能力，可以写出非语法递归的不终止函数，所以 Koka 必须假定这类函数可能发散。

值类型

(Value Types)

值类型是（非递归的）数据类型，它们不在堆上分配，而是作为值在栈上传递。由于所有数据类型都是不可变的，从语义上讲这些类型就是等价的，但值类型可能更高效，因为它们避免了堆分配和引用计数（或者也可能更昂贵，因为它们需要复制而不是共享引用）。

默认情况下，任何大小最多为 3 个机器字（= 64 位平台上的 24 字节）的非递归归纳数据类型都被视为值类型。例如，二元组和三元组按值传递和返回。通常，这意味着在进行优化编译时，此类元组将返回到寄存器中。

3 个机器字是一个平衡点：在这个尺寸以下，复制成本通常低于引用计数开销，且有机会放进寄存器；超过这个尺寸，引用计数方案开始占优。

我们还可以通过在 type 或 struct 声明前使用 value 关键字，来强制将某个类型编译为值类型。

高级

装箱

为了支持泛型多态，值类型有时需要装箱（boxing）。list<a> 只有一份定义、编译成一种表示：无论 a 被实例化成什么，列表节点的元素槽都必须保持固定大小。普通元素（如 int）可以直接填入槽中，但元组这类值类型的内联表示随类型不同、维数不同而大小不一，放不进固定槽——于是元素只能装箱（boxed）、在堆上分配，列表节点的元素槽里存放的是指向元组的统一大小的指针。构造元组列表 [(1,True)] 时，编译器内部就把元素 (1,True) 转换为 [Box((1,True))]。

对常规数据类型和 int 而言，装箱是“免费“的：装箱表示与未装箱表示在数学上同构（一一对应、可逆无损），且编译器能在优化阶段消除不必要的装箱。此外，不超过 63 位（64 位平台上）的值类型采用就地装箱（in-place boxing），无需堆分配（如 int32）。float64 也有专门的底层表示优化：默认情况下，只有绝对值超出 2⁻⁵¹¹ 到 2⁵¹² 范围（无穷大与 NaN 除外）的 float64 才会堆分配。

对于性能敏感的代码，我们可以针对特定元素类型“特化“多态数据类型，以减少装箱带来的分配。例如：

type mylist
  MyCons{ head1: int; head2: bool; mytail: mylist }
  MyNil

这里把 list<(int,bool)> 特化成一个专门的递归类型：head1、head2 直接作为 MyCons 的内联字段存储，不再需要把元组装箱。于是前面 [(1,True)] 的例子对应写成 MyCons(1,True,MyNil)：原来每个元素需要两次分配（Cons 节点一次、堆上装箱的元组一次），现在只需为 MyCons 分配一次，还省掉了指向元组的间接引用。未来 Koka 开发组希望扩展编译器，自动执行这种特化，或通过特殊指令实现。

效应处理器

(Effect Handlers)

效应处理器是一种处理 控制流抽象 和 动态绑定 的新方式，将它们定义为用户自定义的 处理器(handler) ——不再需要为异常、迭代器、async-await、概率编程等特意添加语法。此外，这些处理器可以自由组合，因此诸如 async-await 与异常之间的交互也能得到良好定义。

处理

(Handling)

让我们从定义自己的 异常效应 开始。effect 定义一个新效应类型，声明相关操作。下面我们先使用最通用的 控制（ctl） （之后会详解它）操作写个例子：

effect raise
  ctl raise( msg : string ) : a

这定义了一个效应类型 raise ，声明了一个类型为 (msg : string) -> raise a 的操作 raise 。完整定义决定了效应类型的签名，有了其签名之后，我们就可以使用这个操作了：

fun safe-divide( x : int, y : int ) : raise int
  if y==0 then raise("div-by-zero") else x / y

在这里我们可以看到，安全除法函数带有 raise 效应（因为我们在函数体中使用了 raise 操作）。这样的效应类型意味着，我们只能在 raise 被处理的上下文中对该函数进行求值（换句话说，即在 raise 被“动态绑定”的上下文中，或者在我们“拥有raise能力（capability）”的上下文中）。

我们可以通过为 raise 操作给出一个具体的定义来处理这种效应。例如，我们可能会始终返回一个默认值：

fun raise-const() : int
  with handler
    ctl raise(msg) 42
  8 + safe-divide(1,0)

调用 raise-const() 的结果是42（而非50）。当在 safe-divide 中调用 raise 时，控制权会让渡（yield）给动态调用栈中距离调用点最近的 raise 处理器——即“最内层“处理器：若同一效应有多个嵌套处理器，总是最靠近调用点的那个接管，类似别的语言异常处理中优先匹配最近的 catch 块；本例只有一个处理器，所以由它接管。控制权移交后，处理器展开调用栈，再按操作的定义求值，在此例中直接返回 42。现在我们明白了为何称其为控制操作：raise 改变了常规的线性控制流，从原始调用点直接跳到最内层处理器。处理器已消除了 raise 效应，raise-const 重新变为无效应的 total 函数。

handler{ <ops> } 表达式本身是一个函数，它期望接收一个函数参数，并在此 handler 所在作用域内应用它，例如对于 (handler{ <ops> })(action) ，会在 (action) 内应用它。这自然与 with 语句配合得很好。对于单个操作，我们可以省略 handler 关键字，其翻译如下：

with ctl op(<args>){ <body> }
可被翻译为
with handler
  ctl op(<args>){ <body> }

借助这一翻译，我们可以将之前的示例更简洁地写成：

fun raise-const1() : int
  with ctl raise(msg) 42
  8 + safe-divide(1,0)

它最终会扩展为 (handler{ ctl raise(msg){ 42 } })(fn(){ 8 + safe-divide(1,0) })。

在效应只声明了一个操作时，若效应和操作的名称相同，我们可以仅通过声明其操作来定义这样的效应，这隐式地定义了一个同名的效应类型：

effect ctl op(<parameters>) : <result-type>
可被翻译为
effect op {
  ctl op(<parameters>) : <result-type>
}

这意味着我们可以将 raise 效应的签名更为简洁地写成：

effect ctl raise( msg : string ) : a

恢复

(Resuming)

效应处理器的强大之处不仅在于我们可以让渡（yield）到最内层的处理器，还在于我们可以带着结果 恢复（resume） 回到调用点。

让我们定义一个 ask<a> 效应，它允许我们获取类型为 a 的上下文值。

effect ask<a>                   // 或 effect<a> ctl ask() : a
  ctl ask() : a

fun add-twice() : ask<int> int
  ask() + ask()

用 ctl 声明的操作在动态绑定时操作内部可以使用 resume 这个一等的函数。

add-twice 函数可以请求数字，但它并不关心这些数字是如何提供的——效应签名仅仅指定了一个上下文API。我们可以通过 恢复(resume) 时带上一个常量来处理，例如：

fun ask-const() : int
  with ctl ask() resume(21)
  add-twice()

其中ask-const()的求值结果为42。

调用 resume(x) 的含义是：把 x 作为该 操作(operation) 调用的结果，并在当初调用操作的那个点继续执行。

或者通过返回随机值，例如：

fun ask-random() : random int
  with ctl ask() resume(random-int())
  add-twice()

现在，ask-random() 处理了 ask<int> 效应，但它自身现在具有 random 效应（参见 std/num/random）。

正如我们在异常示例中看到的，我们不需要调用 resume，也可以直接返回到我们的处理器作用域。例如，我们可能只想处理一次询问(ask)，但之后就放弃了：

fun ask-once() : int
  var count := 0
  with ctl ask()
    count := count + 1
    if count <= 1 then resume(42) else 0
  add-twice()

此处 ask-once() 的取值为 0，因为对 ask 的第二次调用不会恢复执行（并在 ask-once 上下文中直接返回 0）。这种模式可用于在计算仅被允许执行有限步数的场景中实现 燃料(fuel) 的概念。

“fuel” 是计算理论中的一个隐喻性概念——表示计算可消耗的“步数配额“或“执行预算“。每执行一步扣减一点，耗尽即终止。在很多场景(沙箱/多租户、智能合约、交互式程序…)里，我们需要保证计算一定会终止，或者限制不可信代码的资源消耗。EVM 的 gas、Wasmtime 的 fuel metering 都是同一个概念在不同系统中的实例化。

尾恢复操作

(Tail-Resumptive Operations)

ctl 操作是定义操作最通用的方式之一，因为在其中我们有一个能自己决定书写位置的一等的 resume 函数。然而，实践中几乎所有操作结果都是 尾恢复性的(tail-resumptive)：也就是说，它们恰好只恢复一次，并带有最终的结果值。为了方便，我们可以声明 fun 操作——这类操作 在构造上（by construction）就保证了恰好一次尾恢复 ：它的语义被固定的翻译规则钉死为“求值 body 后立即恢复一次“，不可能出现不恢复或恢复多次的情况，即

with fun op(<args>){ <body> }
可翻译成
with ctl op(<args>){ val f = fn(){ <body> }; resume( f() ) }

（该翻译借助中间函数 f 包装操作体，使操作体（<body>）里可能出现的 return 语句能按预期工作：return x 会从中间函数返回 x 并传给 resume，而不是意外退出外层函数）

有了这种语法糖，我们可以用更有趣的 fun 操作来重写之前的 ask-const 示例：

fun ask-const2() : int
  with fun ask() 21
  add-twice()

这也更好地传达了一点：即便 ask 是动态绑定的，它的行为也就像一个普通函数，不会改变控制流。

此外，声明为 fun 的操作比一般的 ctl 操作效率要高得多。Koka编译器使用（广义的）证据传递(evidence passing) 将处理器信息传递到每个调用点。在 add-twice 中对 ask 的调用中，编译器从证据向量(evidence vector)中选择处理器，当操作是尾恢复性的 fun 时，它会像普通函数一样直接调用它（只是针对其上下文调整了证据向量）。与一般的 ctl 操作不同，fun 操作无需向上让渡到处理器、捕获恢复栈，并最终恢复。这使得 fun（和下文 val）操作的性能开销非常接近 虚方法（virtual method） 调用，其效率可以相当高。

为了获得更佳性能，你还可以在效应定义时直接提前声明任何操作定义都必须是尾部可恢复的，具体如下：

effect ask<a>
  fun ask() : a

这限制了 ask 效应的所有处理器定义使用 ask 操作的 fun 定义。但是，它方便了阅读和推理代码，并且编译器可以进一步优化此类调用，因为它不再需要在运行时检查处理器是否恰好将操作定义为尾恢复。

高级
为了获得更佳性能，可以将效应标记为 线性的(linear)。此类效应在静态上保证永远不会使用一般的控制操作，也永远不需要捕获恢复。在编译期间，这消除了进行单子转换的需要，并提升了任何使用此类效应的效应多态的函数（如 map 或 foldr）的性能。线性效应的示例包括状态（st）以及内置效应（如 io 或 console）。

值操作

(Value Operations)

一类常见的操作子集始终以单个值进行尾恢复；这些本质上就是动态绑定变量（但具有静态类型！）。此类操作可以通过以下翻译方式声明为一个val：

with val v = <expr>
可翻译成
val x = <expr>
with fun v(){ x }
可翻译成
val x = <expr>
with ctl v(){ resume(x) }

作为值操作的一个使用示例，可以设想一个从文档生成漂亮字符串的漂亮打印机：

fun pretty( d : doc ) : string

不幸的是，在 pretty 的代码深处，它硬编码了最大显示宽度(width)为40：

fun pretty-internal( line : string ) : string
  line.truncate(40)

为了对宽度进行抽象，我们有几种选择：可以把宽度作为一个常规参数，但这样一来，我们就需要在库中的所有函数里显式地添加这个参数，并手动地在各处传递它。另一种选择是使用一个全局可变变量，但这会引入副作用，并且缺乏模块化。

或者，我们可以将其定义为一种值操作（value operation）：

effect val width : int

这还允许我们像使用常规值一样来引用 width 操作（尽管在内部它实际会调用该操作）。因此，在漂亮打印机（pretty printer）中检查宽度时，可以这样写：

fun pretty-internal( line : string ) : width string
  line.truncate(width)

在使用漂亮打印机时，我们可以将 width 绑定为一个常规的效应处理器：

fun pretty-thin(d : doc) : string
  with val width = 40
  pretty(d)

请注意，我们并不需要改变原始库函数的结构。不过，函数的类型仍然会发生变化，因为这些函数现在需要包含 width 效应，这意味着宽度值必须在某个时候被处理。例如，pretty 的类型变为：

fun pretty( d : doc ) : width string

因为它需要处理 width 效应（也可以称为“为 width : int 定义动态绑定”，或称为“width 能力（capability）”）。

  • ctl：控制操作，调用时会挂起当前执行，捕获续延，handler 可通过 resume 恢复
  • fun：函数操作，像普通函数一样调用，不改变控制流，handler 直接计算并返回
  • val：值操作，本质上是一个动态绑定的值（常量），编译期会被翻译成特殊的 fun 或 ctl

抽象处理器

(Abstracting Handlers)

上一章我们总是把处理器内联写在 with 里。这一章的“抽象“指：handler{...} 表达式本身就是一个函数（一等值），因此可以把处理器抽离成独立的、可命名、可参数化、可复用的函数，再通过 with 注入到任意计算中。下面用写者效应逐步演示。

作为另一个例子，写者(writer) 效应非常常见，其中值由处理器收集。例如，我们可以定义一个 emit 效应来发出消息：

effect fun emit( msg : string ) : ()

fun ehello() : emit ()
  emit("hello")
  emit("world")

我们可以定义一个处理器，例如直接将发出的消息打印到控制台：

fun ehello-console() : console ()
  with fun emit(msg) println(msg)
  ehello()

这里处理器是直接定义的，但我们也可以将为控制台发出消息的处理器抽象为一个单独的函数：

fun emit-console( action )
  with fun emit(msg) println(msg)
  action()

其中 emit-console 的推断类型为 (action : () -> <emit,console|e> a) -> <console|e> a，其中 action 可以使用效应 emit、console 以及任何其他效应 e，而最终效应仅为 <console|e>，因为 emit 效应已被处理器消解。 注意，我们也可以将上述代码写成：

val emit-console2 = handler
  fun emit(msg) println(msg)

因为 handler{ ... } 表达式本身就是一个函数（因此也是一个值）。不过我们通常更倾向于前面的定义，因为它允许添加额外的参数，例如初始状态。 由于 with 的通用性，我们可以像使用常规处理器一样使用抽象化的处理器，我们之前的示例可以写成：

fun ehello-console2() : console ()
  with emit-console
  ehello()

（这展开为 emit-console( fn(){ ehello() } )）。另一个有用的处理器可能会收集所有发出的消息作为字符串列表：

fun emit-collect( action : () -> <emit|e> () ) : e string
  var lines := []
  with handler
    return(x)     lines.reverse.join("\n")
    fun emit(msg) lines := Cons(msg,lines)
  action()

fun ehello-commit() : string
  with emit-collect
  ehello()

这是一个完全处理器（total handler），仅消解 emit 效应。 作为另一个例子，考虑一个带泛型的 catch 处理器，当对我们的异常示例调用 raise 时，它会应用一个处理函数：

fun catch( hnd : (string) -> e a, action : () -> <raise|e> a ) : e a
  with ctl raise(msg) hnd(msg)
  action()

我们现在可以方便地使用 with 语句来处理异常情况：

fun catch-example()
  with catch( fn(msg){ println("error: " ++ msg); 42 } )
  safe-divide(1,0)

高级

catch 处理器有一个有趣的类型，其中 action 可以具有 raise 效应（() -> <raise|e> a）以及可能更多的效应 e，而处理函数 hnd 仅具有效应 e。现在考虑提供一个本身会调用 raise 的处理函数：在这种情况下，catch 的类型会被实例化为：(hnd: (string) -> <raise> a, action : () -> <raise, raise> a ) : <raise> a。这是正确的：action 的（外层）raise 效应被处理并消解，但由于处理函数 hnd 仍可能引发 raise，最终效应仍然包含 raise。

在这里我们看到 Koka 允许重复的效应标签[8]，其中 action 具有实例化的 <raise,raise> 效应类型。这类类型在多态效应存在时会自然出现，并且与运行时证据向量的结构有自然的对应关系（每个嵌套效应处理器对应一个条目）。直观地说，action 的效应表明其外层（最左侧）的 raise 已被处理，但可能还有其他未处理的异常——在这种情况下来自处理函数 hnd，但它们也可以是掩蔽的异常。

返回操作

(Return Operations)

在之前的 emit-collect 示例中，我们看到了 return 返回操作的使用。这种操作会改变处理器动作（action）的最终结果。例如，考虑我们之前使用的自定义异常效应 raise。我们可以定义一个带泛型的处理器，将任何异常动作转换为返回一个 maybe 类型的动作：

fun raise-maybe( action : () -> <raise|e> a ) : e maybe<a>
  with handler
    return(x)      Just(x)   // normal return: wrap in Just
    ctl raise(msg) Nothing   // exception: return Nothing directly
  action()


fun div42()
  (raise-maybe{ safe-divide(1,0) }).default(42)

（div42的函数体脱糖后为 default( raise-maybe(fn(){ safe-divide(1,0) }), 42 )）

一个起名为 state 的效应

为了更全面地了解返回操作的用法，我们来看一下一个起名为 state 的效应，表示一种状态访问方式。在最一般的形式下，它仅包含一个设置（set）操作和一个获取（get）操作：

effect state<a>
  fun get() : a
  fun set( x : a ) : ()

fun sumdown( sum : int = 0 ) : <state<int>,div> int
  val i = get()
  if i <= 0 then sum else
    set( i - 1 )
    sumdown( sum + i )

我们可以通过使用 var 声明来最简便地定义一个带泛型的状态处理器：

fun state( init : a, action : () -> <state<a>,div|e> b ) : <div|e> b
  var st := init
  with handler
    fun get()  st
    fun set(i) st := i
  action()

其中 state(10){ sumdown() } 的求值结果为 55。

在前一个状态示例的基础上，假设我们还希望返回最终状态。一种简洁的做法是再次利用返回操作，将最终结果与最终状态配对在一起：

fun pstate( init : a, action : () -> <state<a>,div|e> b ) : <div|e> (b,a)
  var st := init
  with handler
    return(x)  (x,st)       // pair with the final state
    fun get()  st
    fun set(i) st := i
  action()

其中 pstate(10){ sumdown() } 求值结果为 (55, 0)。

高级

甚至有可能定义一个只包含返回操作的处理程序：这样的处理程序完全不处理任何效应，而仅仅转换函数的最终结果。例如，我们可以用单独的返回处理程序来定义前面的示例，如下所示：

fun pstate2( init : a, action : () -> <state<a>,div|e> b ) : <div|e> (b,a)
  var st := init
  with return(x) (x,st)
  with handler
    fun get()  st
    fun set(i) st := i
  action()

这里有点牵强，但它可以使某些程序的定义更加简洁，例如[5]。

处理器组合

(Combining Handlers)

高级

是什么让效应处理器成为一种良好的控制流抽象？与其他方法相比，它有三个根本性优势：

  1. 效应处理器可以拥有简单的（Hindley-Milner）类型。这与 shift/reset 不同，例如后者需要带有答案（answer）类型的类型规则（因为 shift 的类型取决于其匹配的 reset 的上下文）。
  2. 效应处理器的作用域由处理器定义所限定。这类似于shift/reset，但与call/cc不同。限定 恢复（resumption）的范围 具有多种良好特性，例如高效的实现策略，同时也允许模块化组合（另见Oleg Kiselyov的“反对call/cc”一文）。
  3. 效应处理器可以自由组合。这与一般的单子（monads）不同，后者需要单子转换器以特定方式进行组合。本质上，效应处理器可以自由组合，因为每个效应处理器最终都可以表示为自由单子的实例，而自由单子是可组合的。这也意味着某些单子无法表示为效应处理器（即非代数（non-algebraic）单子）。一个具体的例子是续延（continuation）单子（它可以表达call/cc）。

不过，Koka编译器内部使用单子和shift/reset来编译效应处理器，并将处理器编译为基于多提示分隔控制的内部自由单子。通过内联单子的绑定操作，我们能够生成高效的C代码，只在实际让渡到通用 ctl 操作的情况下才分配续延。

效果处理器的一个出色特性是它们可以自由组合。例如，假设我们有一个函数，当状态为奇数时它会调用 raise：

fun no-odds() : <raise,state<int>> int
  val i = get()
  if i.is-odd then raise("no odds") else
    set(i / 2)
    i

然后我们可以将pstate和raise-maybe处理器组合在一起，以处理这些效果：

fun state-raise(init) : div (maybe<int>,int)
  with pstate(init)
  with raise-maybe
  no-odds()

其中 state<int> 和 raise 这两个效应分别由各自的处理器来处理。请注意，该类型反映出我们总是返回一个对（pair），其第一个元素要么是 Nothing （如果调用了 raise ），要么是带有最终结果的 Just ，而第二个元素则是最终状态。这对应于我们通常如何组合状态和异常：在发生异常时，状态（或堆）被设置为异常发生时的状态。

然而，如果我们以相反的顺序组合这些处理器，我们便会得到一种形式的事务状态——要么抛出一个异常（且没有最终状态），要么得到结果与最终状态组成的对。

fun raise-state(init) : div maybe<(int,int)>
  with raise-maybe
  with pstate(init)
  no-odds()

效应掩蔽

(Masking Effects)

类似于Unix中的信号屏蔽（masking signals），我们可以掩蔽（mask）效应，使其不被最内层的效应处理器处理。表达式 mask<eff>(action) 会模块化地掩蔽 action 内部所有属于 eff 的效应操作。例如，考虑两个嵌套的 emit 操作处理器：

fun mask-emit()
  with fun emit(msg) println("outer:" ++ msg)
  with fun emit(msg) println("inner:" ++ msg)
  emit("hi")
  mask<emit>
    emit("there")

如果我们调用 mask-emit()，它会打印：

inner: hi
outer: there

第二次 emit 调用被掩蔽，因此它会跳过最内层的处理器，随后由外层的处理器处理（即掩蔽只会对于最内层处理器掩蔽一次操作）。

泛型处填入某种效应标签 l 的掩蔽 mask<l> 的类型是 (action: () -> e a) -> <l|e> a ，其中它将效应 l 注入到最终的效应结果 <l|e> 中（尽管掩蔽本身实际上从不执行任何属于 l 的操作——它只是在 action 中掩蔽了所有属于 l 的操作）。

此类型通常会导致重复的效应标签，例如，mask<emit>{ emit("there") } 的效应为 <emit,emit>，表示需要有两个针对 emit 的处理器：在这种情况下，一个应跳过，另一个随后处理被屏蔽的操作。

效应抽象

(Effect Abstraction)

前面的例子不太实用，但一般来说，我们可以使用掩蔽来隐藏高阶函数中的内部效应处理。例如，考虑以下需要处理内部异常的函数：

fun mask-print( action : () -> e int ) : e int
  with ctl raise(msg) 42
  val x = mask<raise>(action)
  if x.is-odd then raise("wrong")   // 内部异常
  x

在这里，mask-print 的类型完全没有暴露出我们为特定代码在内部处理 raise 效应，并且它是完全抽象的——即使动作本身会调用raise，由于 mask<raise> 表达式，它也会巧妙地跳过内部处理器。

如果我们去掉掩蔽，直接调用 action()，那么 action 的推断类型将是 () -> <raise|e> int ，表明 raise 效应会被处理。请注意，这通常是所期望的行为，因为在大多数情况下，当我们定义处理器抽象时，我们希望以特定方式处理效应。根据我们的经验，需要 mask 的情况要少得多。

高级

状态作为一种被组合的效应

掩蔽另一个很好的用例是，在直接使用效应处理器建模状态时，无需使用可变局部变量[1]。我们可以通过两个独立的操作 peek 和 poke 来实现这一点：

effect<a> val peek : a             // 获得状态
effect<a> ctl poke( x : a ) : ()   // 把状态赋为x

我们现在可以将带泛型的状态处理器定义为：

fun ppstate( init : a, action : () -> <peek<a>,poke<a>|e> b ) : e b
  with val peek = init
  with ctl poke(x)
    mask<peek>
      with val peek = x
      resume(())
  action()

在 poke 的处理函数中，我们在一个绑定到新状态的、全新的 peek 处理函数下恢复执行。这意味着，尽管会存在一个不断增长的 peek 处理器“栈”，但为了保持类型不会无限增长，我们需要掩蔽掉对先前 peek 处理函数的任何潜在操作，这正是 mask 存在的必要原因。（另一种理解方式就是直接遵循类型规则： action 具有 peek 效应，并且与 poke 操作定义的效应统一。由于它自身处理了 peek 效应，因此需要借助 mask 将其重新注入回去。）

Note

由于处理器栈随 poke 调用次数无限增长，因此这个示例主要是具有理论上的意义。但是，我们正在研究一种栈粉碎（stack smashing）技术：在运行时检测到掩蔽可以从栈中丢弃处理器帧。）

处理器重写

(Overriding Handlers)

掩蔽的一个常见用途是重写覆盖掉处理器。例如，考虑重写 emit 的行为。

fun emit-quoted1( action : () -> <emit,emit|e> a ) : <emit|e> a
  with fun emit(msg) emit("\"" ++ msg ++ "\"")
  action()

在这里，emit 的处理器调用自身 emit 来实际发出新引用的字符串。为 emit-quoted1 推断出的效应类型是 (action : () -> <emit,emit|e> a) -> <emit|e> a。这并不是最理想的类型，因为它暴露了 action 是在（至少）两个 emit 处理器下被求值的（这使得别人可以在 action 内部使用 mask 来调用外部的 emit 处理器）。

override 关键字保持了类型的一致，并完全重写了之前的处理器，该处理器不再可从 action 中访问。

fun emit-quoted2( action : () -> <emit|e> a ) : <emit|e> a
  with override fun emit(msg) emit("\"" ++ msg ++ "\"" )
  action()

这当然适用于任何处理器或值，例如，要在漂亮打印的例子里临时增加宽度（width），我们可以通过以下方式重写 width：

fun extra-wide( action )
  with override val width = 2*width
  action()

高级

不幸的是，我们无法仅通过掩蔽来模块化地定义重写；如果我们在 emit 处理器之外添加掩蔽，那么操作定义内部的 emit 调用会被掩蔽，从而跳过我们预期的处理器。另一方面，如果我们仅在 action 上添加掩蔽，那么它的所有 emit 调用都将被掩蔽，同样无法命中我们预期的处理器！

对于这种情况，还有另一种原语。表达式 mask behind<eff> 的类型为 (() -> <eff|e> a) -> <eff,eff|e> a，它只遮蔽任何被遮蔽的操作，而不遮蔽直接的操作。override 关键字就是基于这个原语定义的：

with override handler<eff> { <ops> }
<body>
可被翻译成
(handler<eff> { <ops> })(mask behind<eff>{ <body> })

这确保了在 <body> 中的任何操作调用都会转到新定义的处理器，而被掩蔽的操作则会再向上掩蔽一层，从而跳过最内层的两个处理器。

副作用隔离​

(Side-effect Isolation)

恢复多于一次

由于 resume 是一等函数（嗯，几乎是），可以将其存储在列表中，例如用于实现调度器，但也可以多次调用它。这可以用于实现回溯或概率编程模型。

多次恢复的一个常见示例是 choice 效应：

effect ctl choice() : bool

fun xor() : choice bool
  val p = choice()
  val q = choice()
  if p then !q else q

一种可能的效应实现方式是就使用随机数：

fun choice-random(action : () -> <choice,random|e> a) : <random|e> a
  with fun choice() random-bool()
  action()

其中 choice-random(xor) 会随机返回 True 或 False。

不过，我们也可以多次恢复，一次使用 False ，一次使用 True ，以返回所有可能的结果。这也会将处理程序类型改为返回该action所有结果的列表，并且我们需要一个 返回子句(return clause)，将操作的结果包装在单元素列表中：

fun choice-all(action : () -> <choice|e> a) : e list<a>
  with handler
    return(x)    [x]
    ctl choice() resume(False) ++ resume(True)
  action()

其中 choice-all(xor) 返回 [False,True,True,False]。 多次恢复与状态效应的交互会产生有趣的结果。考虑以下同时使用 choice 和 state 的示例：

fun surprising() : <choice,state<int>> bool
  val p = choice()
  val i = get()
  set(i+1)
  if i>0 && p then xor() else False

我们可以通过两种有趣的方式组合这些处理器：

fun state-choice() : div (list<bool>,int)
  pstate(0)
    choice-all(surprising)

fun choice-state() : div list<(bool,int)>
  choice-all
    pstate(0,surprising)

在 state-choice() 中，pstate 是外层处理器，并像是一个全局状态，覆盖 choice-all 中的所有恢复链。因此，在第一次恢复之后，surprising 中的 i>0（&&）p 条件为真，我们得到 ([False,False,True,True,False],2)。

在 choice-state() 中，pstate 是内部处理器，并变得像事务性状态，此时该状态对于choice-all中的每个恢复分支而言都是局部的。现在，i一开始总是为0，因此我们得到[(False,1),(False,1)]。

高级

这个示例还展示了 var 状态在恢复时如何作为栈的一部分被正确保存和复原，而这对效应处理器的正确组合至关重要。如果 var 声明改为堆分配或用引用捕获，它们将不再局限于各自的作用域，副作用可能会在不同恢复之间“泄漏”。

initially与finally函数

(Initially and Finally)

对于任意效应处理器，在与文件等外部资源交互时我们需要格外小心。一般来说，操作可能永远不会恢复（如异常）、恰好恢复一次（提供通常的线性控制流），或者恢复多次。为了稳健地处理这些不同情况，Koka 提供了 finally 和 initially 函数。

std/core/hnd/finally: forall<a,e> (fin : () -> e (), action : () -> e a) -> e a

std/core/hnd/initially: forall<a,e> (init : (int) -> e (), action : () -> e a) -> e a

假设我们有以下针对文件句柄的低级文件操作：

type fhandle
fun fopen( path : string )   : <exn,filesys> fhandle
fun hreadline( h : fhandle ) : <exn,filesys> string
fun hclose( h : fhandle )    : <exn,filesys> ()

使用这些原语，我们可以声明一个 fread 效应来从文件中读取。

effect fun fread() : string

fun with-file( path : string, action : () -> <fread,exn,filesys|e> a ) : <exn,filesys|e> a
  val h = fopen(path)
  with handler
    return(x)   { hclose(h); x }
    fun fread() hreadline(h)
  action()

然而，就目前而言，如果在 action 内部使用了异常效果（即，或任何永不恢复的操作），它无法关闭文件句柄。finally 函数能处理这些情况，其第一个参数是一个函数，该函数在正常返回或为不恢复操作而展开时总是会被执行。因此，编写 with-file 更健壮的方式如下：

fun with-file( path : string, action : () -> <fread,exn,filesys|e> a ) : <exn,filesys|e> a
  val h = fopen(path)
  with finally
    hclose(h)
  with fun fread()
    hreadline(h)
  action()

当前的定义对于从不恢复或只恢复一次的操作是稳健的——但一旦需要恢复多次，问题就出现了。如果有人在 action 内部调用 choice，那么第二次恢复时文件句柄会再次被关闭，这很可能不是预期的行为。目前有研究正在探索利用类型系统在静态层面阻止这种情况的发生。

另一种处理多次恢复的方式是使用 initially 函数。该函数接受两个参数：第一个参数是一个函数，它会在 initially 首次被求值时被调用，并且之后每当特定恢复被多次恢复时也会被调用。

高级

原始控制

使用 raw ctl 定义原始控制操作时，这些操作不会自动完成终结（finalize）。借助 raw ctl 可以利用隐式绑定的恢复上下文 rcontext 要么恢复执行（如 rcontext.resume(x)），要么终结恢复（如 rcontext.finalize），后者会运行所有 finally 处理器以清理资源。这使得 rcontext 可以作为一等值存储，以便稍后在不同作用域中恢复或终结。当然，使用时需格外谨慎，因为现在确保恢复最终被恢复或终结（以便能释放任何资源）的责任完全在程序员身上。

线性效应

(Linear Effects)

普通代数效应（algebraic effects）的灵活性来源于：一个操作（operation）的 resume 续延可以被调用零次、一次或多次——这赋予了异常处理（零次）、非确定性搜索（多次）、生成器（一次）等丰富语义。但这种灵活性是有代价的：编译器通常必须为效应操作捕获续延（continuation），并通过单子化翻译（monadic translation）将其表示为首类值，以便运行时能灵活地控制续延的调用次数。

线性效应是一类受到严格控制流线性（control-flow linearity）约束的效应——它要求其所有操作的 resume 必须恰好被调用一次，且位于处理子句的尾部（tail-resumptive），同时这些操作自身也只能使用线性效应。这种约束让编译器可以完全免除单子化翻译，使得“仅使用线性效应的代码“在运行时更紧凑、更高效。

控制流线性：四种分类

微软研究院的技术报告《Qualified Effect Types》形式化了控制流线性的概念。一个函数（或表达式）的控制流线性属性可分为四类 ：

分类英文返回次数典型代表
线性linear恰好一次普通纯函数、尾恢复操作
中止性abortive永不返回abort、exit、无限循环
仿射性affine至多一次可能抛异常的函数
自由性wild可能零次或多次非确定性选择、回溯搜索

Koka 的核心洞察是 ：在 Koka 这类基于代数效应的语言中，改变控制流的唯一途径就是通过效应操作。因此，如果一个函数只使用被线性处理器处理的效应操作，那么这个函数本身就是控制流线性的（恰好返回一次）。

基于此，Koka 允许在效应声明中标注其控制流线性属性 ：

effect abort exn    { throw(e: exception): a }   // 中止性
effect linear out   { println(x: string): () }   // 线性
effect wild amb     { flip(): bool }             // 自由性

整个效应行（effect row）的线性属性定义为其各组成效应线性属性的 join（上确界）。

线性效应的定义与约束

当用户说“线性效应“时，指的是满足以下三条约束的效应 ：

  1. 操作是尾恢复的（tail-resumptive）：处理子句中 resume 的调用必须出现在尾部位置——即 resume(...) 是子句返回前的最后一个动作。这保证了 resume 在编译后可以展开为一个简单的跳转/循环回边，而非需要捕获续延。

  2. resume 恰好调用一次：处理子句必须且只能调用 resume 一次。这排除了：

    • 零次调用（如异常处理 throw → abortive）
    • 多次调用（如非确定性 flip → wild）

  3. 操作只能使用线性效应：该效应的操作本体（以及其处理子句）自身只能引用其他线性效应，从而形成封闭的“线性效应世界“。

这三条约束共同保证了：任何只使用线性效应的表达式，在运行时的控制流是线性的（恰好返回一次） 。

为什么能免除单子化翻译

普通效应操作的 resume 续延是**多射（multi-shot）**的——它可能被调用零次或多次。为了让程序能灵活控制调用次数，编译器必须：

  • 将续延捕获为堆分配的首类值（continuation object）
  • 通过证据传递（evidence passing） 或类似的机制，在调用栈中传递效应操作的字典
  • 在处理子句中通过 resume(...) 显式调用续延

这就是所谓的“单子化翻译“——效应的存在迫使编译器把代码重写成带有续延传递的风格，带来：

  • 堆分配开销：续延对象需要分配内存
  • 间接调用开销：resume 是通过函数指针/字典调用的
  • 代码膨胀：需要生成续延的封装与传递逻辑

而线性效应的 resume 恰好被调用一次且位于尾部——这让编译器可以做一个关键优化：尾恢复处理子句（tail-resumptive handler）可以直接编译为简单的循环，无需堆分配、无需捕获续延、无需协程机制 。

技术报告《Qualified Effect Types》证明 ：如果表达式的类型声明它只使用线性效应，那么运行时的控制流确实是线性的。这一类型系统保证与效应处理器的结合，让我们可以在局部推理程序——确保外部资源的使用约束得到满足，同时完全免除单子化翻译的开销。

示例：线性效应 vs 普通效应

普通效应（需要续延捕获）

// 普通 state 效应——ctl 表示 control 效应，续延是多射的
effect state
  ctl get(): int
  ctl put(n: int): ()

// 标准 state 处理器——resume 被调用恰好一次，但不在尾部
// 因为 resume 的结果还要参与后续计算（如 resume(s)(s)）
fun state(action: () -> <state|e> a): e (a, int)
  var s := 0
  with handler
    return(x) -> (x, s)
    ctl get() -> resume(s)           // resume 的结果被使用
    ctl put(n) -> { s := n; resume(()) }
  action()

这里 ctl get() 的 resume(s) 虽然被调用一次，但 resume 的结果 resume(s) 还要被应用 (s)——resume 不在尾部位置。编译器必须捕获续延。

线性效应（尾恢复，免除单子化）

// 线性 out 效应——操作是尾恢复的
effect linear out
  println(x: string): ()

// 线性处理器——resume 恰好调用一次且在尾部
fun capture-output(action: () -> <out|e> a): e (a, list<string>)
  var lines := []
  with handler
    return(x) -> (x, lines.reverse)
    println(msg) -> {              // 尾恢复子句
      lines := Cons(msg, lines)
      resume(())                    // resume 在尾部，恰好调用一次
    }
  action()

println 的处理子句中 resume(()) 是最后一个动作——尾恢复。编译器可以将其编译为一个简单的循环：每次 println 操作被“执行“时，实际上就是循环的一次迭代，无需堆分配续延。

多次 resume 的对比

// 非确定性选择——wild 效应，resume 被调用两次
effect amb
  flip(): bool

fun collect-all(action: () -> <amb|e> a): e list<a>
  with handler
    return(x) -> [x]
    flip() ->
      val false-branch = resume(False)
      val true-branch = resume(True)   // resume 被调用两次 → wild
      false-branch ++ true-branch
  action()

flip() 的处理子句调用 resume 两次——这是 wild 效应，必须捕获续延（实际上需要捕获两份续延，或用其他机制实现回溯）。这与线性效应的“恰好一次、尾部“形成鲜明对比。

性能收益

对于仅使用线性效应的程序，Koka 编译器可以：

  1. 消除续延堆分配：因为 resume 尾恢复且调用一次，编译器可以将其编译为直接的跳转/循环回边，无需在堆上分配续延对象 。

  2. 消除证据传递开销：普通效应需要通过证据传递（evidence passing）在调用栈中传递操作字典 ；线性效应因为控制流是线性的，可以通过更直接的代码生成来避免这部分开销。

  3. 生成紧凑代码：尾恢复处理子句编译后等价于一个简单的 while 循环或尾递归——与手写命令式代码效率相当 。

技术报告中的实证 ：对于迭代、可选（optional）、状态（state）、读取器（reader）等常见模式——这些都可以表达为线性效应——其运行时开销与直接命令式实现相比，没有任何额外代价。

线性效应的类型级保证

Koka 的类型系统通过 qualified types 框架 传播控制流线性约束。当你写一个函数：

fun process(items: list<int>): <out|e> int
  match items
    Cons(x, xs) -> { println(x.show); process(xs) }
    Nil -> 0

类型 <out|e> 中的 out 是一个 linear 效应。编译器由此推断：process 的控制流是线性的（恰好返回一次），且它只使用线性效应。这一保证让：

  • 局部推理成为可能：你可以确保外部资源的使用约束得到满足，而无需理解完整的程序
  • 优化是安全的：编译器可以放心地免除单子化翻译，因为类型系统已经静态保证了控制流线性

限制与注意事项

线性效应虽然高效，但也有其限制：

⚠️ 操作必须是尾恢复的：如果你写的线性效应处理子句中 resume 不在尾部（如 resume(x) + 1），编译器要么报错，要么退回到普通效应翻译。Koka issue #72 记录了这样一个案例：effect fun() { resume(f()) } 是尾恢复的，而 fun() { f() } 经效应行展开后会包裹 .open 调用，导致尾恢复分析失效 ——这说明尾恢复分析对语法形式敏感。

⚠️ resume 恰好一次：线性效应禁止零次或多次 resume。如果需要异常语义（零次）或非确定性（多次），必须使用普通效应（abortive 或 wild）。

⚠️ 闭世界假设：线性效应构成封闭的“线性世界“——其操作只能使用其他线性效应。如果需要与 wild/abortive 效应交互，需要通过效应行的 join 操作，此时整体线性属性退化为较弱的分类（affine 或 wild）。

与其他语言的对比

线性效应的思想与以下概念相关但不同：

  • Haskell 的 LinearTypes 扩展：a %1 -> b 要求参数被使用恰好一次——这是值级别的线性，而 Koka 的线性效应是控制流级别的线性
  • Clean 的唯一性类型（uniqueness types）：保证引用被使用恰好一次，用于安全 in-place 更新
  • Rust 的所有权系统：通过所有权保证每个值有且仅有一个所有者

Koka 的线性效应独特之处在于：它将控制流线性编码进效应类型系统，与 Koka 既有的行多态效应类型（row-polymorphic effect types）无缝集成 。你无需显式标注 %1 或所有权修饰符——只需声明效应为 linear，编译器会自动跟踪并优化。

小结

线性效应是 Koka 类型系统的一项强大特性：

  • 语法层面：在 effect 声明中标注 linear 关键字，约束其操作为尾恢复且 resume 恰好一次
  • 语义层面：线性效应保证控制流线性（恰好返回一次），且操作只能使用其他线性效应
  • 编译层面：因为 resume 尾恢复且调用一次，编译器可以完全免除单子化翻译，将处理子句编译为简单的循环，无堆分配、无续延捕获、无协程机制
  • 性能层面：仅使用线性效应的代码，其运行时效率与手写命令式代码相当 ——迭代、状态、读取器等常见模式零开销
  • 安全层面：类型系统静态保证控制流线性，使局部推理成为可能，确保外部资源使用约束得到满足

线性效应体现了 Koka “类型级效应跟踪“与“零开销抽象“设计哲学的完美结合——你用 linear 关键字给编译器一个承诺，编译器回报你极致的运行时效率。

📌 译注：本章节核心概念对应——

  • linear effect：线性效应
  • tail-resumptive：尾恢复（指 resume 调用位于处理子句的尾部位置）
  • control-flow linearity：控制流线性
  • monadic translation：单子化翻译
  • exactly once resume：恰好一次恢复

参考微软研究院技术报告《Qualified Effect Types — Taming Control-Flow through Linear Effect Handlers》（MSR-TR-2023-42） ，该报告由 Jonathan Brachthäuser 实习期间在 Microsoft Research 完成，形式化了控制流线性的类型理论，并证明了“若表达式类型声明仅使用线性效应，则运行时控制流是线性的“这一核心定理 。

关键要点：线性效应通过约束操作“尾恢复且 resume 恰好一次“，让编译器能完全免除单子化翻译，将效应处理编译为高效的循环结构。这是 Koka 实现“零开销效应处理“的核心机制之一——与证据传递（evidence passing）技术 互补，共同保证了 Koka 效应系统在提供强大表达力的同时，不牺牲运行时性能。

具名处理器与作用域处理器

(Named and Scoped Handlers)

普通代数效应处理器（handler）是匿名的——当同一效应有多个活跃的处理器实例时，操作（operation）无法区分该由哪一个实例来处理。这在需要“同时存在多个同类资源“的场景下会成为表达力的瓶颈：比如同时打开多个文件、维护多个独立的堆（heap）、或在同一个计算中使用多个独立的 reader 环境。

Koka 通过**具名处理器（named handlers）与作用域处理器（scoped handlers）**解决了这个问题——让处理器拥有词法上可区分的“名字“，使操作可以通过名字指向特定的处理器实例。

为什么需要具名处理器

考虑经典的 reader 效应（只读环境）：

effect reader
  fun ask(): int

使用匿名处理器时：

fun read(x, action)
  with handler
    fun ask() x
  action()

这里的 ask() 操作会被最近的匿名 reader 处理器处理。但如果我们想同时使用两个 reader 环境——例如 f₁ 提供 42，f₂ 提供 7——匿名处理器就无法区分两次 ask() 调用该由谁处理。

具名处理器让处理器拥有一个首类（first-class）的名字，操作可以通过这个名字显式地指向特定的处理器实例。

具名效应与具名处理器的语法

声明一个具名效应：

named effect file
  fun read-line(): string

named 关键字标记这是一个具名效应——它的操作必须通过具体的处理器名字来调用。

创建具名处理器实例：

fun file(fname, action)
  var content := read-text-file(fname.path).lines
  with f = named handler
    fun read-line()
      match content
        Nil -> ""
        Cons(x, xx) -> { content := xx; x }
  action(f)

这里：

  • named handler { ... } 创建一个具名处理器，其名字绑定到 f
  • f 是一个首类值——可以传递、可以放入数据结构、可以作为函数参数
  • action(f) 将名字 f 传入被处理的计算，使得 action 内部可以通过 f.read-line() 显式调用这个特定实例的操作

示例：同时操作两个文件

具名处理器的威力在于——多个同类资源可以独立共存：

pub fun main()
  with f1 = file("foo.txt".path)
  with f2 = file("bar.txt".path)
  println( f1.read-line() ++ f2.read-line() )

由于 f1 和 f2 是词法上不同的名字，f1.read-line() 与 f2.read-line() 调用的是两个不同的处理器实例——分别从 foo.txt 和 bar.txt 读取第一行。如果没有具名处理器，两次 read-line() 调用都会解析到同一个处理器，无法区分文件来源。

Koka 官方 OOPSLA’22 论文明确指出 ：具名处理器让程序员可以“deal with each file independently, and easily read the content of a particular file in the presence of multiple opened files“——这正是具名处理器的核心价值。

作用域处理器：类型级的作用域安全

具名处理器解决了“多个实例共存“的问题，但还有一个安全隐患：action 可能将处理器名字 f 逃逸到处理器的作用域之外。例如：

var escaped: file? = None

fun file(fname, action)
  var content := read-text-file(fname.path).lines
  with f = named handler
    fun read-line() ...
  action(f)   // 危险：action 可能把 f 保存到 escaped 中

如果 action 将 f 赋值给全局变量 escaped，那么 file 返回后，escaped 仍然持有 f——但此时 f 对应的处理器作用域已经结束，调用 escaped.read-line() 会导致未定义行为。

作用域处理器（scoped handler） 通过类型系统静态地阻止这种逃逸：

named scoped effect file<s>
  fun read-line(): string

fun file(fname: string, action: forall s. file<s> -> <scope<s>|e> a): e a
  var i := 0
  with f <- named handler
    fun read-line()
      i := i + 1
      (fname ++ ": line " ++ i.show)
  action(f)

关键变化：

  1. 效应参数化：file<s> 中的 s 是一个作用域变量（scope variable），标识这个特定处理器实例的作用域
  2. rank-2 多态：action 的类型 forall s. file<s> -> <scope<s>|e> a 表示——action 对任意作用域变量 s 都成立，但 s 不能逃逸出 action 的调用
  3. scope<s> 效应：action 包含 scope<s> 效应，这意味着它只能在作用域 s 内执行——一旦 action 返回，scope<s> 就被 discharge（解除），s 不能再被使用

由于 rank-2 多态的约束，action 无法将 f（类型为 file<s>）逃逸到外部——因为任何试图在 action 返回后使用 f 的代码，都无法提供匹配的 s。Koka 类型检查器会在编译期拒绝这种逃逸。

作用域类型的机制

作用域处理器依赖于 Koka 的**作用域类型（scope types）**机制。带 ::S 种类注解的类型构造子可以创建作用域变量 ：

type scope :: S -> X

scope<s> 是一个类型——它代表“在作用域 s 内有效“。当处理器 f 的类型为 file<s> 时，任何使用 f 的操作都会产生 scope<s> 效应。由于 file 函数在 action 返回时 discharge 了 scope<s>，action 内部获得的 f 无法被带回外部。

Koka 的 nmd 与 scope 类型 ：

// 具名效应的默认总括效应
pub type nmd :: X

// 作用域效应：确保具名效应无法逃逸出其作用域
pub type scope :: S -> X

完整示例：具名与作用域文件处理器对比

普通具名处理器（Figure 8 左）

named effect file
  fun read-line(): string

fun file(fname: path, action: file -> <exn,fsys|e> a): <exn,fsys|e> a
  var ls := read-text-file(fname).lines
  with f = named handler
    fun read-line()
      match ls
        Nil -> ""
        Cons(x, xx) -> { ls := xx; x }
  action(f)

具名与作用域处理器（Figure 8 右）

named scoped effect file<s>
  fun read-line(): string

fun file(fname: path, action: forall<s. file<s> -> <scope<s>,fsys|e> a): <fsys|e> a
  var ls := read-text-file(fname).lines
  with f <- named handler
    fun read-line()
      match ls
        Nil -> ""
        Cons(x, xx) -> { ls := xx; x }
  action(f)

两段代码的运行时行为完全一致——区别在类型层面：作用域版本通过 forall<s> 与 scope<s> 保证 action 不能将 f 逃逸到 file 函数之外。

更丰富的应用场景

Koka 官方 samples/handlers/named 目录提供了多个展示具名与作用域处理器的实例 ：

样例演示内容论文章节
ask.kk简单的 reader 效应（具名处理器入门）§2.2
file.kk非作用域的文件效应§2.3.1 / Figure 1
file-scoped.kk作用域的文件效应类似 Figure 4
heap.kk首类堆（first-class heap）§3.2.4 / Figure 5
unify.kk合一算法（unification）效应§7.2
ask-poly.kk多态 reader 效应—

其中 heap.kk 展示了一个精妙的用法 ：通过具名处理器，Koka 不需要内置的状态机制——可以完全用具名处理器表达首类堆（first-class heap），动态创建引用（references）。每个 newref 操作在处理器 h 的作用域内创建新引用，引用本身携带处理器名字 h，从而保证引用的访问被限定在正确的堆实例中。

具名处理器与匿名处理器的关系

具名处理器是匿名处理器的超集——匿名处理器可以视为“名字不可见“的特殊情况。Koka 的 with 语句语法统一了两者 ：

// 匿名处理器：名字不可见
with handler
  fun ask() 42
action()

// 具名处理器：名字 f 绑定到处理器
with f = named handler
  fun ask() 42
action(f)

// 作用域具名处理器：f 携带作用域变量
with f <- named handler
  fun ask() 42
action(f)

with 语句的两种变体 ：

  • with f = ... —— 绑定变体，用于具名处理器
  • with f <- ... —— 绑定变体，用于作用域具名处理器（< 暗示类型级约束）

设计意义

具名与作用域处理器体现了 Koka 效应系统的核心设计哲学——效应即能力（effect as capability）：

  1. 模块化：处理函数不再依赖全局单例效应，而是显式地传递处理器名字——这让多个同类资源可以独立共存
  2. 首类性：处理器名字是首类值，可以自由传递、存入数据结构——这为构建复杂效应组合（如首类堆、神经网络）提供了基础
  3. 类型安全：作用域处理器通过 rank-2 多态与作用域类型，在编译期静态保证处理器无法逃逸其作用域
  4. 零开销抽象：具名与作用域处理器在编译后等价于手工管理的状态——没有运行时开销

Koka 论文总结道 ：具名处理器让程序员可以“deal with each file independently“——这正是代数效应系统走向工程实用化的关键一步。通过将处理器名字化、首类化、作用域化，Koka 的效应系统能够自然地表达现实世界中“多实例、有边界“的资源管理模式。

本章小结

概念关键字核心特征
具名效应named effect操作必须通过处理器名字调用
具名处理器with f = named handler处理器绑定到首类名字 f，可传递
作用域效应named scoped effect file<s>效应参数化作用域变量 s
作用域处理器with f <- named handleraction 受 forall s. 约束，f 无法逃逸

具名处理器解决了“多个同类效应实例共存“的问题；作用域处理器在此基础上通过类型系统静态保证处理器名字不会逃逸到其作用域之外。两者共同构成了 Koka 表达复杂、模块化、类型安全的效应处理的基础。

📌 译注：

  • named handler → 具名处理器
  • scoped handler → 作用域处理器
  • named effect → 具名效应
  • scope variable → 作用域变量
  • rank-2 polymorphism → 二阶多态
  • first-class name → 首类名字
  • effect as capability → 效应即能力

参考：Koka OOPSLA’22 论文《First-Class Names for Effect Handlers》 与微软技术报告 MSR-TR-2021-10 。示例代码语法以当前 Koka 版本（参见 samples/handlers/named/ ）为准——不同版本在 with f = named handler 与 with f <- named handler 的语法细节上可能有差异，但语义一致。

关键要点：具名处理器让同一效应的多个实例可以词法区分、独立共存，处理器名字是首类值；作用域处理器在此基础上通过 rank-2 多态与作用域类型，在类型层面静态保证处理器无法逃逸其作用域。这是 Koka 效应系统表达“多实例、有边界“资源管理模式的基石，也是代数效应走向工程实用化的关键机制 。

FBIP(Functional but In-Place): 函数式但原地

借助 Perceus 复用分析，我们能够编写出这样的算法：在可能的情况下动态适应并采用原地修改（而在持久使用时则采用复制）。重要的是，你可以信赖这种优化确实会发生，例如，参见 match 模式，并在每个分支中将它们与相同大小的构造器配对。

这种编程风格催生了一个我们称之为FBIP的新范式：“函数式但原地”。正如尾调用优化让我们能用常规函数调用来描述循环，复用分析让我们能以纯函数式方式描述原地修改的指令式算法（同时也能实现持久性）。

Note

FBIP仍属于活跃研究领域。特别是，我们希望增加添加注解的方式，以确保复用确实发生。

红黑树再平衡

(Tree Rebalancing)

作为一个示例，我们考虑向红黑树[3]中插入节点。该示例的多态版本位于Koka安装后的samples目录中，可通过 :l samples/basic/rbtree 加载。我们将红黑树定义为：

type color
  Red
  Black

type tree
  Leaf
  Node(color: color, left: tree, key: int, value: bool, right: tree)

红黑树具有一个不变性质，即从根节点到任意叶节点的黑色节点数量相同，并且红色节点永远不会是红色节点的父节点。这两者共同确保了树始终是平衡的。在插入节点时，需要通过在必要时重新平衡节点来维护这些不变性质。Okasaki 的算法[19]以优雅且函数式的方式实现了这一点：

fun balance-left( l : tree, k : int, v : bool, r : tree ): tree
  match l
    Node(_, Node(Red, lx, kx, vx, rx), ky, vy, ry)
      -> Node(Red, Node(Black, lx, kx, vx, rx), ky, vy, Node(Black, ry, k, v, r))
    ...

fun ins( t : tree, k : int, v : bool ): tree
  match t
    Leaf -> Node(Red, Leaf, k, v, Leaf)
    Node(Red, l, kx, vx, r)
      -> if k < kx then Node(Red, ins(l, k, v), kx, vx, r)
         ...
    Node(Black, l, kx, vx, r)
      -> if k < kx (&&) is-red(l) then balance-left(ins(l,k,v), kx, vx, r)
         ...

Koka编译器会对 balance-left 函数进行内联。这样一来，在 ins 函数中，每个匹配到的 Node 构造函数都会对应一个 Node 分配——如果考虑所有分支，我们可以看到，要么匹配一个 Node 并分配一个，要么匹配三个深层的 Node 并分配三个。实际上，在快速路径中，每个 Node 都会被直接重用，而无需进行任何分配！研究生成的代码时，我们可以发现，Perceus会在快速路径中直接原地为Node的字段赋值，这与C语言中通常的非持久化再平衡算法做法非常相似。

这本质上意味着，对于唯一的树结构，上述纯函数算法会在运行时自适应地转变为一种原地修改的再平衡算法（且无需额外分配）。此外，如果我们以持久化方式使用树[20]，并且树被共享或部分共享，算法会自适应地仅复制树中共享的脊（不多复制任何部分），同时对任何非共享部分仍进行原地再平衡。

莫里斯遍历

(Morris Traversal)

作为FBIP的另一个例子，考虑按照中序顺序对二叉树中的所有元素应用函数 f，如 tmap-inorder 示例所示：

type tree
  Tip
  Bin( left: tree, value : int, right: tree )

fun tmap-inorder( t : tree, f : int -> int ) : tree
  match t
    Bin(l,x,r) -> Bin( l.tmap-inorder(f), f(x), r.tmap-inorder(f) )
    Tip        -> Tip

这已经相当高效了，因为当 t 唯一时，所有的 Bin 和 Tip 节点都会被原地复用。然而，tmap 函数并不是尾递归的，因此它使用的栈空间与树的深度成正比。

void inorder( tree* root, void (*f)(int) ) {
  tree* cursor = root;
  while (cursor != NULL /* Tip */) {
    if (cursor->left == NULL) {
      // no left tree, go down the right
      f(cursor->value);
      cursor = cursor->right;
    } else {
      // has a left tree
      tree* pre = cursor->left;  // find the predecessor
      while(pre->right != NULL && pre->right != cursor) {
        pre = pre->right;
      }
      if (pre->right == NULL) {
        // first visit, remember to visit right tree
        pre->right = cursor;
        cursor = cursor->left;
      } else {
        // already set, restore
        f(cursor->value);
        pre->right = NULL;
        cursor = cursor->right;
      }
    }
  }
}

1968年，Knuth提出了在不使用额外栈或堆空间的情况下按中序遍历树的问题[7]（对于不熟悉该问题的读者，不妨先用你最喜欢的命令式语言尝试一下，就会发现这并不容易做到）。自那以后，文献中出现了许多解决方案。其中一种特别优雅的方案由Morris[18]提出。这是一种原地修改算法，通过交换树中的指针来“记住”哪些部分尚未访问。本教程不打算给出完整解释，但这里附带展示了一个C语言实现。该遍历本质上利用右线索树来跟踪待访问的节点。不过，该算法相当微妙。由于它将树转换为中间图，我们需要对所谓的Morris循环[16]陈述不变量，以证明其正确性。

我们可以利用FBIP技术推导出一个函数式且更直观的解决方案。我们首先定义一个显式的访问者数据结构，用于跟踪树中仍需访问的部分。在Koka中，我们将此数据类型定义为 visitor：

type visitor
  Done
  BinR( right:tree, value : int, visit : visitor )
  BinL( left:tree, value : int, visit : visitor )

以下是翻译后的带 LaTeX 的 Markdown 文本：

(顺便一提，Conor McBride[17] 描述了我们可以如何为任意递归类型 $\mu x. F$ 泛型地推导出一个 zipper [6] 访问器，其形式即为该类型的导数所构成的列表，即 \(list(\frac{\partial}{\partial x} F \mid_{x=\mu x.F})\)。在我们这个案例中，归纳型 tree 类型的代数表示为 \(\mu x. 1 + x \times \text{int} \times x \cong \mu x. 1 + x^2 \times \text{int}\)。通过计算导数 \(list(\frac{\partial}{\partial x} (1 + x^2 \times \text{int}) \mid_{x=\text{tree}})\) 并进行进一步的化简，我们得到 \(\mu x. 1 + (\text{tree} \times \text{int} \times x) + (\text{tree} \times \text{int} \times x)\)，这恰好对应于我们所定义的 visitor 数据类型。)

我们还记录在树中移动的方向（direction），是向上(Up)还是向下(Down)。

type direction
  Up
  Down

我们通过使用一个空的访问者向下遍历树来开始遍历，表示为 tmap(f, t, Done, Down)。

fun tmap( f : int -> int, t : tree, visit : visitor, d : direction )
  match d
    Down -> match t     // going down a left spine
      Bin(l,x,r) -> tmap(f,l,BinR(r,x,visit),Down) // A
      Tip        -> tmap(f,Tip,visit,Up)           // B
    Up -> match visit   // go up through the visitor
      Done        -> t                             // C
      BinR(r,x,v) -> tmap(f,r,BinL(t,f(x),v),Down) // D
      BinL(l,x,v) -> tmap(f,Bin(l,x,t),v,Up)       // E

核心思想是：我们要么已完成Done（C），要么在沿着左脊柱向下走时，将所有仍需访问的右树记录在一个BinR（A）中；或者，在再次向上走（B）时，将我们刚刚构造的左树记录为一个BinL，同时访问右树（D）。当我们回到顶部（E）时，我们用结果值恢复原始树。请注意，我们在分支D中将函数f应用于保存的值（因为我们按中序访问），但函数式实现使得通过分别在分支A或分支E应用f，可以轻松指定前序或后序遍历。

观察每个分支，我们可以看到每个Bin与一个BinR匹配，每个BinR与一个BinL匹配，最后每个BinL与一个Bin匹配。由于它们大小相同，如果树是唯一的，则每个分支在运行时原地更新树节点而无需任何分配，其中visiter访问者结构在遍历树时实际上覆盖在树节点之上。由于所有tmap调用都是尾调用，这也会编译成一个紧凑的循环，因此不需要额外的栈空间或堆空间。

最后，就像重新平衡树插入一样，所指定的算法仍然是纯函数式的：当传入唯一树时，它使用原地更新；但也能优雅地适应持久化情况，即输入树被共享，或输入树的部分被共享，此时会仅复制树的那些共享部分。

引用目录

[1] Dariusz Biernacki, Maciej Piróg, Piotr Polesiuk, and Filip Sieczkowski. “Handle with Care: Relational Interpretation of Algebraic Effects and Handlers.” Proc. ACM Program. Lang. 2 (POPL’17 issue): 8:1–8:30. Dec. 2017. doi:10.1145/3158096.

[2] Nicholas Boucher, and Ross Anderson. “Trojan Source: Invisible Vulnerabilities.” Preprint. 2021. arXiv:cs.CR/2111.00169.

[3] Leo J Guibas, and Robert Sedgewick. “A Dichromatic Framework for Balanced Trees.” In 19th Annual Symposium on Foundations of Computer Science (sfcs 1978), 8–21. IEEE. 1978.

[4] Carl A. Gunter, Didier Rémy, and Jon G. Riecke. “A Generalization of Exceptions and Control in ML-like Languages.” In Proceedings of the Seventh International Conference on Functional Programming Languages and Computer Architecture, 12–23. FPCA ’95. ACM, La Jolla, California, USA. 1995. doi:10.1145/224164.224173.

[5] Daniel Hillerström, and Sam Lindley. “Liberating Effects with Rows and Handlers.” In Proceedings of the 1st International Workshop on Type-Driven Development, 15–27. TyDe 2016. Nara, Japan. 2016. doi:10.1145/2976022.2976033.

[6] Gérard P. Huet. “The Zipper.” Journal of Functional Programming 7 (5): 549–554. 1997.

[7] Donald E. Knuth. The Art of Computer Programming, Volume 1 (3rd Ed.): Fundamental Algorithms. Addison Wesley Longman Publishing Co., Inc. 1997.

[8] Daan Leijen. “Extensible Records with Scoped Labels.” In Proceedings of the 2005 Symposium on Trends in Functional Programming, 297–312. 2005.

[9] Daan Leijen. “Structured Asynchrony with Algebraic Effects.” In Proceedings of the 2nd ACM SIGPLAN International Workshop on Type-Driven Development, 16–29. TyDe 2017. Oxford, UK. 2017. doi:10.1145/3122975.3122977.

[10] Daan Leijen. “Type Directed Compilation of Row-Typed Algebraic Effects.” In Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages (POPL’17), 486–499. Paris, France. Jan. 2017. doi:10.1145/3009837.3009872.

[11] Daan Leijen, and Anton Lorenzen. Tail Recursion Modulo Context – An Equational Approach. MSR-TR-2022-18. Microsoft Research. Jul. 2022.

[12] Daan Leijen, and Anton Lorenzen. “Tail Recursion Modulo Context: An Equational Approach.” Proc. ACM Program. Lang. 7 (POPL). Jan. 2023. doi:10.1145/3571233. See also [11].

[13] Anton Lorenzen, and Daan Leijen. Reference Counting with Frame Limited Reuse. MSR-TR-2021-30. Microsoft Research. Nov. 2022. https://​www.​microsoft.​com/​en-​us/​research/​publication/​reference-​counting-​with-​frame-​limited-​reuse-​extended-​version/​.

[14] Anton Lorenzen, Daan Leijen, and Wouter Swierstra. FP: Fully in-Place Functional Programming. MSR-TR-2023-19. Microsoft Research. May 2023. https://​www.​microsoft.​com/​en-​us/​research/​publication/​fp2-​fully-​in-​place-​functional-​programming.

[15] Anton Lorenzen, Daan Leijen, and Wouter Swierstra. “FP: Fully in-Place Functional Programming.” In Proceedings of the 28th ACM SIGPLAN International Conference on Functional Programming (ICFP’2023). ICFP’23. Seattle, WA, USA. Sep. 2023. See also [14].

[16] Prabhaker Mateti, and Ravi Manghirmalani. “Morris’ Tree Traversal Algorithm Reconsidered.” Science of Computer Programming 11 (1): 29–43. 1988. doi:10.1016/0167-6423(88)90063-9.

[17] Conor McBride. “The Derivative of a Regular Type Is Its Type of One-Hole Contexts.” 2001. http://​strictlypositive.​org/​diff.​pdf. (Extended Abstract).

[18] Joseph M. Morris. “Traversing Binary Trees Simply and Cheaply.” Information Processing Letters 9 (5): 197–200. 1979. doi:10.1016/0020-0190(79)90068-1.

[19] Chris Okasaki. “Red-Black Trees in a Functional Setting.” Journal of Functional Programming 9 (4). Cambridge University Press: 471–477. 1999. doi:10.1017/S0956796899003494.

[20] Chris Okasaki. Purely Functional Data Structures. Colombia University, New York. Jun. 1999.

[21] Gordon D. Plotkin, and Matija Pretnar. “Handlers of Algebraic Effects.” In 18th European Symposium on Programming Languages and Systems, 80–94. ESOP’09. York, UK. Mar. 2009. doi:10.1007/978-3-642-00590-9_7.

[22] Alex Reinking, Ningning Xie, Leonardo de Moura, and Daan Leijen. “Perceus: Garbage Free Reference Counting with Reuse.” In Proceedings of the 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation, 96–111. PLDI 2021. Virtual, Canada. 2021. doi:10.1145/3453483.3454032.

[23] Ningning Xie, Jonathan Brachthäuser, Phillip Schuster, Daniel Hillerström, and Daan Leijen. “Effect Handlers, Evidently.” In Proceedings of the 25th ACM SIGPLAN International Conference on Functional Programming (ICFP’2020). ICFP ’20. Jersey City, NJ. Aug. 2020.

[24] Ningning Xie, and Daan Leijen. Generized Evidence Passing for Effect Handlers – Efficient Compilation of Effect Handlers to C. MSR-TR-2021-5. Microsoft Research. Mar. 2021. https://​www.​microsoft.​com/​en-​us/​research/​publication/​generalized-​evidence-​passing-​for-​effect-​handlers/​.

[25] Ningning Xie, and Daan Leijen. “Generized Evidence Passing for Effect Handlers – Efficient Compilation of Effect Handlers to C.” In Proceedings of the 26th ACM SIGPLAN International Conference on Functional Programming (ICFP’2021). ICFP ’21. Virtual. Aug. 2021.