引用单元格、状态隔离

(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的论文）