Blog [blog]

Blog 1. MoonBit 实现树的先序遍历 [blog/iterator/preorder-traversal]

二叉树的定义

priv enum Tree[A] {
  Nil
  Node(A, Tree[A], Tree[A])
}

先序遍历一棵树

fn[A] Tree::preorder(self : Tree[A], f : (A) -> Unit) -> Unit {
  fn dfs(root) {
    match root {
      Nil => ()
      Node(x, left, right) => {
        f(x)
        dfs(left)
        dfs(right)
      }
    }
  }

  dfs(self)
}

我们把 Tree::preorder 改写为手动控制栈的过程 Tree::preorder_stack

fn[A] Tree::preorder_stack(self : Tree[A], f : (A) -> Unit) -> Unit {
  let stack = Array::new(capacity=4096)
  stack.push(self)
  while not(stack.is_empty()) {
    let root = stack.unsafe_pop()
    match root {
      Nil => ()
      Node(x, left, right) => {
        f(x)
        stack.push(right) // 先进后出, 先被压入后处理
        stack.push(left) // 先处理左节点
      }
    }
  }
}

下面的部分是用来测试系统栈版本和手动控制栈版本的一致性。

fn Tree::from_n(n : Int) -> Tree[Int] {
  let mut i = 0
  fn dfs() {
    if i < n {
      let x = i
      i += 1
      let res = Node(x, dfs(), dfs())
      res
    } else {
      Nil
    }
  }

  dfs()
}

fn test_preorder(root : Tree[Int]) -> Unit raise {
  let b1 = StringBuilder::new()
  let b2 = StringBuilder::new()
  root.preorder(fn(x) { b1.write_object(x) })
  root.preorder_stack(fn(x) { b2.write_object(x) })
  assert_eq(b1.to_string(), b2.to_string())
}

test "preorder/preorder_stack" {
  let t1 = Node(
    1,
    Node(2, Nil, Nil),
    Node(3, Node(4, Nil, Nil), Node(5, Nil, Nil)),
  )
  let mut sum = 0
  t1.preorder(fn(x) { sum += x })
  inspect(sum, content="15")
  let t2 = Tree::from_n(15)
  test_preorder(t2)
}

Blog 2. MoonBit 实现外部迭代器 [blog/iterator/external]

目前 MoonBit 社区有两个外部迭代器的实现, Yu-zh/iteratorFlammeShadow/iter

本文提供一个由浅入深的教程,来帮助读者学习外部迭代器。

2.1. 内部迭代器和外部迭代器 [blog/iterator/internal-vs-external]

  • 内部迭代器 迭代过程是不可分割的。
  • 外部迭代器 迭代过程是可分割的。

Moonbit 标准库的 Iter[A] 是内部迭代器, 没有办法把iter切分为(first : A?)(rest : Iter[A])

所以无法实现 fn uncons[A](xs : Iter[A]) -> (A, Iter[A])? 这样的接口。

也无法实现 fn next[A](self : Iter[A]) -> A? 这样的接口。

test "split internal iterator" {
  let xs = [1,2,3,4,5]
  let iter = xs.iter().drop(4)
  // 这里的 drop 只是修饰器,改变迭代的行为
  inspect!(xs.iter().last(), content="Some(5)")
  // 但是迭代过程还是 xs.iter()
  inspect!(iter.head(), content="Some(5)")
  // xs.iter().last() 仍然需要迭代5次
}

不可变外部迭代器可以很自然的实现uncons

可变外部迭代器可以实现next

2.2. 不可变外部迭代器和可变外部迭代器 [blog/iterator/immut-vs-mut]

不可变外部迭代器没有内部可变状态可以迭代多次。

可变外部迭代器只能迭代一次,虽然无法实现uncons, 但是迭代每个元素的过程仍是可分割的。

调用 next 方法后,可变外部迭代器的内部状态改变,变成剩余的迭代了。

2.3. 可变外部迭代器 [blog/iterator/mut-exiter]

可变外部迭代器,可以不断获取下一个元素的值,内部有一个可变的状态。

priv type ExIter[A] () -> A?

fn ExIter::next[A](self : ExIter[A]) -> A? {
  (self._)()
}
fn ExIter::from_array[A](xs : Array[A]) -> ExIter[A] {
  let mut i = 0 // i 是内部可变状态
  fn() {
    if i < xs.length() {
      let res = xs[i]
      i = i + 1
      Some(res)
    } else {
      None
    }
  }
}


test {
  let xs = [1, 2, 3, 4, 5]
  let iter = ExIter::from_array(xs)
  let mut sum = 0
  loop iter.next() {
    None => ()
    Some(x) => {
      sum += x
      continue iter.next()
    }
  }
  inspect!(sum, content="15")
}

ExIter::from_tree 是从 Tree::Tree::preorder_stack 改编而来, loop 变成 if 迭代过程可以切分,而不是一个整体。

比如 eacheachi 这样的内部迭代器的方法,只能一下子迭代全部元素

读者可以再一次看外部迭代器的性质 [blog/iterator/internal-vs-external]

  • 内部迭代器 迭代过程是不可分割的。
  • 外部迭代器 迭代过程是可分割的。

Moonbit 标准库的 Iter[A] 是内部迭代器, 没有办法把iter切分为(first : A?)(rest : Iter[A])

所以无法实现 fn uncons[A](xs : Iter[A]) -> (A, Iter[A])? 这样的接口。

也无法实现 fn next[A](self : Iter[A]) -> A? 这样的接口。

test "split internal iterator" {
  let xs = [1,2,3,4,5]
  let iter = xs.iter().drop(4)
  // 这里的 drop 只是修饰器,改变迭代的行为
  inspect!(xs.iter().last(), content="Some(5)")
  // 但是迭代过程还是 xs.iter()
  inspect!(iter.head(), content="Some(5)")
  // xs.iter().last() 仍然需要迭代5次
}

不可变外部迭代器可以很自然的实现uncons

可变外部迭代器可以实现next

fn ExIter::from_tree[A](root : Tree[A]) -> ExIter[A] {
  let stack = Array::new(capacity=4096) // stack 是内部可变状态
  stack.push(root)
  fn() {
    if not(stack.is_empty()) {
      let root = stack.unsafe_pop()
      match root {
        Nil => None
        Node(x, left, right) => {
          stack.push(right)
          stack.push(left)
          Some(x)
        }
      }
    } else {
      None
    }
  }
}

我们可以实现 zipWith 来同时迭代两个迭代器, 但是和不可变迭代器比,ExIter只能迭代一次,迭代后就使用完所有的元素。 这个和文件流的概念很相似。

fn ExIter::zipWith[A,B,C](self : ExIter[A], other : ExIter[B], f : (A,B) -> C) -> ExIter[C] {
  let xs = self
  let ys = other
  fn () {
    match (xs.next(),ys.next() ) {
      (Some(x),Some(y)) => {
        Some(f(x,y))
      }
      (_,_) => None
    }
  }
}

test "ExIter::zipWith" {
  let xs = ["apple", "orange", "watermetlon"]
  let ys = Tree::from_n(5)

  let xs = ExIter::from_array(xs)
  let ys = ExIter::from_tree(ys)

  let zs = xs.zipWith(ys,fn (x,y) { (x,y)})

  let b1 = StringBuilder::new()
  loop zs.next() {
    None => ()
    Some(x) => {
      b1.write_string("\{x},")
      continue zs.next()
    }
  }
  inspect!(b1, content=
    #|("apple", 0),("orange", 1),("watermetlon", 2),
  )
}

test "ExIter::from_tree" {
  let t2 = Tree::from_n(15)
  let iter = ExIter::from_tree(t2)
  let b1 = StringBuilder::new()
  loop iter.next() {
    None => ()
    Some(x) => {
      b1.write_string("\{x},")
      continue iter.next()
    }
  }
  inspect!(b1, content="0,1,2,3,4,5,6,7,8,9,10,11,12,13,14,")
  let b2 = StringBuilder::new()
  t2.preorder(fn(x) { b2.write_string("\{x},") })
  inspect!(b2, content="0,1,2,3,4,5,6,7,8,9,10,11,12,13,14,")
}

接下来我们来实现不可变外部迭代器

2.4. 不可变外部迭代器 [blog/iterator/immut-exiter]

不可变外部迭代器可以返回第一个元素和剩余的迭代过程

priv type ImmutExIter[A] () -> (A,ImmutExIter[A])?

fn ImmutExIter::uncons[A](self : ImmutExIter[A]) -> (A,ImmutExIter[A])? {
  (self._)()
}

这里从Array[A]构造不可变外部迭代器

fn ImmutExIter::from_array[A](xs : Array[A]) -> ImmutExIter[A] {
  fn aux(i) -> (A,ImmutExIter[A])? {
    if (i < xs.length()) {
      Some((xs[i],fn () { aux(i + 1) } ) )
    } else {
      None
    }
  }
  fn () {
    aux(0)
  }
}

测试一下迭代过程

test "ImmutExIter::from_array" {
  let xs = [1,2,3,4,5]
  let iter = ImmutExIter::from_array(xs)

  let buf = StringBuilder::new()

  loop iter.uncons() {
    None => ()
    Some((x,xs)) => {
      buf.write_object(x)
      continue xs.uncons()
    }
  }
  inspect!(buf, content="12345")
}

2.4.1. 实现树的不可变外部迭代器 [blog/iterator/immut-exiter-tree]

Blog 2.4.1.1. 前置知识 [blog/iterator/preorder-traversal]

二叉树的定义

priv enum Tree[A] {
  Nil
  Node(A, Tree[A], Tree[A])
}

先序遍历一棵树

fn[A] Tree::preorder(self : Tree[A], f : (A) -> Unit) -> Unit {
  fn dfs(root) {
    match root {
      Nil => ()
      Node(x, left, right) => {
        f(x)
        dfs(left)
        dfs(right)
      }
    }
  }

  dfs(self)
}

我们把 Tree::preorder 改写为手动控制栈的过程 Tree::preorder_stack

fn[A] Tree::preorder_stack(self : Tree[A], f : (A) -> Unit) -> Unit {
  let stack = Array::new(capacity=4096)
  stack.push(self)
  while not(stack.is_empty()) {
    let root = stack.unsafe_pop()
    match root {
      Nil => ()
      Node(x, left, right) => {
        f(x)
        stack.push(right) // 先进后出, 先被压入后处理
        stack.push(left) // 先处理左节点
      }
    }
  }
}

下面的部分是用来测试系统栈版本和手动控制栈版本的一致性。

fn Tree::from_n(n : Int) -> Tree[Int] {
  let mut i = 0
  fn dfs() {
    if i < n {
      let x = i
      i += 1
      let res = Node(x, dfs(), dfs())
      res
    } else {
      Nil
    }
  }

  dfs()
}

fn test_preorder(root : Tree[Int]) -> Unit raise {
  let b1 = StringBuilder::new()
  let b2 = StringBuilder::new()
  root.preorder(fn(x) { b1.write_object(x) })
  root.preorder_stack(fn(x) { b2.write_object(x) })
  assert_eq(b1.to_string(), b2.to_string())
}

test "preorder/preorder_stack" {
  let t1 = Node(
    1,
    Node(2, Nil, Nil),
    Node(3, Node(4, Nil, Nil), Node(5, Nil, Nil)),
  )
  let mut sum = 0
  t1.preorder(fn(x) { sum += x })
  inspect(sum, content="15")
  let t2 = Tree::from_n(15)
  test_preorder(t2)
}

2.4.1.2. 正文 [blog/iterator/immut-exiter-tree-content]

这里使用不可变单向链表作为栈,每次返回一个 ImmutExIter[A] 需要保存整个迭代上下文,

  • 可变外部迭代器并不会保存,只能运行一次

  • 不可变外部迭代器可以运行多次,但是需要额外保存迭代上下文

typealias Stack[A] = @immut/list.T[A]

fn ImmutExIter::from_tree[A](root : Tree[A]) -> ImmutExIter[A] {

  fn aux(stack : Stack[_]) -> (A,ImmutExIter[A])? {
    match stack {
      Nil => None
      Cons(root,rest_stack) => { // pop root from stack
        match root {
          Nil => None
          Node(x,left,right) => {
            let stack = Stack::Cons(left,Stack::Cons(right,rest_stack))
            // push right into stack
            // push left into stack
            Some((x,fn () { aux(stack)}))
          }
        }
      }
    }
  }
  fn () {
    aux(@immut/list.singleton(root))
  }
}

这里测试一下,不可变外部迭代器和 preorder 的一致性

test "ImmutExIter::from_tree" {
  let t2 = Tree::from_n(15)
  let iter = ImmutExIter::from_tree(t2)
  let b1 = StringBuilder::new()
  loop iter.uncons() {
    None => ()
    Some((x,rest)) => {
      b1.write_string("\{x},")
      continue rest.uncons()
    }
  }
  inspect!(b1, content="0,1,2,3,4,5,6,7,8,9,10,11,12,13,14,")
  let b2 = StringBuilder::new()
  t2.preorder(fn(x) { b2.write_string("\{x},") })
  inspect!(b2, content="0,1,2,3,4,5,6,7,8,9,10,11,12,13,14,")
}

接下来我们来实现 zipWith,这里和普通的List[A]zipWith 别无二致

fn ImmutExIter::zipWith[A,B,C](self : ImmutExIter[A], other : ImmutExIter[B], f : (A,B) -> C) -> ImmutExIter[C] {
  let xs = self
  let ys = other

  match (xs.uncons(),ys.uncons()) {
    (Some((x,xs)),Some((y,ys))) => {
      fn () { Some((f(x,y),  ImmutExIter::zipWith(xs,ys,f)))}
    }
    (_,_) => {
      fn () { None }
    }
  }
}


test {
  let xs = ["apple", "orange", "watermetlon"]
  let ys = Tree::from_n(5)

  let xs = ImmutExIter::from_array(xs)
  let ys = ImmutExIter::from_tree(ys)

  let zs = xs.zipWith(ys,fn (x,y) { (x,y)})

  let b1 = StringBuilder::new()
  loop zs.uncons() {
    None => ()
    Some((x,rest)) => {
      b1.write_string("\{x},")
      continue rest.uncons()
    }
  }
  inspect!(b1, content=
    #|("apple", 0),("orange", 1),("watermetlon", 2),
  )
}

2.5. 参考资料 [blog/iterator/reference]

Why does the callback for Iter::new() need to return IterResult?

external iterator

internal iterator

zip n^2 complexity

Proposal: peekable iterator and pattern matching on iterators

Blog 3. MoonBit 实现内部迭代器 [blog/iterator/internal]

本文实现的内部迭代器参考 OCaml iter

priv type InIter[A] ((A) -> Unit) -> Unit

fn InIter::run[A](self : InIter[A], f : (A) -> Unit) -> Unit {
  (self._)(f)
}

这里的 InIter::from_array 相当于 OCaml 的柯里化。

fn InIter::from_array[A](xs : Array[A]) -> InIter[A] {
  fn(k) { xs.each(k) }
}

with_index 是装饰器,装饰 iter 默认的行为。

fn InIter::with_index[A](self : InIter[A]) -> InIter[(Int, A)] {
  let mut i = 0
  fn(k) {
    self.run(fn(x) {
      k((i, x))
      i += 1
    })
  }
}
impl[A : Show] Show for InIter[A] with output(self, logger) {
  logger.write_string("[")
  self.run(fn(x) {
    logger.write_object(x)
    logger.write_string(",")
  })
  logger.write_string("]")
}

test {
  let xs = ["apple", "orange", "strawberry"]
  let iter = InIter::from_array(xs).with_index()

  inspect!(iter.to_string(), content=#|[(0, "apple"),(1, "orange"),(2, "strawberry"),]
  )
}

为了在迭代过程中停止循环,MoonBit 引入了 IterResult.

yield : (A) -> IterResult 这个回调函数可以控制循环是停止还是继续。

type InIter[A] ((A) -> Unit) -> Unit
type Iter[A] ((A) -> IterResult) -> IterResult

我们比较 Iter[A]InIter[A] 的定义,

Unit 替换成 IterResult 之后,就和 MoonBit 内建的内部迭代器定义一样了 InIter[A] 返回 Unit 和 回调函数返回 Unit, 相当于一直返回 IterResult::IterContinue

MoonBit 标准库中的 Iter::take, Iter::drop, Iter::flat_map … 这些方法都是装饰器,用来修饰原先 iter 的行为。

我们来看 coreIter::take 的实现, 这个 Iter::take 可以用来解释, yield_ 如何控制循环的状态。

// ref: https://github.com/moonbitlang/core/blob/main/builtin/iter.mbt

pub fn Iter::take[T](self : Iter[T], n : Int) -> Iter[T] {
  // [..take(10,seq), next] would continue
  // even if seq has less than 10 elements
  // but `for x in [..take(10,seq), next ] { break }` would stop
  //
  fn(yield_) {
    let mut i = 0
    let mut r = IterContinue
    self.just_run(fn {
      a =>
        if i < n {
          if yield_(a) == IterContinue {
            // yield_ 这个回调函数,有循环的控制权
            i = i + 1
            IterContinue
          } else {
            r = IterEnd
            IterEnd // 这里 yield 让整个循环退出了
          }
        } else {
          IterEnd // i < n, 停止循环
        }
    })
    r
  }
}

Iter::drop 的实现,可以解释为什么内部迭代器是不可分割的。

// ref: https://github.com/moonbitlang/core/blob/main/builtin/iter.mbt


pub fn Iter::drop[T](self : Iter[T], n : Int) -> Iter[T] {
  fn(yield_) {
    let mut i = 0
    self.run(fn(a) {
      if i < n {
        i = i + 1
        IterContinue
        // 这里跳过 n 个元素, 但是这个 Iter::drop 只是装饰器,
        // 让 self 这个迭代器,不对前 n 个元素,调用 yield_ 而已
        // 即使drop 之后,i 仍然会递增 n
      } else {
        yield_(a)
      }
    })
  }
}
test "split internal iterator" {
  let xs = [1,2,3,4,5]
  let iter = xs.iter().drop(4)
  // 这里的 drop 只是修饰器,改变迭代的行为
  inspect!(xs.iter().last(), content="Some(5)")
  // 但是迭代过程还是 xs.iter()
  inspect!(iter.head(), content="Some(5)")
  // xs.iter().last() 仍然需要迭代 5 次
  // 上面的源码解析,解释了为什么仍然需要迭代 5 次

}

Iter::drop 之后,还需要递增内部状态的 i, 所以说内部迭代器是不可分割的

3.1. 内部迭代器和外部迭代器 [blog/iterator/internal-vs-external]

  • 内部迭代器 迭代过程是不可分割的。
  • 外部迭代器 迭代过程是可分割的。

Moonbit 标准库的 Iter[A] 是内部迭代器, 没有办法把iter切分为(first : A?)(rest : Iter[A])

所以无法实现 fn uncons[A](xs : Iter[A]) -> (A, Iter[A])? 这样的接口。

也无法实现 fn next[A](self : Iter[A]) -> A? 这样的接口。

test "split internal iterator" {
  let xs = [1,2,3,4,5]
  let iter = xs.iter().drop(4)
  // 这里的 drop 只是修饰器,改变迭代的行为
  inspect!(xs.iter().last(), content="Some(5)")
  // 但是迭代过程还是 xs.iter()
  inspect!(iter.head(), content="Some(5)")
  // xs.iter().last() 仍然需要迭代5次
}

不可变外部迭代器可以很自然的实现uncons

可变外部迭代器可以实现next

Blog 4. Derive Iteration from Recursion [blog/defunctionalize]

递归和迭代是编程中两种基础的重复执行模式,它们在实现方式上有所不同,但计算能力上是等价的。 递归通过函数调用自身来分解问题,通常表达简洁,符合数学 (结构) 归纳法的思维模式;而迭代则借助循环结构 (如 forwhile) 逐步更新状态,直接控制计算流程。然揆诸实现,则各具长短:

  • 递归代码短小清晰,适合解决分治问题 (如树的遍历、动态规划),但可能导致栈溢出 (stack overflow) 和较高的函数调用开销,尤其是深度递归时效率降低。
  • 迭代虽然执行更快,节省栈空间,但需要开发者显式管理状态 (如循环变量、临时存储、甚至需要手动维护一个栈),逻辑可能不如递归直观。

既然两者各有优劣,是否存在一种通用方法,能够自动或半自动地将递归逻辑转换为等价的迭代实现?答案是肯定的,而这正是本文的核心概念——去函数化 (defunctionalization),即将递归的函数调用关系转换为显式的栈管理结构,从而在保持正确性的同时提升运行效率。

4.1. Defunctionalization: A Taste on Filter DSL [blog/defunctionalize/filter]

让我们以循序渐进的方式展开论述。 作为切入点,不妨考察一个具有典型性的基础案例:设想需要实现 filter 函数,该函数接收列表与谓词函数作为输入,返回满足谓词条件的所有元素构成的新列表。 采用递归策略可达成如下实现:

fn[T] filter(xs : List[T], pred : (T) -> Bool) -> List[T] {
  match xs {
    Nil => Nil
    Cons(x, xs) if pred(x) => Cons(x, filter(xs, pred))
    Cons(_, xs) => filter(xs, pred)
  }
}

此处 pred 作为高阶函数的特性引发了一个本质性问题:在底层编译场景中 (如将 MoonBit 编译至 C 语言时),函数无法以常规数据结构的形式进行存储与传递。换言之,在目标语言层面,一等函数的直接表示存在根本性限制。

最直观的解决思路莫过于穷举法——将所有可能用到的谓词函数进行枚举编码。以下示例展示了针对整数的几种基本谓词:

enum Filter {
  IsEven
  IsOdd
  IsPositive
  IsNegative
}

fn run(self : Filter, data : Int) -> Bool {
  match self {
    IsEven => data % 2 == 0
    IsOdd => data % 2 != 0
    IsPositive => data > 0
    IsNegative => data < 0
  }
}

借此定义,可重构出经过去函数化处理的过滤函数:

fn filter_defunct(xs : List[Int], pred : Filter) -> List[Int] {
  match xs {
    Nil => Nil
    Cons(x, xs) if pred.run(x) => Cons(x, filter_defunct(xs, pred))
    Cons(_, xs) => filter_defunct(xs, pred)
  }
}

然而此方案存在明显局限性。 诚然,高阶谓词函数的集合实为不可数无穷集,这使得完备枚举在理论上即不可行。 但通过代数数据类型的参数化特性,我们可获得某种程度上的扩展能力。 例如将 IsNegative 推广为带参数的 IsLessThan

enum FilterExtend {
  //...
  IsLessThan(Int)
}

fn run_extend(self : FilterExtend, data : Int) -> Bool {
  match self {
    IsLessThan(n) => data < n
    //...
  }
}

更富启发性的是引入复合逻辑结构。 通过增加 And 等逻辑连接词,可实现谓词函数的组合运算:

enum FilterExtendCompose {
  //...
  And(FilterExtend, FilterExtend)
}

fn run_extend_compose(self : FilterExtendCompose, data : Int) -> Bool {
  match self {
    And(f1, f2) => f1.run_extend(data) && f2.run_extend(data)
    //...
  }
}

经过这般层层抽象,我们所构建的 Filter 类型本质上已演变为一种领域特定语言 (Domain-Specific Language)。 建议感兴趣的读者可进一步探索其 Parser 与 Pretty Printer 的实现路径,以完善该 DSL 的序列化能力。

但必须指出,这种基于代数数据类型的方案存在固有的封闭性缺陷——每新增一个枚举成员都需要修改所有相关的模式匹配逻辑 (本案例中的 run 函数)。 这与高阶函数与生俱来的开放性形成鲜明对比:后者允许在不修改现有代码的前提下自由扩展新函数。

4.2. Traverse a Tree [blog/defunctionalize/tree]

通过前文的讨论,读者应对去函数化的核心思想建立了基本认知。 本节将运用该技术解决更具挑战性的问题——二叉树遍历优化。首先给出二叉树的规范定义:

enum Tree[T] {
  Leaf(T)
  Node(T, Tree[T], Tree[T])
}

考虑基础的前序遍历实现:

fn[T] pre_order(tree : Tree[T], f : (T) -> Unit) -> Unit {
  match tree {
    Leaf(x) => f(x)
    Node(x, left, right) => {
      f(x)
      pre_order(left, f)
      pre_order(right, f)
    }
  }
}

在该函数的设计实现中,我们采用递归算法对树形数据结构进行系统性遍历, 这种方法虽能确保每个节点都受到函数 f 的精确, 且严格遵循前序遍历(pre-order traversal)的既定顺序,但其递归范式存在显著的效率瓶颈。 具体而言,由于该递归过程并非尾递归(tail recursion)的优化形态, 导致现代编译器的尾调用优化(TCO)机制无法将其自动转换为等价的迭代形式, 这种特性必然造成调用栈的持续累积,进而影响程序的执行效能。 有鉴于此,我们亟需运用前文阐述的「去函数化」(defunctionalization)这一程序变换技术来突破此局限。

4.3. Continuation-Passing Style Transformation [blog/defunctionalize/cps]

面对这个看似棘手的控制流问题,我们稍作停顿。 考虑引入“延续” (continuation) 这一关键概念——其本质是对程序剩余计算过程的抽象建模。 具体而言,对于表达式 $1 + 2 * 3 + 4$ 的求值过程:当计算 $2 * 3$ 时,其延续即为带洞表达式 $1 + \square + 4$ 所表征的后续计算。 形式化地,我们可以将延续定义为高阶函数 $\lambda x. 1 + x + 4$, 该函数接收当前计算结果并执行剩余计算过程。

延续传递形式 (Continuation-Passing Style,CPS) 的核心范式在于: 所有函数均不直接返回结果,而是通过将中间值传递给延续函数来实现控制流转移。 以树的前序遍历为例,当第一个 pre_order(left, f) 调用执行时, 其延续正是 fn (_) { pre_order(right, f) } 表征的右子树遍历过程。 我们通过扩展函数签名引入延续参数,重构后的实现显式地将计算结果注入到延续中:

fn[T] pre_order_cps(self : Tree[T], f : (T) -> Unit) -> Unit {
  fn go(t, g) {
    match (t, g) {
      (Leaf(x), k) => k(f(x))
      (Node(x, left, right), k) => {
        f(x)
        go(left, _ => go(right, k))
      }
    }
  }

  go(self, x => x)
}

通过严格的 CPS 变换,程序的控制流获得了显式的过程化表征。 基于此,我们可进一步实施延续的去函数化,即将高阶函数表示转化为数据结构表示。 观察到延续包含两种形态:递归处理函数 go(tree, cont) 与恒等函数 fn { x => x },我们将其编码为代数数据类型:

enum TreeCont[T] {
  Return
  Next(Tree[T], TreeCont[T])
}

重构后的实现将函数调用转化为对延续结构的模式匹配,引入辅助函数 run_cont 实现之:

fn[T] pre_order_cps_defunct(self : Tree[T], f : (T) -> Unit) -> Unit {
  letrec run_cont = fn(k) {
    match k {
      Next(tree, k) => go(tree, k)
      Return => ()
    }
  }
  and go = fn(t, g) {
    match (t, g) {
      (Leaf(x), k) => {
        f(x)
        run_cont(k)
      }
      (Node(x, left, right), k) => {
        f(x)
        go(left, Next(right, k))
      }
    }
  }

  go(self, Return)
}

为实现彻底的命令式转换,我们先将尾递归形式改写为显式循环结构。 通过 MoonBit 的 loop 语法,控制流的跳转关系得到直观呈现:

fn[T] pre_order_cps_defunct_loop(self : Tree[T], f : (T) -> Unit) -> Unit {
  loop (self, Return) {
    (Leaf(x), k) => {
      f(x)
      match k {
        Next(tree, k) => continue (tree, k)
        Return => ()
      }
    }
    (Node(x, left, right), k) => {
      f(x)
      continue (left, Next(right, k))
    }
  }
}

此时,向传统循环的转换已水到渠成。通过引入可变状态变量,我们获得完全命令式的实现:

fn[T] pre_order_loop(self : Tree[T], f : (T) -> Unit) -> Unit {
  let mut k = Return
  let mut t = self
  while true {
    match t {
      Leaf(x) => {
        f(x)
        match k {
          Next(tree, next) => {
            k = next
            t = tree
          }
          Return => break
        }
      }
      Node(x, left, right) => {
        f(x)
        k = Next(right, k)
        t = left
      }
    }
  }
}

经仔细分析可见,延续结构 TreeCont 实质上模拟了栈式存储结构:Next(right, k) 对应入栈操作, 而模式匹配 Next(tree, next) 则对应出栈操作。 这一洞察使我们能直接给出基于显式栈的实现:

fn[T] pre_order_loop_stack(self : Tree[T], f : (T) -> Unit) -> Unit {
  let k = []
  let mut t = self
  while true {
    match t {
      Leaf(x) => {
        f(x)
        match k.pop() {
          Some(tree) => t = tree
          None => break
        }
      }
      Node(x, left, right) => {
        f(x)
        k.push(right)
        t = left
      }
    }
  }
}

这项系统性的转换工程清晰展现了从高阶函数到数据结构, 从递归到迭代,从隐式控制流到显式状态管理的完整范式迁移路径。

4.4. Review and Summary [blog/defunctionalize/review]

$$ \text{CPS} \to \text{Defunctionalization} \to \text{Inlining} \to \text{Tail Call Elimination} $$

让我们对这一系列精妙的程序转换过程进行系统性的理论总结。 整个改造工程可分解为四个阶段:

  • 第 Ⅰ 阶段:控制流显式化 (CPS 变换): 通过引入延续传递形式,我们将原本隐含在语言运行时中的执行上下文显式提升为可操作的一等公民。 这一关键转换使递归调用点的控制流转移过程浮出水面,为后续的机械化改造奠定了基础。

  • 第 Ⅱ 阶段:去函数化: 基于 Reynolds 提出的去函数化理论, 我们将高阶的延续函数降维为具体的代数数据类型 TreeCont。 这一转换揭示了延续本质上是对调用栈的结构化建模, 其中 Next 构造子对应栈帧压入操作,对其模式匹配则是出栈, Return 则表征栈空状态。 通过此步骤,动态的函数调用关系被静态的数据结构所替代。

  • 第 Ⅲ 阶段:内联与尾递归化: 通过将辅助函数 run_cont 内联到主处理流程, 我们消除了函数间的相互递归调用,形成严格的尾递归形式。 此时程序的执行流已呈现近线性结构, 每个函数调用点的上下文关系完全由传入的延续对象所决定, 这为尾调用优化提供了理想的先决条件。

  • 第 Ⅳ 阶段:迭代式转换: 最终阶段将尾递归结构转换为基于可变状态和循环命令的迭代实现。 这一转换过程严格对应现代编译器对尾调用的优化策略: 将递归调用点改写为带状态更新的循环跳转,将延续对象转换为显式的栈数据结构。 值得注意的是,从 TreeCont 到命令式栈的转换验证了理论计算机科学中“程序即数据”的观点。

“去函数化”的确是精妙的程序转换技术, 若读者在看完本文仍意犹未尽, 希望能够深入了解其背后的理论基础和更多实现细节, 可以参考以下资源:

Blog 5. The Abstraction of Scientific Computing in LunaFlow [blog/lunaflow]

LunaFlow 是一个基于 MoonBit 的科学计算框架, 旨在为用户提供高效、灵活的计算能力。 该框架在设计理念上有许多独到之处, 尤其体现在数据抽象与泛型算法的实现。 然而遗憾的是,未有技术文档详尽阐释这些核心设计背后的理论依据与实践权衡。

作为 LunaFlow 的架构者之一,笔者撰写本文的目的在于: 其一,系统性地剖析 LunaFlow 的顶层设计哲学,揭示其主要设计原则与实现细节。 其二,通过具体用例的实证分析,展示如何利用该框架构建高效的数值计算流程。 希望读者不仅能够领悟到此种抽象设计在工程实践中的精妙之处, 还能将这种范式迁移至自身的项目开发之中,提升代码的表达力与泛用性。

5.1. Levels of Abstraction [blog/lunaflow/layers]

LunaFlow 采用分层模块化架构, 通过严格的抽象层级将系统组件进行逻辑划分。 其架构可组织为树形结构: 位于根基位置的是 Luna-Generic 核心模块, 该模块借助 MoonBit 的 trait 系统实现了对基础数学结构的代码描述。 在此基础上,作为首要叶子节点的 Luna-Utils 模块承担了通用工具函数的实现, 而诸如 ComplexQuaternion 等基础数据结构包则构成了更为细化的叶节点。

Modules

高阶数学工具包被置于抽象体系的更上层级, 当前主力模块包括 Calculus NumericalLinear AlgebraPolynomial 等, 这些模块通过显式的依赖关系调用底层服务,展现出清晰的依赖倒置原则(Dependence Inversion Principle)。 尤为精妙的是,LunaFlow 的架构设计允许用户在 Luna-Generic 的抽象框架下扩展自定义数据结构, 这些用户定义类型可无缝融入现有类型系统,并与上层模块达成双向互操作。 自然地,这引出一个关键性问题:如何构建具有数学严谨性的通用数据抽象?

5.2. Mathematical Structures In Luna-Generic [blog/lunaflow/generic]

程序设计语言中抽象机制的一个根本目标, 在于对行为模式进行精确的形式化描述并实现有效的代码复用。 在此语境下,代数结构因其严谨的数学内涵, 恰好为这类抽象提供了坚实的理论基础。 MoonBit 语言设计的 trait 系统,通过精妙的类型约束与组合机制, 构建了一套完整的代数结构表达体系。 该系统允许开发者以类型安全的方式,将半群(Semigroup)到半环(Semiring),乃至更复杂的环(Ring)等代数结构进行层级化建模。

5.2.1. Semiring [blog/lunaflow/semiring]

在抽象代数中,一个半环(Semiring)是一个集合 $R$, 配备了两个二元运算:加法 $+$ 和乘法 $*$,且满足下面的性质:

  • $(R, +, 0)$ 是一个交换群(Commutative Group),即满足结合律、交换律和存在单位元。
  • $(R, *, 1)$ 是一个幺半群(Monoid),即满足结合律和存在单位元。

除此之外,还满足下面两条性质:

  • 分配律:$a * (b + c) = a * b + a * c$ 和 $(a + b) * c = a * c + b * c$。
  • $0 * a = 0$ 和 $a * 0 = 0$,其中 $0$ 是加法的单位元。

从数学定义出发,半环结构实际上包含两个相互关联的代数组成部分: 其一是具有交换性质的加法幺半群, 其二是乘法幺半群。 在 MoonBit 的类型系统中, 这两个基本结构分别对应着 trait AddMonoidMulMonoid 的实现 (其中 AddMonoid 隐含地要求加法运算满足交换律这一数学性质):

trait AddMonoid: Add + Zero {}
trait MulMonoid: Mul + One {}
trait Semiring: AddMonoid + MulMonoid {}

需要特别说明的是, 当前 MoonBit 的 trait 机制尚无法在类型层面强制保证代数公理的成立 —— 包括但不限于结合律、分配律等基本性质的正确性。 这种限制本质上源于类型系统的表达能力边界: 若要严格验证代数公理,必须借助依赖类型等高级类型理论工具, 而这与 MoonBit 作为工业级语言的设计目标有所偏离。 对这一话题感兴趣的读者,可进一步研读 LeanCoq 等定理证明器的相关文献, 这些语言可通过精密的类型机制表达更为复杂的数学约束。 下面是一个在 Lean 中定义半群的示例:

/-- A semigroup is a type with an associative `(*)`. -/
class Semigroup (G : Type u) extends Mul G where
  /-- Multiplication is associative -/
  protected mul_assoc : ∀ a b c : G, a * b * c = a * (b * c)

此类抽象机制的核心价值在于实现真正基于代数性质的通用编程范式。 譬如,撰写矩阵乘法算法时,开发者只需约束类型参数满足 Semiring 特征, 即可安全地调用加法与乘法运算。无论具体实例化为整数环、 布尔半环还是其他自定义代数结构, 编译器都能在类型检查阶段确保所有运算的合法性与完备性。 这种设计在保障类型安全的同时,达到了代码复用的最大化。 如 Luna-Poly 的实现中,多项式结构被 A 参数化, 并通过 Semiring 特征约束其元素类型, 任意实现了 Semiring 特征的类型都可以作为多项式的系数类型, 从而可以调用多项式的加法与乘法运算:

impl[A : Eq + Semiring] Mul for Polynomial[A] with op_mul(xs, ys)
impl[A : Eq + Semiring] Add for Polynomial[A] with op_add(xs, ys)

从软件工程的角度审视,代数结构的层级化抽象完美体现了关注点分离(Separation of Concerns)的设计哲学。 数学上,群(Group)在幺半群基础上引入逆元概念, 而环(Ring)又要求加法构成交换群。 这些递进关系在 MoonBit 中表现为 trait 的组合: 每个新特征只需声明其扩展的代数运算,无需重复定义底层运算。这种设计不仅消除了代码冗余, 更重要的是建立了数学理论与程序实现之间的严格对应, 使得抽象层次之间的关系如抽丝剥茧般清晰可见。

5.3. Validating Constraints on Algebraic Structures [blog/lunaflow/testing]

对于代数结构公理的验证,我们并非束手无策。 虽然从完备性角度无法穷尽所有可能的验证场景, 但通过精心构建的测试用例集合, 我们能够对公理在特定实例上的有效性进行系统化验证。 借助 QuickCheck 这一强大的属性测试框架, 我们得以实现从抽象代数公理转化为可执行规范(Executable Specifications)的范式转变。这一过程中,代数结构的基本公理恰成为指导属性编写的理论基石,配合自动生成的测试数据,能够对类型实现进行统计学上的验证。

5.3.1. How QuickCheck Works? [blog/lunaflow/quickcheck]

简单来说,QuickCheck 的本质是通过随机采样对程序行为进行统计验证。 用户可以制定待测试程序具有的属性, 通常可以视为是 (T) -> Bool 的函数, 其中返回值 Bool 表示程序是否满足该属性。 随后通过生成器(Generator)来创建随机数据, 并将其传递给属性函数,并验证返回值是否为 true。 (默认采用的是类型导向采样:即通过 Arbitrary trait 将类型与数据生成规则绑定) 若属性函数在所有随机数据上均返回 true, 则可以认为该属性成立。 否则,可认为该属性不成立,并且找到了一个反例, QuickCheck 接着尝试缩小反例的大小, 以便更好地理解问题的根源。

简单来说,QuickCheck 是一种基于随机采样对程序行为进行统计验证的测试框架。其核心工作机制可解构为以下几个的骤:

  1. 测试者形式化地定义待验证程序的属性,通常表示为一个谓词函数,其类型签名为 (T) -> Bool。其中,布尔返回值直观地表征当前输入数据是否满足预期性质。
  2. 框架通过预定义的生成器(Generator)构造符合类型约束的随机测试数据。这里涉及一个关键的技术实现细节:默认情况下,系统采用类型导向的采样策略,即通过 Arbitrary 这个 trait 将具体数据类型与其对应的随机生成规则进行约束绑定,从而实现类型安全的测试用例自动化生成。
  3. 当测试引擎获得随机生成的测试数据后,会将其作为参数传递给前述属性函数进行求值验证。倘若所有随机样本都能使属性函数返回 true,则表明属性成立。反之,若发现存在反例,框架不仅会精准定位违规用例,还会使用收缩算法,通过逐步缩小反例的大小,最终呈现最精简的反例形态,以提高诊断问题的效率与精确度。

在 QuickCheck 测试系统中,属性构造居于核心地位。 对于代数结构而言,其公理体系天然具备可检验性特质: 我们可以通过将数学公理直接映射为测试属性,在具体实现中建立严格的验证机制。 以 Linear-Algebra 代码库中的典型案例进行说明: 当定义表示向量的 Vector[T] 类型及其加法运算 op_add 时, 作为向量空间的基本要求,加法运算必须严格满足交换律与结合律。 具体而言,对于任意选择的向量 $\vec{u}, \vec{v}, \vec{w} \in V$, 必须满足以下数学约束:

$$ \begin{align*} \vec{u} + \vec{v} &= \vec{v} + \vec{u} \quad \text{(交换律)} \\ \vec{u} + (\vec{v} + \vec{w}) &= (\vec{u} + \vec{v}) + \vec{w} \quad \text{(结合律)} \end{align*} $$

在实现层面,我们可将其转化为如下测试验证(注:此处假定 Vector 类型已正确实现 Arbitrary trait):

test "algebraic laws" {
    fn prop(a : Vector[Int], b) { a + b == b + a }
    fn prop(a : Vector[Int], b, c) { a + (b + c) == (a + b) + c }
    quick_check_fn!(fn {
        ((a : Vector[Int]), (b : Vector[Int])) => {
        guard a.length() == b.length() else { true }
        prop(a, b)
        }
    })
    quick_check_fn!(fn {
        ((a : Vector[Int]), (b : Vector[Int]), (c : Vector[Int])) => {
        guard a.length() == b.length() && b.length() == c.length() else { true }
        prop(a, b, c)
        }
    })
}

这种将数学公理机械性地转化为可执行验证机制的范式, 使得 LunaFlow 得以利用数学上的公理体系, 为实现的正确性提供强有力的测试保障。

5.4. Real-world Usage of LunaFlow (Polynomial) [blog/lunaflow/instances]

5.5. Future of LunaFlow [blog/lunaflow/future]

Blog 6. You could have invented Fenwick trees [blog/fenwick]

本文译自 Brent Yorgey 的 Functional Pearl 论文 You could have invented Fenwick trees,并做了一些解释补充、错误修正,以及将原文的 Haskell 代码都翻译到了 MoonBit 代码。

芬威克树(Fenwick trees),亦称二叉索引树(binary indexed trees),是一种精巧的数据结构,旨在解决这样一个问题:如何在维护一个数值序列的同时,支持在亚线性时间内完成更新操作与区间查询。其实现简洁高效,然亦颇为费解,多由一些针对索引的、不甚直观的位运算构成。本文将从线段树(segment trees)入手——这是一种更为直接、易于验证的纯函数式解法——并运用等式推理,阐释芬威克树的实现乃是一种优化变体,此过程将借助一个 MoonBit 嵌入式领域特定语言(EDSL)来处理无限二进制补码数。

Blog 7. 用 MoonBit 实现 LRU 缓存算法 [blog/lrualgorithm]

7.1. LRU 缓存简介 [blog/lrualgorithm/whats]

大家好!今天我想和大家分享如何用 MoonBit 语言实现一个 LRU(Least Recently Used,最近最少使用)缓存算法。无论你是刚接触 MoonBit,还是想了解 LRU 算法的实现细节,这篇文章都会带你深入了解这个经典而实用的算法。

什么是 LRU 缓存?

LRU 缓存是一种常见的缓存淘汰策略,它基于一个简单的假设:最近访问过的数据在不久的将来很可能再次被访问。因此,当缓存空间不足需要淘汰数据时,应该优先淘汰最长时间未被访问的数据。

一个日常生活的例子

想象你的书桌上只能放 5 本书。每次你需要一本新书,但书桌已满时,你会把哪本书放回书架?最合理的选择是把最久没看的那本书放回去。这就是 LRU 策略的直观体现。

技术应用场景

LRU 缓存在计算机系统中有广泛的应用:

  • 操作系统的页面置换:当物理内存不足时,系统需要决定将哪些页面从内存换出到磁盘
  • 数据库的缓存管理:数据库会在内存中缓存经常访问的数据块,提高读写性能
  • Web 服务器的缓存:缓存热门的网页、图片等资源,减少服务器负载
  • 浏览器的缓存机制:存储最近浏览的网页,加快重复访问的速度
  • CDN 内容分发网络:根据访问频率调整内容缓存策略

LRU 缓存的实际例子

假设我们有一个容量为 3 的 LRU 缓存,初始为空。现在执行以下操作:

  1. put(1, "一") → 缓存现状:[(1, “一”)]
  2. put(2, "二") → 缓存现状:[(2, “二”), (1, “一”)]
  3. put(3, "三") → 缓存现状:[(3, “三”), (2, “二”), (1, “一”)]
  4. get(1) → 返回 “一”,缓存现状:[(1, “一”), (3, “三”), (2, “二”)] (注意 1 被移到了最前面)
  5. put(4, "四") → 缓存已满,淘汰最久未使用的 (2, “二”),缓存现状:[(4, “四”), (1, “一”), (3, “三”)]
  6. get(2) → 返回 None (不存在)

通过这个例子,我们可以看到 LRU 缓存如何维护“最近使用“的顺序,以及如何在缓存满时进行淘汰。

LRU 缓存的核心操作

一个标准的 LRU 缓存需要支持以下两个核心操作:

  1. get(key): 获取缓存中键对应的值

    • 如果键存在,返回对应的值,并将该键值对移动到“最近使用“的位置
    • 如果键不存在,返回特殊值(如 None)
  2. put(key, value): 向缓存中插入或更新键值对

    • 如果键已存在,更新值,并将该键值对移动到“最近使用“的位置
    • 如果键不存在,创建新的键值对,放到“最近使用“的位置
    • 如果缓存已满,先删除“最久未使用“的键值对,再添加新的键值对

这两个操作的时间复杂度都应该是 O(1),这就需要我们精心设计数据结构。

为什么需要特殊的数据结构?

实现一个高效的 LRU 缓存面临两个主要挑战:

  1. 快速查找:我们需要 O(1) 时间确定一个键是否存在于缓存中
  2. 顺序维护:我们需要跟踪所有缓存项的使用顺序,以便知道哪个是“最久未使用“的

如果只用数组,查找需要 O(n) 时间;如果只用哈希表,无法跟踪使用顺序。因此,我们需要结合两种数据结构。

实现思路:哈希表 + 双向链表

LRU 缓存的经典实现方式是结合使用:

  • 哈希表:提供 O(1) 的查找能力,键映射到链表中的节点
  • 双向链表:维护数据的访问顺序,最近使用的在链表头,最久未使用的在链表尾

这种组合让我们能够同时满足快速查找和顺序维护的需求。

接下来,我们将用 MoonBit 语言一步步实现这个数据结构,从基础的节点定义,到完整的 LRU 缓存功能。

7.2. 定义基础数据结构 [blog/lrualgorithm/define]

在实现 LRU 缓存之前,我们首先需要定义一些基础的数据结构。正如前面所说,我们需要结合哈希表和双向链表来实现高效的 LRU 缓存。

节点结构

我们先定义双向链表的节点结构。每个节点需要存储键值对,并且包含指向前一个和后一个节点的引用:

// 定义Node结构体,用于双向链表
struct Node[K, V] {
  key : K
  mut value : V
  mut pre : Node[K, V]?  // 前驱节点
  mut next : Node[K, V]? // 后继节点
}

// Node构造函数
fn new_node[K, V](k : K, v : V) -> Node[K, V] {
  { key: k, value: v, pre: None, next: None }
}

在这个节点结构中有几个有趣的 MoonBit 特性值得我们关注:

  • 泛型参数 [K, V]:这使得我们的 LRU 缓存可以适用于任何类型的键和值,非常灵活。

  • 可变字段 mutvalueprenext 都被标记为 mut,意味着它们可以在创建后修改。这对于我们需要频繁调整链表结构的 LRU 缓存来说是必须的。

  • 可选类型 ?prenext 是可选类型,表示它们可能为 None。这样处理链表两端的节点会更加自然。

  • 简单构造函数new_node 函数帮助我们创建一个新节点,初始状态下前驱和后继都是 None

LRU 缓存结构

接下来,我们来定义 LRU 缓存的主体结构:

// LRU缓存结构体
struct LRUCache[K, V] {
  capacity : Int // 容量
  dummy : Node[K, V] // 哑节点,用于标记双向链表的头尾
  key_to_node : Map[K, Node[K, V]] // 键到节点的映射
}

这个结构包含三个关键字段:

  • capacity:定义了缓存可以存储的最大键值对数量。

  • dummy:一个特殊的哑元节点,不存储实际的键值对,而是用来简化链表操作。使用哑元节点是一个常见的编程技巧,它可以帮助我们避免处理空链表和边界条件的特殊情况。

  • key_to_node:一个从键到节点的映射表,使我们能够在 O(1) 时间内通过键找到对应的节点。

为什么使用哑元节点?

哑元节点的使用是一个很巧妙的设计。我们将在链表中使用一个环形结构,其中哑元节点同时充当链表的“头“和“尾“:

  • dummy.next 指向链表中最近使用的节点(实际的第一个节点)
  • dummy.pre 指向链表中最久未使用的节点(实际的最后一个节点)

这样的设计使得我们在处理节点插入和删除时,不必担心空链表的特殊情况,代码逻辑会更加统一和清晰。

通过这两个基础数据结构,我们已经为实现一个高效的 LRU 缓存打下了基础。在下一部分,我们将开始实现 LRU 缓存的构造函数和核心操作。

7.3. 构造函数实现 [blog/lrualgorithm/construction]

现在我们已经定义好了基础数据结构,接下来需要实现 LRU 缓存的构造函数。构造函数是任何数据结构的起点,它负责正确初始化内部状态。

构造函数的设计

在设计 LRU 缓存的构造函数时,我们需要考虑:

  • 初始化缓存的最大容量
  • 创建并设置哑元节点
  • 初始化空的键值映射表

让我们看看如何用 MoonBit 实现这个构造函数:

fn new[K : Hash + Eq, V](
  capacity : Int,
  default_k : K,
  default_v : V
) -> LRUCache[K, V] {
  // 创建一个哑元节点,使用提供的默认值
  let dummy = new_node(default_k, default_v)

  // 初始化dummy节点,指向自身形成环
  dummy.next = Some(dummy)
  dummy.pre = Some(dummy)
  { capacity, dummy, key_to_node: Map::new() }
}

这段代码做了几件重要的事情:

  • 泛型约束:注意 K : Hash + Eq 这个约束,它表明我们的键类型必须支持哈希操作和相等性比较。这是因为我们要用键来创建哈希映射,所以键必须是可哈希和可比较的。

  • 默认值参数:我们需要 default_kdefault_v 来初始化哑元节点。这是 MoonBit 类型系统的要求,即使哑元节点不用于存储实际数据,我们也需要为它提供合法的值。

  • 自引用环:我们将哑元节点的 nextpre 都指向自身,形成一个空的环形链表。这是一种巧妙的技巧,确保我们在链表为空时,不会遇到空指针问题。

  • 返回结构体实例:使用了 MoonBit 的结构体字面量语法 { capacity, dummy, key_to_node: Map::new() } 创建并返回了 LRUCache 的实例。

为什么要形成环形结构?

你可能注意到了,我们将哑元节点的前驱和后继都指向了自身,形成了一个环。这样做的好处是:

  • 不需要处理空链表的边界情况
  • 插入第一个节点和之后的节点使用相同的逻辑
  • 删除最后一个节点和之前的节点使用相同的逻辑

在空链表中,哑元节点既是“头“也是“尾“。当我们添加实际节点时,它们会被插入到这个环中,而哑元节点始终保持在原位,帮助我们定位链表的逻辑起点和终点。

示意图说明

初始状态下,我们的链表结构如下:

dummy ⟷ dummy (自己指向自己)

添加一个节点 A 后:

dummy ⟷ A ⟷ dummy

添加另一个节点 B(放在最近使用的位置)后:

dummy ⟷ B ⟷ A ⟷ dummy

在这个结构中,dummy.next 指向最近使用的节点(B),而 dummy.pre 指向最久未使用的节点(A)。

这样的设计为我们后面实现 getput 等核心操作奠定了基础。下一步,我们将实现这些核心操作以完成 LRU 缓存的功能。

7.4. 核心操作 - get 和 put [blog/lrualgorithm/core]

接下来我们要实现 LRU 缓存的两个核心操作:getput。这两个操作是 LRU 缓存的精髓所在,也是最常用的接口。

get 方法实现

get 方法用于从缓存中获取某个键对应的值。如果键存在,它还需要将对应的节点移到“最近使用“的位置:

fn get[K : Hash + Eq, V](self : LRUCache[K, V], key : K) -> V? {
  let node = get_node(self, key)
  match node {
    Some(n) => Some(n.value)
    None => None
  }
}

这个实现看起来很简单,但它内部调用了 get_node 方法,这个方法不仅查找节点,还负责调整节点位置。下面是 get_node 的实现:

fn get_node[K : Hash + Eq, V](self : LRUCache[K, V], key : K) -> Node[K, V]? {
  if self.key_to_node.contains(key) {
    if self.key_to_node.get(key) is Some(node) {
      // 将节点移到链表前端
      remove(self, node)
      push_front(self, node)
      return Some(node)
    }
  }
  None
}

get_node 方法做了几件重要的事:

  1. 检查键是否存在于哈希表中
  2. 如果存在,获取对应的节点
  3. 将节点从当前位置移除
  4. 将节点插入到链表前端(表示最近使用)
  5. 返回找到的节点

这里我们用到了两个辅助方法 removepush_front(后面会详细介绍),它们负责链表的具体操作。

put 方法实现

put 方法用于向缓存中添加或更新键值对:

fn put[K : Hash + Eq, V](self : LRUCache[K, V], key : K, value : V) -> Unit {
  // 如果键已存在,更新值并移到链表前端
  let existing = get_node(self, key)
  if existing is Some(node) {
    node.value = value
    return
  }

  // 创建新节点
  let node = new_node(key, value)

  // 将新节点加入链表前端
  push_front(self, node)
  self.key_to_node.set(key, node)

  // 如果超出容量,删除最久未使用的节点
  if self.key_to_node.size() > self.capacity {
    if self.dummy.pre is Some(last_node) {
      self.key_to_node.remove(last_node.key)
      remove(self, last_node)
    }
  }
}

put 方法的逻辑分为几个部分:

  1. 检查键是否已存在

    • 如果存在,直接更新值并调整位置(通过前面的 get_node 方法)
    • 这里我们只需要修改值,因为 get_node 已经将节点移到了链表前端
  2. 创建新节点

    • 如果键不存在,则创建一个新的节点存储键值对
  3. 添加到链表和哈希表

    • 将新节点插入到链表前端
    • 在哈希表中添加键到节点的映射
  4. 检查容量并可能淘汰

    • 如果缓存大小超过了容量,需要淘汰最久未使用的项
    • 最久未使用的项就是链表尾部(dummy.pre)指向的节点
    • 从哈希表和链表中都删除这个节点

LRU 算法的核心思想

通过这两个方法,我们可以看到 LRU 算法的核心思想:

  • 每次访问(get)或更新(put)一个键,都将它移到“最近使用“位置
  • 当需要淘汰时,移除“最久未使用“位置的键

这种设计确保了我们总是保留最有可能再次被访问的数据,而丢弃最不可能再次被访问的数据,从而最大化缓存的命中率。

在下一部分,我们将详细介绍 push_frontremove 这两个关键的辅助方法,它们是实现 LRU 缓存链表操作的基础。

7.5. 辅助操作 - push_front 和 remove [blog/lrualgorithm/auxiliary]

在上一部分中,我们实现了 LRU 缓存的核心操作 getput,但它们都依赖于两个关键的辅助方法:push_frontremove。这两个方法负责维护双向链表的结构,是整个 LRU 算法能够正常工作的基础。

push_front 方法实现

push_front 方法用于将一个节点插入到链表的最前端(即最近使用的位置):

fn push_front[K, V](self : LRUCache[K, V], node : Node[K, V]) -> Unit {
  node.next = self.dummy.next
  node.pre = Some(self.dummy)
  if node.pre is Some(pre) {
    pre.next = Some(node)
  }
  if node.next is Some(next) {
    next.pre = Some(node)
  }
}

这个方法的逻辑虽然只有几行,但需要仔细理解:

  1. 将新节点的 next 指向原来的第一个节点(即 dummy.next
  2. 将新节点的 pre 指向哑元节点
  3. 更新哑元节点的 next 指向新节点
  4. 更新原第一个节点的 pre 指向新节点

通过这四步,我们完成了在链表头部插入新节点的操作。注意我们使用了 is Some 模式匹配来安全地处理可选值,这是 MoonBit 处理空值的一种优雅方式。

remove 方法实现

remove 方法用于从链表中删除一个节点:

fn remove[K, V](self : LRUCache[K, V], node : Node[K, V]) -> Unit {
  if node.pre is Some(pre) {
    pre.next = node.next
  }
  if node.next is Some(next) {
    next.pre = node.pre
  }
}

这个方法的实现非常直观:

  1. 将节点的前一个节点的 next 指向节点的下一个节点
  2. 将节点的下一个节点的 pre 指向节点的前一个节点

通过这两步,节点就从链表中“断开“了,不再是链表的一部分。

为什么这两个操作如此重要?

这两个看似简单的操作是整个 LRU 缓存算法的关键:

  • push_front 确保最近访问的项总是位于链表的前端
  • remove 用于两个场景:
    1. 将节点从当前位置移除,然后重新插入到链表前端(更新使用顺序)
    2. 淘汰最久未使用的节点(当缓存超出容量时)

通过这两个基本操作,我们能够维护一个按照“最近使用“到“最久未使用“排序的双向链表,从而实现 LRU 缓存的核心功能。

双向链表操作的细节

在处理双向链表时,容易出现的错误是指针操作顺序不当导致链表断裂或形成环。我们的实现避免了这些问题:

  • push_front 中,我们先设置新节点的指针,再更新相邻节点的指针
  • remove 中,我们直接更新相邻节点的指针,跳过要删除的节点

这种实现方式确保了链表操作的安全性和正确性。

使用哑元节点的优势

回顾一下我们设计中使用的哑元节点(dummy node),它带来了以下优势:

  • 简化了链表为空的处理
  • 统一了节点插入和删除的逻辑
  • 提供了稳定的“头“和“尾“引用点

有了这些辅助操作,我们的 LRU 缓存算法就更加完整了。接下来,我们会添加一些额外的实用方法,让我们的 LRU 缓存更加易用。

7.6. 实用辅助方法 [blog/lrualgorithm/auxiliary-other]

我们已经实现了 LRU 缓存的核心功能,包括基本数据结构、构造函数、核心操作 get/put 以及链表操作的辅助方法。为了让我们的 LRU 缓存更加完整和易用,现在我们来添加一些实用的辅助方法。

获取缓存大小

首先,我们实现一个方法来获取当前缓存中的元素数量:

fn size[K, V](self : LRUCache[K, V]) -> Int {
  self.key_to_node.size()
}

这个方法非常简单,直接返回哈希表的大小,因为哈希表中的每一项都对应缓存中的一个元素。

检查缓存是否为空

接下来,我们添加一个方法来检查缓存是否为空:

fn is_empty[K, V](self : LRUCache[K, V]) -> Bool {
  self.key_to_node.size() == 0
}

这个方法检查哈希表是否为空,从而判断整个缓存是否为空。

检查键是否存在

最后,我们实现一个方法来检查缓存中是否存在某个键:

fn contains[K : Hash + Eq, V](self : LRUCache[K, V], key : K) -> Bool {
  self.key_to_node.contains(key)
}

这个方法直接利用哈希表的 contains 方法,快速判断一个键是否在缓存中。

这些辅助方法的意义

虽然这些方法看起来很简单,但它们对于实际使用 LRU 缓存非常有价值:

  • 提高可读性:使用 is_empty()size() == 0 更直观
  • 封装实现细节:用户不需要知道内部使用了 key_to_node 哈希表
  • 接口完整性:提供了一套完整的接口,满足各种使用场景

这些辅助方法体现了良好的 API 设计原则 —— 简单、一致且易于使用。通过提供这些方法,我们的 LRU 缓存实现更加健壮和用户友好。

实际应用示例

这些辅助方法在实际应用中非常有用,例如:

// 检查键是否存在,而不获取值(避免改变使用顺序)
if contains(cache, "key") {
  // 键存在,可以进行一些操作
}

// 缓存为空时执行特定逻辑
if is_empty(cache) {
  // 缓存为空,可以执行初始化或其他操作
}

// 获取缓存使用情况
let usage_percentage = size(cache) * 100 / cache.capacity

这些方法虽然简单,但它们大大增强了 LRU 缓存的实用性。通过这些辅助方法,我们的 LRU 缓存实现已经相当完整和实用。

7.7. 总结与思考 [blog/lrualgorithm/summary]

终于到了我们 LRU 缓存实现之旅的终点。这一路走来,我们从基本概念开始,一步步构建了一个完整的 LRU 缓存。说实话,当我第一次接触 LRU 算法时,就被它简单而优雅的设计所吸引。在实现过程中,我不仅体会到了算法的精妙之处,也感受到了 MoonBit 语言的表达力。

回顾整个实现过程,我最满意的是数据结构的选择。哈希表和双向链表的组合虽然是经典方案,但在 MoonBit 中实现时,语言本身的特性让代码显得格外简洁。特别是哑元节点的使用,解决了链表操作中的边界情况,让代码逻辑更加一致。这种小技巧看似简单,却能大幅简化实现,减少潜在的错误。

在编写过程中,我发现 MoonBit 的类型系统非常适合这类数据结构的实现。泛型让我们的缓存可以适用于各种类型的键值对,而可选类型(Option 类型)则优雅地处理了可能不存在的值的情况。与其他语言相比,不必担心空指针异常是一种解脱,让我可以更专注于算法本身的逻辑。

对我而言,编写 getput 方法是最有趣的部分。这两个方法看似简单,却包含了 LRU 算法的核心思想:每次访问都要更新使用顺序,确保最近使用的项目保留在缓存中。当我看到这些方法能够正确工作时,那种成就感是难以形容的。

说到实际应用,这种 LRU 缓存在日常开发中其实非常实用。我曾在一个网页应用中使用类似的缓存来存储频繁访问的数据,显著提升了应用响应速度。见过太多项目因为缺乏合理的缓存策略而性能低下,一个好的 LRU 实现往往能起到事半功倍的效果。

当然,这个实现还有改进空间。比如添加线程安全支持,或者引入基于时间的过期策略。在实际项目中,我会考虑根据具体需求扩展这些功能。不过,目前的实现已经涵盖了 LRU 缓存的核心功能,足以应对大多数场景。

我最大的收获可能是深入理解了算法与数据结构如何相互配合。LRU 缓存的优雅之处在于它巧妙地结合了两种数据结构,各取所长,达到了理想的性能。这种思路启发我在面对其他问题时,不要局限于单一的数据结构,而是思考如何组合现有工具来获得最佳解决方案。

最后,希望这个 LRU 缓存的实现过程对你有所帮助。无论你是在学习 MoonBit 语言,还是想深入了解缓存算法,我都希望这篇文章能给你一些启发。编程的乐趣不仅在于解决问题,还在于创造优雅的解决方案。在这个意义上,LRU 缓存是一个小巧而完美的例子。

如果你有任何问题或改进建议,欢迎在 Github 留言讨论。毕竟,代码和思想总是在交流中不断完善的。

Blog 8. Understanding Local Type Inference [blog/lti]

在静态类型编程语言的演进历程中,类型推断(type inference)机制始终扮演着至关重要的角色。 它允许程序员省略那些可由上下文导出的类型标注,从而极大地降低了代码的冗余度, 使得程序无论在阅读还是编写上都更为便捷。

在这一背景下,System $F_\leq$ 堪称一座里程碑式的理论高峰。 它优雅地统一了两种在现代编程中至关重要的概念:源自面向对象编程、 为代码复用与抽象提供极大便利的子类型化(subtyping), 以及作为泛型编程基石的非直谓多态impredicative polymorphism)。 然而,一个严峻的现实阻碍了其在实践中的广泛应用: 其强大的表达能力,使得完全类型推断(complete type inference)被证明是不可判定的(undecidable)难题。

本文基于 Pierce 与 Turner 的研究 Local Type Inference, 但也关注工程实践。 它提出了一条迥然不同的路径:摒弃对「完全性」的执着,转而探索一种更简单、更务实的部分类型推断(partial type inference)。其核心理念,在于引入一个额外的简化原则 —— 局部性(locality)。 所谓「局部」,意指任何缺失的类型标注,都应仅仅依据其在语法树上的相邻节点信息来恢复,而不引入任何长距离的约束(例如 Algorithm J 中的那种全局性的合一变量)。

8.1. How to Read Typing Rules [blog/lti/how_to_read]

对于初次接触编程语言理论的读者而言,文中遍布的数学符号与推导规则或许会显得有些陌生和令人生畏。 请不必担忧。这些形式化工具并非为了故作高深,恰恰相反, 它们是为了达到自然语言难以企及的精确性(precision)与无歧义性(unambiguity)。 本节将提供一份阅读这些规则的简单指南,熟悉的读者可以直接跳过。

读者可以将这些规则,看作是一门编程语言最根本的「物理定律」。它们以一种极为严谨的方式, 定义了什么样的程序是结构良好、有意义的,而什么样的程序则不是。

本文中的大多数规则,都呈现为如下的结构: $$\frac{\text{前提}_1 \quad \text{前提}_2 \quad ...}{\text{结论}} \quad (\text{规则名称})$$ 这条长长的横线,是理解一切的核心。

  • 横线上方:前提(Premises)
    • 这里列出的是一组条件假设
    • 只有当所有前提都得到满足时,这条规则才能被激活或使用。
  • 横线下方:结论(Conclusion)
    • 这是在所有前提都满足后,我们能够推导出的新事实
  • 右侧括号:规则名称 (Rule Name)
    • 这只是为了方便我们引用和讨论,给规则起的一个名字,如 VarApp

在规则的前提与结论中,您会反复看到一种形如 $\Gamma \vdash e : T$ 的核心判断(judgment)。让我们来拆解它的每一个符号:

  • $\Gamma$ (Gamma):这是上下文(Context)。它代表了我们进行推导时,所有已知的背景信息或假设。通常,它记录了变量已经被赋予的类型,例如:$x : \mathbb{Z},\ f : \mathrm{Bool} \to \mathrm{Bool}$。您可以把它看作是「在…的环境下」或「已知…」。
  • $\vdash$ (Turnstile):这个符号读作「推导出」或「证明」。它是上下文与待证论断之间的分隔符。
  • $e$:这是项(Term),即我们正在分析的那段程序代码。它可以是一个简单的变量 $x$,一个函数 $\mathsf{fun}(x)\ x + 1$,或是一个复杂的表达式。
  • $:$ 表示「拥有类型」(has type)。
  • $T$:这是类型(Type),例如 $\mathbb{Z}$、$\mathrm{Bool}$、$\mathrm{String} \to \mathbb{Z}$ 等。

将它们组合在一起,$\Gamma \vdash e : T$ 这整个判断的直白解读就是:「在上下文 $\Gamma$ 所提供的已知条件下,我们可以推导出(或证明),程序项 $e$ 拥有类型 $T$。」

8.2. Just Enough Type Information [blog/lti/enough]

在放弃了对「完全类型推断」的追求之后,一个至关重要的问题便浮现出来:一个「部分」类型推断算法,其推断能力需要达到何种程度,才算是「足够」?一个极具实践智慧的回答:一个好的部分类型推断算法,其核心使命在于消除那些既普遍又愚蠢的类型标注。

此处的「愚蠢」与「合理」相对。「合理的」标注,如顶级函数定义中对其参数的类型声明,通常能作为有价值的、且经由编译器检查的文档,帮助人们理解代码。「愚蠢的」标注则恰恰相反,它们徒增代码的冗余,却几乎不提供任何有用的信息。可以想见,在一个完全显式类型的语言中,任何人都不会愿意去书写或阅读 cons[Int](3, nil[Int]) 中那两个多余的 Int 标注。

Pierce 对十几万行 ML 代码的调研,揭示了三种最主要的「愚蠢标注」来源:

  • 多态实例化:在所测量的代码中,类型应用(即对多态函数的实例化)的现象无处不在,平均来看,每三行代码中就至少出现一次。这些在多态函数调用点插入的类型参数,几乎没有任何文档价值,纯属语法上的累赘。
  • 匿名函数定义:在类似 map(list, fun(x) x+1) 这样的上下文中,为匿名函数的参数 x 补上类型标注,只会掩盖其核心逻辑,实为一种不必要的干扰。
  • 局部变量绑定 (Let): 为这些生命周期短暂的中间变量一一标注类型,显然是繁琐且意义不大的。

基于上述的定量观察,我们可以勾画出一个「足够」的部分类型推断算法的轮廓:

  1. 它必须能够推断出多态函数应用中的类型参数。与此同时,要求程序员为顶级函数或相对稀少的局部函数提供显式标注,则是完全可以接受的,因为这些标注本身就是有益的文档。
  2. 为了使高阶编程更加便捷,算法应当能够推断匿名函数参数的类型,尽管这并非绝对必要。
  3. 局部变量绑定通常不应要求显式的类型标注。

8.2.1. Strategies [blog/lti/strategies]

为了实现我们的目标,我们需要设计一套高效的策略来处理上述三种类型推断的场景。 下面的是两种本文将要介绍的主要策略:

  • 局部类型参数合成 (Local Synthesis of Type Arguments):此策略旨在自动推断多态函数应用中被省略的类型参数。其基本思路是,通过比较函数参数的期望类型与实际参数的类型,生成一组关于待定类型参数的局部子类型约束。随后,算法会求解这组约束,并选取一组能使整个应用表达式获得「最佳」(即最精确、最小)结果类型的解。
  • 双向类型信息传播 (Bidirectional Propagation of Type Information):此策略主要用于推断匿名函数中绑定变量的类型标注。它通过将类型信息从外围的表达式(如函数应用节点)向下传播至其子表达式,从而为子表达式提供一个「期望类型」,以指导其类型检查过程。

这两项技术均恪守「局部性」原则,即所有推断所需的信息都只在语法树的相邻节点间传递,不涉及长距离的依赖或全局性的合一变量。

8.3. Language Specification [blog/lti/language]

在严谨地探讨类型推导这一议题之前,我们必须首先清晰地界定其推断的目标——一个无歧义的、 被完全标注的内核语言(internal language)。此语言是编译器内部的「真实」表达,亦是程序员书写的、 允许省略标注的外部语言(external language)所要翻译成的最终形式。 本文所用的内核语言,源自 Cardelli 与 Wegner 提出的,融合了子类型化与非论域性多态的著名演算 System $F_\leq$, 但在此基础上我们增设了 $\bot$ (Bottom) 类型,为了保证上确界和下确界的存在,这种代数结构的完备性, 是后续章节中约束求解算法得以简洁、确定地运行的根本保障。此外它也可以被用作那些永不返回的表达式(如抛出异常的函数)的结果类型, 我们先定义形式语言如下 (注:横线是序列记号 $\overline{X} = X_1, X_2, \dots, X_n$,类似的,$\overline{x} : \overline{T} = x_1 : T_1, \dots, x_n : T_n$):

$$ \begin{array}{ll} T ::= X & \text{type variable} \\ \quad~\mid~ \top & \text{maximal type} \\ \quad~\mid~ \bot & \text{minimal type} \\ \quad~\mid~ \forall \overline{X} . \overline{T} \rightarrow T & \text{function type} \\[1em] e ::= x & \text{variable} \\ \quad~\mid~ \text{fun}[ \overline{X} ]\, ( \overline{x} : \overline{T} )\, e & \text{abstraction} \\ \quad~\mid~ e[ \overline{T} ]\, ( \overline{e} ) & \text{application} \\[1em] \Gamma ::= \bullet & \text{empty context} \\ \quad~\mid~ \Gamma, x : T & \text{variable binding} \\ \quad~\mid~ \Gamma, X & \text{type variable binding} \end{array} $$

我们可将上面的形式语言简单翻译到下面的 MoonBit 代码, 其中 Var 是类型变量的实现:

pub(all) enum Type {
  TyVar(Var)
  TyTop
  TyBot
  TyFun(Array[Var], Array[Type], Type)
} derive(Eq)

pub(all) enum Expr {
  EVar(Var)
  EApp(Expr, Array[Type], Array[Expr])
  EAbs(Array[Var], Array[(Var, Type)], Expr)
}

8.3.1. Subtyping Relation [blog/lti/subtype]

子类型关系,记作 $S \lt: T$(读作 $S$ 是 $T$ 的一个子类型),是本形式系统的核心。它定义了类型之间的一种「可替换性」:凡是需要类型 $T$ 的地方,都可以安全地使用一个类型为 $S$ 的项来代替。

与许多理论文献中的定义不同,本文特意选择了一种算法化(algorithmic)的方式来呈现子类型关系。这意味着,定义中仅包含一组最核心的、可直接用于实现判定的规则,而像传递性(transitivity)这样通常作为公理的性质,在此系统中则成为了可被证明的引理。这种风格使得定义本身更接近于一个类型检查算法的规约:

$$ \begin{array}{ll} X \lt: X & \text{(S-Refl)} \\[1em] T \lt: \top & \text{(S-Top)} \\[1em] \bot \lt: T & \text{(S-Bot)} \\[1em] \dfrac{ \overline{T} \lt: \overline{R} \quad S \le: U }{ \forall \overline{X}. \overline{R} \rightarrow S \lt: \forall \overline{X}. \overline{T} \rightarrow U } & \text{(S-Fun)} \end{array} $$

其中 $\overline{T} \lt: \overline{R}$ 成立当且仅当 $\text{len}(T) = \text{len}(S) \land \forall 1 \leq i \leq \text{len}(S). S_i \lt: T_i$。 S-Fun 规则体现了函数类型子类型化的核心特征:在参数类型上是逆变(contravariant)的(子类型关系的箭头方向反转),而在返回类型上是协变(covariant)的(子类型关系箭头方向保持不变)。读者可以自己尝试一下将上文的形式语言翻译到 MoonBit 的一个谓词函数,或参考下面折叠起来的代码片段。

8.3.1.1. Solution [blog/lti/subtype_code]

/// l <: r
struct Subtype {
  l : Type
  r : Type
}

pub fn subtype(self : Subtype) -> Bool {
  match (self.l, self.r) {
    (TyVar(v1), TyVar(v2)) => v1 == v2
    (_, TyTop) => true
    (TyBot, _) => true
    (TyFun(xs1, r, s), TyFun(xs2, t, u)) if xs1 == xs2 =>
      subtypes(t, r) && { l: s, r: u }.subtype()
    _ => false
  }
}

为了支持后续的约束求解算法,系统必须能计算任意两个类型的最小上界(join, 记作 $\lor$)和最大下界(meet, 记作 $\land$)。得益于 $\bot$ 和 $\top$ 的存在,这两个运算在本系统中是全函数(total functions),即对于任意一对类型,其界都必然存在。下面我们给出这两个运算的定义:

  • 最小上界 $S \vee T$

    • 若 $S \lt: T$,则结果为 $T$。
    • 若 $T \lt: S$,则结果为 $S$。
    • 若 $S$ 和 $T$ 分别为 $\forall\overline{X}.\overline{V} \to P$ 和 $\forall\overline{X}.\overline{W} \to Q$,则结果为 $\forall\overline{X}.(\overline{V} \wedge \overline{W}) \to (P \vee Q)$。
    • 在其他所有情况下,结果为 $\top$
  • 最大下界 $S \wedge T$

    • 若 $S \lt: T$,则结果为 $S$。
    • 若 $T \lt: S$,则结果为 $T$。
    • 若 $S$ 和 $T$ 分别为 $\forall\overline{X}.\overline{V} \to P$ 和 $\forall\overline{X}.\overline{W} \to Q$,则结果为 $\forall\overline{X}.(\overline{V} \vee \overline{W}) \to (P \wedge Q)$。
    • 在其他所有情况下,结果为 $\bot$

通过简单的结构归纳法可以证明,这两个运算满足以下性质:

  • $S \vee T$ 和 $S \wedge T$ 分别是 $S$ 和 $T$ 的最小上界和最大下界。
  • $S \lt: U$ 且 $T \lt: U$ 则 $S \vee T \lt: U$
  • $U \lt: S$ 且 $U \lt: T$ 则 $U \lt: S \wedge T$

这里同样鼓励读者自己进行代码翻译,答案可展开下面的代码片段。

8.3.1.2. Solution [blog/lti/subtype_code2]

在 MoonBit 代码中我们将 $S \vee T$ 实现为 s | t, 将 $S \wedge T$ 实现为 s & t。这两个运算符的定义如下:

impl BitAnd for Type with land(s, t) {
  match (s, t) {
    (TyFun(xs1, v, p), TyFun(xs2, w, q)) if xs1 == xs2 => {
      guard v.length() == w.length() else { TyBot }
      TyFun(xs1, v.zip(w).map(z => z.0 | z.1), p & q)
    }
    (s, t) if s.subtype(t) => s
    (s, t) if t.subtype(s) => t
    _ => TyBot
  }
}

impl BitOr for Type with lor(s, t) {
  match (s, t) {
    (TyFun(xs1, v, p), TyFun(xs2, w, q)) if xs1 == xs2 => {
      guard v.length() == w.length() else { TyTop }
      TyFun(xs1, v.zip(w).map(z => z.0 & z.1), p | q)
    }
    (s, t) if s.subtype(t) => t
    (s, t) if t.subtype(s) => s
    _ => TyTop
  }
}

8.4. Explicit Typing Rules [blog/lti/explicit]

在定义了类型与子类型关系之后,我们便可以给出内核语言的类型定则。这些规则定义了类型判断(typing judgment)的形式 $\Gamma \vdash e : T$,意为「在上下文 $\Gamma$ 中,项 $e$ 拥有类型 $T$ 」。

与子类型关系的定义一脉相承,这里的类型定则同样采用了一种算法化的呈现方式。且省略了传统类型系统中常见的包容规则(subsumption,若 $e$ 的类型为 $S$ 且 $S \lt: T$,则 $e$ 的类型亦可为 $T$)。

通过省略此规则,本系统为每一个可被类型化的项,都计算出一个唯一的、最小的类型,作者称之为该项的显式类型(manifest type)。这一设计选择,并不改变语言中可被类型化的项的集合,而只是确保了任何一个项的类型推导路径都是唯一的。这极大地增强了系统的可预测性。

核心定则 (Core Rules)

  • 变量 (Variable)

    $$ \frac{}{\Gamma \vdash x : \Gamma(x)} \quad (\text{Var}) $$

  • 抽象 (Abstraction) 此规则统一了传统的项抽象与类型抽象。

    $$ \frac{\Gamma, \overline{X}, \overline{x}:\overline{S} \vdash e : T}{\Gamma \vdash \mathbf{fun}[\overline{X}] (\overline{x}:\overline{S}) e : \forall \overline{X}.\overline{S} \to T} \quad (\text{Abs}) $$

    若想要求解 $\mathbf{fun}[\overline{X}] (\overline{x}:\overline{S})$ 的类型,必须在上下文 $\Gamma$ 中添加类型变量 $\overline{X}$ 和值变量 $\overline{x}:\overline{S}$ 的绑定。然后,在这个扩展的上下文中,推导函数体 $e$ 的类型为 $T$。最终,整个函数的类型便是 $\forall \overline{X}.\overline{S} \to T$。

  • 应用 (Application) 此规则同样统一了传统的项应用与多态应用。它首先推导函数 f 的类型,然后验证所有实际参数(包括类型参数与项参数)是否与函数的签名相符。 这里的要求更宽松了一些:只要实际参数的类型满足参数类型的子类型关系即可,而不需要完全匹配。

    $$ \frac{\Gamma \vdash f : \forall \overline{X} . \overline{S} \to R \quad \Gamma \vdash \overline{e} \lt: [\overline{T}/\overline{X}]\overline{S}}{\Gamma \vdash f[\overline{T}] (\overline{e}) : [\overline{T}/\overline{X}]R} \quad (\text{App}) $$

    其中,记法 $\Gamma \vdash \overline{e} \lt: [\overline{T}/\overline{X}]\overline{S}$ 是一个缩写,表示 $\Gamma \vdash \overline{e} \lt: \overline{U}$,然后验证 $\overline{U} \lt: [\overline{T}/\overline{X}]\overline{S}$。最终,整个应用表达式的结果类型,是通过将实际类型参数 $\overline{T}$ 代入函数原始返回类型 $R$ 中得到的。

    8.4.1. Type Parameter Substitution [blog/lti/subst_code]

    这里出现了一个新的记号 $[\overline{T}/\overline{X}]R$, 它表示将类型参数 $\overline{X}$ 替换为实际类型 $\overline{T}$ 后的结果类型。 这个记号在后续的代码中会频繁出现。 下面的代码定义 mk_subst 函数,用来生成一个类型替换映射, 还有一个 apply_subst 函数可以将这个映射应用到一个具体类型上。 $[\overline{T}/\overline{X}]R$ 就是通过 $\text{apply\_subst}(\text{mk\_subst}(\overline{X},\overline{T}), R)$ 得到的。

    pub fn mk_subst(vars : Array[Var], tys : Array[Type]) -> Map[Var, Type] raise {
      guard vars.length() == tys.length() else { raise ArgumentLengthMismatch }
      Map::from_array(vars.zip(tys))
    }
    
    pub fn apply_subst(self : Type, subst : Map[Var, Type]) -> Type {
      match self {
        TyVar(v) => subst.get(v).unwrap_or(self)
        TyTop | TyBot => self
        TyFun(xs, ss, t) => {
          let fs = subst.iter().filter(kv => !xs.contains(kv.0)) |> Map::from_iter
          let new_ss = ss.map(s => s.apply_subst(fs))
          let new_t = t.apply_subst(fs)
          TyFun(xs, new_ss, new_t)
        }
      }
    }
    

  • Bot 应用 (Bot Application) $\bot$ 类型的引入,要求我们补充一条特殊的应用规则,以维护系统的类型安全(type soundness)。 由于 $\bot$ 是任何函数类型的子类型,一个类型为 $\bot$ 的表达式应当可以被应用于任何合法的参数,而不会产生类型错误。

    $$ \frac{\Gamma \vdash f : \bot \quad \Gamma \vdash \overline{e} : \overline{S}}{\Gamma \vdash f[\overline{T}] (\overline{e}) : \bot} \quad (\text{App-Bot}) $$

    此规则规定,当一个类型为 $\bot$ 的项被应用时,无论参数为何,整个表达式的结果类型也是 $\bot$,这正是我们能给出的最精确(即最小)的结果类型。

这些规则共同保证了本类型系统的一个关键性质,即显式类型的唯一性(Uniqueness of Manifest Types):若 $\Gamma \vdash e : S$ 且 $\Gamma \vdash e : T$,那么必有 $S=T$。

8.5. Local Type Argument Synthesis [blog/lti/synthesis]

截至目前,我们已经定义了内核语言的类型规则, 但是距离我们的目标还有很大距离:核心语言要求我们做出很多注解, 包括多态实例化时需要提供的类型参数,因为这在代码中非常常见,因此这是我们本节首要解决的痛点。

此即局部类型参数合成(Local Type Argument Synthesis)的目标:允许程序员在调用多态函数时,安全地省略其类型参数,写成 $\text{id}(3)$ 而不是 $\text{id}[\mathbb{Z}](3)$ 的形式。省略类型参数后,一个核心挑战随之而来:对于一个给定的应用,如 $\text{id} (x)$(其中 $x : \mathbb{Z}$,且 $\mathbb{Z} \lt: \mathbb{R}$),通常存在多种合法的类型参数实例化方案,例如这里的 $\text{id} [\mathbb{Z}](x)$ 或 $\text{id} [\mathbb{R}](x)$。我们必须确立一个清晰的标准来做出选择:选择能为整个应用表达式带来最精确(即最小)结果类型的类型参数。在 $\text{id} (x)$ 的例子中,由于 $\text{id} [\mathbb{Z}](x)$ 的结果类型 $\mathbb{Z}$ 是 $\text{id} [\mathbb{R}](x)$ 的结果类型 $\mathbb{R}$ 的一个子类型,前者显然是更优、更具信息量的选择。

然而,这种基于「最佳结果类型」的局部策略并非万能。在某些情况下,「最佳」解可能并不存在。例如,假设一个函数 $f$ 的类型为 $\forall X. () \to (X \to X)$。对于应用 $f()$,$f[\mathbb{Z}]()$ 和 $f[\mathbb{R}]()$ 都是合法的补全,其结果类型分别为 $\mathbb{Z} \to \mathbb{Z}$ 和 $\mathbb{R} \to \mathbb{R}$。这两种函数类型在子类型关系下是不可比较的,因此不存在一个唯一的最小结果类型。在这种情况下,局部合成宣告失败。

回顾之前的核心语言定义,我们要求 application 构造的形式为 $e[\overline{T}](\overline{e})$, 也就是说我们手动填写了类型参数 $\overline{T}$,规则 App 能够根据此参数为应用表达式计算出结果类型。 现在我们为了语言更简单易用,允许省略类型参数 $\overline{T}$,现在我们更新语言的构造:

pub(all) enum Type {
  TyVar(Var)
  TyTop
  TyBot
  TyFun(Array[Var], Array[Type], Type)
} derive(Eq)

pub(all) enum Expr {
  EVar(Var)
  EAppI(Expr, Array[Expr])
  EApp(Expr, Array[Type], Array[Expr])
  EAbs(Array[Var], Array[(Var, Type)], Expr)
  EAbsI(Array[Var], Array[Var], Expr)
}

这里加入了新的表达式结构 EAppI(Expr, Array[Expr]),对应我们的省略类型参数形式。 (为了后文叙述方便,这里也增加了后文会用到的 EAbsI 构造) 现在我们需要一条新的规则:

$$ \frac{\text{magic we don't know}}{\Gamma \vdash f (\overline{e}) : [\overline{T}/\overline{X}]R} \quad (\text{App-Magic}) $$

身为人类我们可以用直觉来制定规则,甚至设计出一些无法写成代码的声明式规则, 精确地定义「何为一次正确的、最优的类型参数推断」:

$$ \frac{ \begin{array}{l} \Gamma \vdash f : \forall \overline{X}. \overline{T} \to R \qquad \exists \overline{U} \\ \Gamma \vdash \overline{e} : \overline{S} \qquad |\overline{X}| > 0 \qquad \overline{S} \lt: [\overline{U}/\overline{X}]\overline{T} \\ \text{forall} (\overline{V}). \overline{S} \lt: [\overline{V}/\overline{X}]\overline{T} \implies [\overline{U}/\overline{X}]R \lt: [\overline{V}/\overline{X}]R \end{array} }{\Gamma \vdash f(\overline{e}) : [\overline{U}/\overline{X}]R} \quad (\text{App-InfSpec}) $$

此处我们使用存在量化 $\exists \overline{U}$,并且要求 $\overline{U}$ 满足很多条件。 例如 $\overline{S} \lt: [\overline{U}/\overline{X}]\overline{T}$ 为合法性约束。 它规定我们所选定的类型参数 $\overline{U}$ 必须是合法的。 所谓合法,即指将 $\overline{U}$ 代入函数的形式参数类型 $\overline{T}$ 后,实际参数的类型 $\overline{S}$ 必须是其子类型。 更重要的是最后一条 $\text{forall} (\overline{V}). \overline{S} \lt: [\overline{V}/\overline{X}]\overline{T} \implies [\overline{U}/\overline{X}]R \lt: [\overline{V}/\overline{X}]R$ 规则, 它要求我们对所有可能的类型参数元组 $\overline{V}$ 进行考量, 这可以转化为对潜在无限空间 $\overline{V}$ 进行搜索的过程,是典型的非构造性描述, 我们无法在计算机中实现它。

至此,我们的目标已经明确:我们需要一个真正可执行的算法,其结果与 (App-InfSpec) 一致, 但不需要我们进行非构造性的搜索和回溯。这正是「约束生成」这一步骤所要扮演的角色。 它的设计动机,源于对问题本身的一次精妙的视角转换。

8.6. Constraint Generation [blog/lti/cg]

与其将类型参数推断视为一个在无限可能性中「寻找并验证最优解」的搜索问题, 不妨将其重构为一个类似于解代数方程的「求解未知数边界」的问题。 我们不再去猜测类型参数 $\overline{X}$ 可能是什么, 而是通过分析子类型关系本身,去推导出 $\overline{X}$ 必须满足的条件。

观察到我们的规则存在子类型约束,不妨考虑一般情况 $S \lt: T$, 这本身就隐含着对其构成部分(包括其中的未知变量)的约束。 若 $X$ 是 $T$ 中的一个未知变量,那么 $S$ 的结构就必然会限制 $X$ 可能的形态。 我们的算法,正是要将这种隐含的、结构上的限制,转化为一组显式的、关于 $X$ 上下界的断言。

然而,在系统性地提取这些约束之前,我们必须首先面对一个与变量作用域相关的、 虽属前期准备但至关重要的挑战。若不妥善处理,我们生成的约束本身就可能是非良构的。 这一挑战,催生了算法的第一个具体操作步骤:变量消去。

8.6.1. Variable Elimination [blog/lti/var_elim]

设想我们想为变量 $X$ 生成约束,以使得类型 $\forall Y. () \to (Y\to Y)$ 成为 $\forall Y. () \to X$ 的一个子类型。根据函数子类型的逆变/协变规则,这要求 $Y \to Y \lt: X$。然而,我们不能直接生成约束 $\{ Y \to Y \lt: X \lt: \top\}$,因为类型变量 $Y$ 在此约束中是自由的,但它本应被 $\forall Y$ 所绑定,这就造成了一种作用域错误。

正确的做法是,找到 $Y \to Y$ 的一个不含 $Y$ 的、且尽可能精确的超类型,并用它来约束 $X$。在本例中,即 $\bot \to \top$。变量消去机制,正是为了形式化地完成这一「寻找最精确边界」的任务。

  1. 提升 (Promotion), $S \Uparrow^V T$:$T$ 是 $S$ 的一个不含集合 $V$ 中任何自由变量的最小超类型
  2. 下降 (Demotion), $S \Downarrow^V T$:$T$ 是 $S$ 的一个不含集合 $V$ 中任何自由变量的最大子类型

这两套关系由一组递归的定则所定义,确保了对于任何类型 $S$ 和变量集 $V$,其结果 $T$ 都是唯一且总能被计算出来的(即它们是全函数)。 此处建议读者停下来思考一下,如何设计这两套关系的递归规则并自己使用代码实现它(提示:对于提升规则的情况,若 $X\in V$ 则将其提升到 $\top$,反之不变,其他情况是显然的)

8.6.1.1. Promotion and Demotion Rules [blog/lti/ve_rules]

  • 提升规则 ($S \Uparrow^V T$)

    • 对于 $\top$ 和 $\bot$: $$ \top \Uparrow^V \top \quad (\text{VU-Top}) $$ $$ \bot \Uparrow^V \bot \quad (\text{VU-Bot}) $$
    • 对于类型变量 $X$:
      • 若 $X$ 属于需要被消除的集合 $V$,则将其提升至 $\top$。 $$ \frac{X \in V}{X \Uparrow^V \top} \quad (\text{VU-Var-1}) $$
      • 若 $X$ 不在 $V$ 中,则保持不变。 $$ \frac{X \notin V}{X \Uparrow^V X} \quad (\text{VU-Var-2}) $$
    • 对于函数类型:
      • 递归地对其参数类型进行下降(因为参数位置是逆变的),并对其返回类型进行提升(因为返回位置是协变的)。 $$ \frac{\overline{S} \Downarrow^V \overline{U} \quad T \Uparrow^V R \quad \overline{X} \notin V}{\forall\overline{X}.\overline{S} \to T \Uparrow^V \forall\overline{X}.\overline{U} \to R} \quad (\text{VU-Fun}) $$
  • 下降规则 ($S \Downarrow^V T$)

    • 对于 $\top$ 和 $\bot$ 的处理和提升规则一致。
    • 对于类型变量 $X$:
      • 若 $X$ 属于 $V$,则将其下降至 $\bot$。 $$ \frac{X \in V}{X \Downarrow^V \bot} \quad (\text{VD-Var-1}) $$
      • 若 $X$ 不在 $V$ 中,则保持不变。
    • 对于函数类型:
      • 递归地对其参数类型进行提升,并对其返回类型进行下降。 $$ \frac{\overline{S} \Uparrow^V \overline{U} \quad T \Downarrow^V R \quad \overline{X} \notin V}{\forall\overline{X}.\overline{S} \to T \Downarrow^V \forall\overline{X}.\overline{U} \to R} \quad (\text{VD-Fun}) $$

这可以非常直接地在 MoonBit 中实现:

pub fn promotion(self : Type, v : Set[Var]) -> Type {
  match self {
    TyFun(xs, ss, t) => {
      let vP = v.iter().filter(x => !xs.contains(x)) |> Set::from_iter
      let us = ss.map(_.demotion(vP))
      let r = t.promotion(vP)
      guard xs.iter().all(x => !v.contains(x))
      TyFun(xs, us, r)
    }
    TyVar(vr) if v.contains(vr) => TyTop
    _ => self
  }
}

pub fn demotion(self : Type, v : Set[Var]) -> Type {
  match self {
    TyFun(xs, ss, t) => {
      let vP = v.iter().filter(x => !xs.contains(x)) |> Set::from_iter
      let us = ss.map(_.demotion(vP))
      let r = t.demotion(vP)
      TyFun(xs, us, r)
    }
    TyVar(vr) if v.contains(vr) => TyBot
    _ => self
  }
}

这套精心设计的规则,保证了变量消去操作的正确性与最优性,这由两个关键引理所保证:

  • 可靠性(Soundness):若 $S \Uparrow^V T$,那么可以证明 $S \lt: T$ 且 $T$ 中确实不含 $V$ 中的自由变量。对偶地,若 $S \Downarrow^V T$,则 $T \lt: S$ 且 $T$ 不含 $V$ 中的自由变量。
  • 完备性(Completeness):此操作找到了「最好」的边界。例如,对于提升操作,若存在另一个不含 $V$ 中变量的 $S$ 的超类型 $T'$,那么 $S \Uparrow^V T$ 所计算出的 $T$ 必然是 $T'$ 的子类型(即 $T \lt: T'$),这证明了 $T$ 是所有可能选项中最小的那一个。

约束生成是局部类型参数合成算法的核心引擎。 在通过变量消去确保了作用域安全之后, 此步骤的使命是将一个子类型判定问题——例如, $S \lt: T$,其中 $S$ 或 $T$ 中含有待定的类型参数 $\overline{X}$ 转化为一组对这些未知参数 $\overline{X}$ 的显式约束。 现在我们形式化地定义代码中的约束具体是什么结构:

  • 约束 (Constraint):在本系统中,每一个约束都具有形式 $S_i \lt: X_i \lt: T_i$,它为单个未知类型变量 $X_i$ 同时指定了一个下界 (lower bound) $S_i$ 和一个上界 (upper bound) $T_i$ 。

  • 约束集 (Constraint Set):一个约束集 $C$ 是关于一组未知变量 $\overline{X}$ 到其对应约束的有限映射(在代码中可以实现为一个 Hash Map)。约束集的一个关键不变量是,其中任何约束的上下界($S_i, T_i$)都不能含有任何待定的未知变量(即 $\overline{X}$ 中的变量)或任何需要被消去的局部变量(即 $V$ 中的变量)。空约束集 ($\emptyset$) 代表最无限制的约束,相当于为每一个 $X_i$ 指定了约束 $\bot \lt: X_i \lt: \top$ 。

  • 约束集的交 ($\wedge$) 定义为两个约束集 $C$ 和 $D$ 的交集,是通过将其对同一个变量的约束进行合并得到的。新的下界是原下界的最小上界(join, $\vee$),而新的上界是原上界的最大下界(meet, $\wedge$)

8.6.2. Constraint and Constraint Set Code [blog/lti/cg_def_code]

struct Constraints(Map[Var, Subtype])

pub fn Constraints::empty() -> Constraints {
  Constraints(Map::new())
}

pub fn meet(self : Constraints, other : Constraints) -> Constraints {
  union_with(self.inner(), other.inner(), (l, r) => {
    let { l: l1, r: r1 } = l
    let { l: l2, r: r2 } = r
    { l: l1 & l2, r: r1 | r2 }
  })
}

pub fn meets(c : Array[Constraints]) -> Constraints {
  c.iter().fold(init=Constraints::empty(), Constraints::meet)
}

约束生成过程被形式化为一个推导关系 $V \vdash_{\overline{X}} S \lt: T \Rightarrow C$,其意为:在需要回避的变量集为 $V$ 的条件下,为使 $S \lt: T$ 成立,关于未知变量 $\overline{X}$ 需满足的(最弱)约束集是 $C$,这个 $C$ 可以被视为是该推导关系的输出。

算法由一组递归规则定义,其中关键规则如下(注:我们始终假定 $\overline{X} \cap V = \emptyset$):

  • 平凡情况 (Trivial Cases):当子类型关系的上界是 $\top$ 或下界是 $\bot$ 时,该关系无条件成立,因此生成一个空约束集 $\emptyset$ 。
  • 上界约束 (Upper Bound Constraint):当需要判定 $Y \lt: S$(其中 $Y \in \overline{X}$ 是未知变量,而 $S$ 是已知类型)时,算法会为 $Y$ 生成一个上界约束。 $$ \frac{Y \in \overline{X} \quad S \Downarrow^V T \quad \text{FV}(S) \cap \overline{X} = \emptyset}{V \vdash_{\overline{X}} Y \lt: S \Rightarrow \{ \bot \lt: Y \lt: T \}} \quad (\text{CG-Upper}) $$ 注意,这里利用了前述的变量消去操作($S \Downarrow^V T$)来确保上界 $T$ 本身是良构的。
  • 下界约束 (Lower Bound Constraint):对偶地,当需要判定 $S \lt: Y$ 时,算法为 $Y$ 生成一个下界约束。 $$ \frac{Y \in \overline{X} \quad S \Uparrow^V T \quad \text{FV}(S) \cap \overline{X} = \emptyset}{V \vdash_{\overline{X}} S \lt: Y \Rightarrow \{ T \lt: Y \lt: \top \}} \quad (\text{CG-Lower}) $$
  • 函数类型 (Function Type):当比较两个函数类型时,算法递归地处理其参数和返回类型,并将生成的子约束集合并。 $$ \frac{V \cup \{\overline{Y}\} \vdash_{\overline{X}} \overline{T} \lt: \overline{R} \Rightarrow \overline{C} \quad V \cup \{\overline{Y}\} \vdash_{\overline{X}} S \lt: U \Rightarrow D}{V \vdash_{\overline{X}} \forall \overline{Y}.\overline{R} \to S \lt: \forall \overline{Y}.\overline{T} \to U \Rightarrow (\bigwedge \overline{C}) \wedge D} \quad (\text{CG-Fun}) $$ 这里,通过对子约束集取交集 ($\wedge$),实现了约束的累积。

8.6.3. Constraint Generation Code [blog/lti/cg_code]

/// Pre-condition: xs and v are disjoint sets of variables.
pub fn generate(
  self : Subtype,
  xs : Array[Var],
  v : Set[Var],
) -> Constraints raise {
  match (self.l, self.r) {
    (_, TyTop) | (TyBot, _) => Constraints::empty()
    (TyVar(y1), TyVar(y2)) if y1 == y2 && !xs.contains(y1) =>
      Constraints::empty()
    (TyVar(y), s) if xs.contains(y) => {
      let t = s.demotion(v)
      Map::from_array([(y, { l: TyBot, r: t })])
    }
    (s, TyVar(y)) if xs.contains(y) => {
      let t = s.promotion(v)
      Map::from_array([(y, { l: t, r: TyTop })])
    }
    (TyFun(ys1, r, s), TyFun(ys2, t, u)) if ys1 == ys2 => {
      let vy = v.union(Set::from_array(ys1))
      let cs = t.zip(r).map(tr => { l: tr.0, r: tr.1 }.generate(xs, vy))
        |> meets()
      cs.meet({ l: s, r: u }.generate(xs, vy))
    }
    _ => raise ConstraintGenerationError
  }
}

一个至关重要的观察是,在任何一次调用 $V \vdash_{\overline{X}} S \lt: T \Rightarrow C$ 时,未知变量 $\overline{X}$ 都只会出现在 $S$ 和 $T$ 的其中一边。这使得整个过程是一个匹配模子类型(matching-modulo-subtyping)问题,而非一个完全的合一(unification)问题,从而保证了算法的简洁性与确定性。

8.7. Calculating Type Arguments [blog/lti/calc_args]

通过前述的约束生成步骤,我们已经成功地将一个非构造性的最优解搜索问题, 转化为了一个具体、有形的产物:一个约束集 $C$。 这个约束集,凝聚了为了使整个多态应用类型正确,所有待定类型参数 $\overline{X}$ 必须满足的全部边界条件。 对于每一个未知变量 $X_i$,我们都得到了一个形如 $S_i \lt: X_i \lt: T_i$ 的合法区间。

至此,算法的第一阶段「我们对未知数了解了什么?」已经圆满完成。 然而,我们的工作尚未结束。一个约束区间,例如 $\mathbb{Z} \lt: X \lt: \mathbb{R}$, 本身可能允许多个合法的解(如 $\mathbb{Z}$ 或 $\mathbb{R}$)。 我们最终必须为每一个 $X_i$ 挑选出一个具体的类型值,以完成对内核语言项的最终构造。

这就引出了算法的最后一个,也是画龙点睛的一步:我们应依据何种准则,从每个变量的合法区间中做出最终的选择? 答案,必须回归到我们的初衷,即 App-InfSpec 规约中所声明的最优性要求: 我们所做的选择,必须能使整个应用表达式获得唯一的、最小的结果类型。 因此,算法的最后一步,便是要设计一个选择策略, 它能利用我们已经辛勤收集到的约束集 $C$, 并结合函数原始的返回类型 $R$, 来计算出一组能最终最小化 $R$ 的具体类型参数。 这便是本节「参数计算」的核心任务。

8.7.1. Polarity [blog/lti/polarity]

为了计算关于 $R$ 的具体类型参数,还有一个至关重要的操作:变量代换导致的极性变化。 一个类型变量 $X$ 在另一个类型表达式 $R$ 中的极性,描述了当该变量的类型变大或变小时,整个表达式的类型会如何相应地变化。

  • 协变 (Covariant):若 $R$ 在 $X$ 上是协变的,则 $X$ 的「变大」(成为一个超类型)会导致 $R$ 也「变大」。例如,在 $T \to X$ 中,$X$ 是协变的。若 $\mathbb{Z} \lt: \mathbb{R}$,则 $T \to \mathbb{Z} \lt: T \to \mathbb{R}$。
  • 逆变 (Contravariant):若 $R$ 在 $X$ 上是逆变的,则 $X$ 的「变大」会导致 $R$ 「变小」(成为一个子类型)。例如,在 $X \to T$ 中,$X$ 是逆变的。若 $\mathbb{Z} \lt: \mathbb{R}$,则 $\mathbb{R} \to T \lt: \mathbb{Z} \to T$。
  • 不变 (Invariant):若 $R$ 在 $X$ 上是不变的,则只有当 $X$ 保持不变时,$R$ 才保持不变。任何改变都会导致不可比较的结果。例如,在 $X \to X$ 中,$X$ 是不变的。
  • 常量 (Constant):若 $R$ 在 $X$ 上是常量的,则 $X$ 的变化不会影响 $R$ 的类型。常量类型通常是指那些不包含变量的类型,如基本类型或具体的类。

现在我们对极性的考虑主要集中在函数类型之上, 只需要关注变量在函数类型中的位置即可(在箭头的左边还是右边), 当然,需要考虑到嵌套的函数结构。建议读者在此稍作停顿,考虑一下该算法的设计。 当然你也可以直接展开下面的代码块来查看具体实现。

8.7.1.1. Variance Code [blog/lti/variance_code]

pub fn variance(self : Type, va : Var) -> Variance {
  letrec go = (ty : Type, polarity : Bool) => match ty {
    TyVar(v) if v == va => if polarity { Covariant } else { Contravariant }
    TyVar(_) | TyTop | TyBot => Constant
    TyFun(_, params, ret) => {
      let param_variance = params
        .map(p => go(p, !polarity))
        .fold(init=Constant, combine_variance)
      combine_variance(param_variance, go(ret, polarity))
    }
  }
  and combine_variance = (v1 : Variance, v2 : Variance) => match (v1, v2) {
    (Constant, v) | (v, Constant) => v
    (Covariant, Covariant) | (Contravariant, Contravariant) => v1
    (Covariant, Contravariant) | (Contravariant, Covariant) => Invariant
    (Invariant, _) | (_, Invariant) => Invariant
  }

  go(self, true)
}

为了最小化返回类型 $R$,我们的选择策略变得显而易见:

  • 若 $X_i$ 在 $R$ 中是协变的,我们应为 $X_i$ 选择其合法区间内的最小值,即其约束的下界
  • 若 $X_i$ 在 $R$ 中是逆变的,我们应为 $X_i$ 选择其合法区间内的最大值,即其约束的上界
  • 若 $X_i$ 在 $R$ 中是不变的,则为了保证结果的唯一性与可比较性,其合法区间必须是一个「点」,即其约束的上下界必须相等

上述策略被形式化为一个计算最小代换(minimal substitution) $\sigma_{CR}$ 的算法。给定一个可满足的约束集 $C$ 和返回类型 $R$:

对于 $C$ 中的每一个约束 $S \lt: X_i \lt: T$:

  • 若 $R$ 在 $X_i$ 上是协变常数的,则 $\sigma_{CR}(X_i) = S$。
  • 若 $R$ 在 $X_i$ 上是逆变的,则 $\sigma_{CR}(X_i) = T$。
  • 若 $R$ 在 $X_i$ 上是不变的,且 $S=T$,则 $\sigma_{CR}(X_i) = S$。
  • 在其他所有情况下(尤其是不变变量的约束区间 $S \neq T$ 时),$\sigma_{CR}$ 未定义

当 $\sigma_{CR}$ 未定义时,算法宣告失败,这精确地对应了 App-InfSpec 中无法找到唯一最优解的情形。

8.7.2. Solving Constraints [blog/lti/solve_code]

pub fn solve(self : Constraints, ty : Type) -> Map[Var, Type]? {
  let f = (vs : (Var, Subtype)) => {
    let { l, r } = vs.1
    let v = match ty.variance(vs.0) {
      Constant | Covariant => Some(l)
      Contravariant => Some(r)
      Invariant => if l == r { Some(l) } else { None }
    }
    v.map(v => (vs.0, v))
  }
  let i = self.inner().iter().filter_map(f)
  guard i.count() == self.inner().size() else { None }
  Some(Map::from_iter(i))
}

8.7.3. Proof Sketch [blog/lti/proof_eq]

至此,我们已经完整地定义了一个由「变量消去」、「约束生成」和「参数计算」三步构成的、完全可执行的算法。但我们如何确保这个具体的算法,其行为与那个非构造性的、声明式的 App-InfSpec 规约完全一致?

其等价性的证明,浓缩于一个核心命题中,该命题断言:

  1. 若最小代换 $\sigma_{CR}$ 存在,那么它就是规约所要求的那个最优解。
  2. 若最小代换 $\sigma_{CR}$ 不存在,那么规约所要求的最优解也必然不存在。

证明概要:

  • 第一部分(算法的正确性): 为证明 $\sigma_{CR}$ 是最优的,我们任取另一个满足约束的合法代换 $\sigma'$,并需要证明 $\sigma_{CR}(R) \lt: \sigma'(R)$。 考虑构建一个从 $\sigma_{CR}$ 到 $\sigma'$ 的「代换链」,每一步只改变一个变量的值。例如,$\sigma_0 = \sigma_{CR}$,$\sigma_1 = \sigma_0[X_1 \mapsto \sigma'(X_1)]$,…,$\sigma_n = \sigma'$。 接着,我们证明在此路径的每一步中,结果类型都是单调不减的,即 $\sigma_{i-1}(R) \lt: \sigma_i(R)$。这一步的证明,直接依赖于前述的极性定义。例如,若 $R$ 在 $X_i$ 上是协变的,我们的算法选择了下界 $S$,而 $\sigma'(X_i)$ 必然大于等于 $S$,因此根据协变的定义,结果类型必然「变大」。同理可以证明其他情况下该论断也成立。 最终,通过传递性,我们得出 $\sigma_{CR}(R) \lt: \sigma'(R)$,证明了 $\sigma_{CR}$ 的最优性。

  • 第二部分(算法失败的完备性): 当算法失败时,必然是因为某个不变变量 $X_i$ 的约束区间 $[S, T]$ 中 $S \neq T$。 我们采用反证法:假设此时仍然存在一个最优解 $\sigma$。由于 $S \neq T$,我们总能找到另一个合法的代换 $\sigma'$,使得 $\sigma(X_i)$ 与 $\sigma'(X_i)$ 不同。但由于 $R$ 在 $X_i$ 上是不变的,$\sigma(R)$ 与 $\sigma'(R)$ 将变得不可比较,这与「$\sigma$ 是最优解(即比所有其他解都小)」的假设相矛盾。 因此,在这种情况下,最优解必然不存在。

这一核心命题证明了我们设计的这套具体算法与 App-InfSpec 规约之间的等价性。 它允许我们最终用一个完全算法化的规则 App-InfAlg 来取代那个不可执行的规约:

$$ \frac{ \begin{array}{ccc} \Gamma \vdash f : \forall \overline{X}.\overline{T} \to R & \Gamma \vdash \overline{e} : \overline{S} & |\overline{X}| > 0 \\ \emptyset \vdash_X \overline{S} \lt: \overline{T} \Rightarrow \overline{D} & C = \bigwedge \overline{D} & \sigma = \sigma_{CR} \end{array} }{ \Gamma \vdash f(\overline{e}) : \sigma R } \quad (\text{App-InfAlg}) $$

8.8. Bidirectional Checking [blog/lti/bidirectional]

至此,我们已经完整地剖析了本文的第一项重点:局部类型参数合成。它通过一套由「变量消去」、「约束生成」和「参数计算」构成的、逻辑严密且完全可执行的算法,完美地解决了由细粒度多命题所引发的类型参数标注繁琐的问题,达成了引言中所述三条设计准则中的第一条。

然而,我们的工具箱尚不完备。回顾引言中基于 ML 代码分析所提出的三条设计准则,仍有两项亟待解决:

  1. 高阶编程的便利性:如何推断匿名函数(如 fun[](x) x+1)中绑定变量 x 的类型?
  2. 纯函数式风格的支持:如何让大量的局部变量绑定(如 let x = ...)无需显式类型标注?

局部类型参数合成机制,其信息流本质上是自下而上(bottom-up)的,它根据函数和参数的既有类型,向上推导出一个最佳的结果类型。这套机制,对于上述两个问题鞭长莫及,因为在类似 fun[](x) x+1 这样的表达式中,没有任何子结构能为 x 的类型提供信息。

我们考虑一种在思想上与前者互补的、功能强大的局部推断技术。它不再仅仅依赖自下而上的信息综合,而是引入了一股自上而下(top-down)的信息流,让表达式所处的语境(context)来指导其内部的类型检查。这便是双向类型检查(Bidirectional Type Checking),其基本思想虽早已是编程语言社区的「民间共识」,并在一些基于属性文法的 ML 编译器中得以应用,本文将其在一个同时包含子类型化与非直谓多态的形式系统中进行严谨的公理化,并将其作为一种独立的局部推断方法,其威力出人意料地强大。

两种模式:综合与检查

  1. 综合模式 (Synthesis Mode, $\Rightarrow$)

    • 在此模式下,类型信息自下而上传播
    • 其目标是根据一个表达式的子表达式的类型,来计算(或「综合」)出该表达式自身的类型。
    • 这对应于传统的类型检查方式,适用于那些我们对其期望类型一无所知的上下文,例如在处理一个顶层表达式或一个应用节点的函数部分时。
  2. 检查模式 (Checking Mode, $\Leftarrow$)

    • 在此模式下,类型信息自上而下传播
    • 其目标是验证(或「检查」)一个表达式是否拥有一个由其所处语境提供的「期望类型」(或者该期望类型的一个子类型)。
    • 当一个表达式所处的语境已经决定了它的类型时,便可切换至此模式。

双向检查的精髓在于两种模式的灵活切换。一个典型的函数应用 f(e) 完美地展示了这一过程:类型检查器会先综合出函数 f 的类型,然后利用该类型提供的信息,切换模式去检查参数 e

8.8.1. Typing Rules [blog/lti/bidi_rules]

本节是我们类型检查程序的最后一块拼图, 描述了整个双向类型检查的过程。

变量规则 (Variable Rules)

1. 综合 - 变量 (Synthesis-Var)

$$ \frac{}{\Gamma \vdash x \Rightarrow \Gamma(x)} \quad (\text{S-Var}) $$

这是变量的综合规则。如果要在综合模式下推导一个变量 $x$ 的类型,只需在当前的类型上下文 $\Gamma$ 中查找 $x$ 已经声明的类型 $\Gamma(x)$ 即可。这是最直接的类型推导形式:变量的类型就是它被定义时的类型。


2. 检查 - 变量 (Checking-Var)

$$ \frac{\Gamma \vdash \Gamma(x) \lt: T}{\Gamma \vdash x \Leftarrow T} \quad (\text{C-Var}) $$

这是变量的检查规则。要检查变量 $x$ 是否符合预期的类型 $T$,我们需要先从上下文 $\Gamma$ 中查找到 $x$ 的实际类型 $\Gamma(x)$,然后验证这个实际类型 $\Gamma(x)$ 是否是预期类型 $T$ 的一个子类型 (subtype)。这里的子类型关系用 $\Gamma \vdash \Gamma(x) \lt: T$ 表示。


函数抽象规则 (Function Abstraction Rules)

3. 综合 - 抽象 (Synthesis-Abs)

$$ \frac{\Gamma, \overline{X}, \overline{x}:\overline{S} \vdash e \Rightarrow T}{\Gamma \vdash \textbf{fun} [\overline{X}] (\overline{x}:\overline{S}) e \Rightarrow \forall \overline{X}. \overline{S} \rightarrow T} \quad (\text{S-Abs}) $$

这是针对带有完整类型标注的函数抽象综合规则。

  • 一个形式为 fun [X] (x:S) e 的函数,其类型参数 $\overline{X}$ 和值参数 $\overline{x}$ 的类型 $\overline{S}$ 都被明确标注了。
  • 规则的前提是,在将类型变量 $\overline{X}$ 和值变量及其类型 $\overline{x}:\overline{S}$ 加入到当前上下文 $\Gamma$ 后,我们可以综合出函数体 $e$ 的类型为 $T$。
  • 那么,整个函数表达式的类型就可以被综合为多态函数类型 $\forall \overline{X}. \overline{S} \rightarrow T$。

4. 检查 - 无标注抽象 (Checking-Abs-Inf)

$$ \frac{\Gamma, \overline{X}, \overline{x}:\overline{S} \vdash e \Leftarrow T}{\Gamma \vdash \textbf{fun} [\overline{X}] (\overline{x}) e \Leftarrow \forall \overline{X}. \overline{S} \rightarrow T} \quad (\text{C-Abs-Inf}) $$

这是本节的核心规则之一,用于推断无标注匿名函数的参数类型

  • 当我们在检查模式下处理一个没有值参数类型标注的函数 fun [X] (x) e 时,我们可以从预期的函数类型 $\forall \overline{X}. \overline{S} \rightarrow T$ 中获取信息。
  • 具体来说,我们可以从预期的类型中提取出参数类型 $\overline{S}$ 和返回类型 $T$。
  • 然后,我们将类型变量 $\overline{X}$ 和推断出的值参数类型 $\overline{x}:\overline{S}$ 加入上下文,并在这个新上下文中以检查模式验证函数体 $e$ 是否符合返回类型 $T$。如果满足,则整个无标注函数就通过了类型检查。
  • 注意:$\overline{X}$ 在这个系统下是无法省略的。

5. 检查 - 有标注抽象 (Checking-Abs)

$$ \frac{\Gamma, \overline{X} \vdash \overline{T} \lt: \overline{S} \quad \Gamma, \overline{X}, \overline{x}:\overline{S} \vdash e \Leftarrow R}{\Gamma \vdash \textbf{fun} [\overline{X}] (\overline{x}:\overline{S}) e \Leftarrow \forall \overline{X}. \overline{T} \rightarrow R} \quad (\text{C-Abs}) $$

这是在检查模式下处理一个带有类型标注的函数的规则。

  • 当一个有标注的函数 fun [X] (x:S) e 需要被检查是否符合某个预期类型 $\forall \overline{X}. \overline{T} \rightarrow R$ 时:
  • 首先,由于函数类型的参数类型是逆变 (contravariant) 的,我们需要检查预期类型中的参数类型 $\overline{T}$ 是否是函数实际标注的参数类型 $\overline{S}$ 的子类型。
  • 随后我们在扩展后的上下文中,以检查模式验证函数体 $e$ 是否符合预期的返回类型 $R$。

函数应用规则 (Function Application Rules)

6. 综合 - 应用 (Synthesis-App)

$$ \frac{\Gamma \vdash f \Rightarrow \forall \overline{X}. \overline{S} \rightarrow R \quad \Gamma \vdash \overline{e} \Leftarrow [\overline{T}/\overline{X}]\overline{S}}{\Gamma \vdash f [\overline{T}] (\overline{e}) \Rightarrow [\overline{T}/\overline{X}]R} \quad (\text{S-App}) $$

这是函数应用的综合规则。

  • 首先,在综合模式下推断出函数 $f$ 的类型为多态函数 $\forall \overline{X}. \overline{S} \rightarrow R$。
  • 然后,我们将提供的具体类型参数 $\overline{T}$ 替换掉类型变量 $\overline{X}$,得到参数的预期类型 $[\overline{T}/\overline{X}]\overline{S}$。
  • 接下来,我们切换到检查模式,验证实际参数 $\overline{e}$ 是否符合这个预期类型。
  • 如果检查通过,整个应用表达式的类型就被综合为将 $\overline{T}$ 代入后的返回类型 $[\overline{T}/\overline{X}]R$。

7. 检查 - 应用 (Checking-App)

$$ \frac{\Gamma \vdash f \Rightarrow \forall \overline{X}. \overline{S} \rightarrow R \quad \Gamma \vdash [\overline{T}/\overline{X}]R \lt: U \quad \Gamma \vdash \overline{e} \Leftarrow [\overline{T}/\overline{X}]\overline{S}}{\Gamma \vdash f [\overline{T}] (\overline{e}) \Leftarrow U} \quad (\text{C-App}) $$

这是函数应用的检查规则。它与综合规则非常相似,但增加了一个最终的子类型检查。

  • 前两个步骤和 S-App 一样:综合 $f$ 的类型,并检查参数 $\overline{e}$。
  • 在计算出应用的实际返回类型 $[\overline{T}/\overline{X}]R$ 后,我们还必须检查这个实际返回类型是否是整个应用表达式的预期类型 $U$ 的子类型。

结合双向检查和类型参数综合的规则

8. 综合 - 应用 - 推断规格 (Synthesis-App-InfAlg)

$$ \frac{ \begin{array}{ccc} \Gamma \vdash f : \forall \overline{X}.\overline{T} \to R & \Gamma \vdash \overline{e} : \overline{S} & |\overline{X}| > 0 \\ \emptyset \vdash_X \overline{S} \lt: \overline{T} \Rightarrow \overline{D} & C = \bigwedge \overline{D} & \sigma = \sigma_{CR} \end{array} }{ \Gamma \vdash f(\overline{e}) \Rightarrow \sigma R } \quad (\text{S-App-InfAlg}) $$

这是在综合模式下推断函数应用中缺失的类型参数的规则,这正是上文「类型参数计算」一节导出的规则。


9. 检查 - 应用 - 推断规格 (Checking-App-InfAlg)

$$ \frac{\begin{matrix} \Gamma \vdash f \Rightarrow \forall \overline{X}. \overline{T} \rightarrow R \quad \Gamma \vdash \overline{e} \Rightarrow \overline{S} \quad |\overline{X}| \gt 0 \\ \emptyset \vdash \overline{S} \lt: \overline{T} \Rightarrow C \quad \emptyset \vdash R \lt: V \Rightarrow D \quad \sigma \in \bigwedge C \wedge D \end{matrix}}{\Gamma \vdash f(\overline{e}) \Leftarrow V} \quad (\text{C-App-InfAlg}) $$

这是 App-InfAlg 规则的检查版本。

  • 它描述了编译器如何通过约束求解来找到合适的类型参数。
  • 步骤如下:
    1. 综合函数 $f$ 和参数 $\overline{e}$ 的类型。
    2. 生成两组约束:
      • 第一组约束 $C$ 来自于要求参数的实际类型 $\overline{S}$ 必须是函数期望的参数类型 $\overline{T}$ 的子类型。
      • 第二组约束 $D$ 来自于要求函数的实际返回类型 $R$ 必须是整个表达式的预期类型 $V$ 的子类型。
    3. 求解这两组约束的合取($\bigwedge C \wedge D$)。如果能找到一个解(一个替换 $\sigma$),那么类型检查就成功了。 因为这是一条检查规则,因而我们只需要知道解的存在性即可,甚至不需要求解它。

顶类型和底类型

10. 检查 - 顶类型 (Checking-Top)

$$ \frac{\Gamma \vdash e \Rightarrow T}{\Gamma \vdash e \Leftarrow \top} \quad (\text{C-Top}) $$

这是一个从检查模式切换到综合模式的规则。如果一个表达式 $e$ 被要求检查是否符合顶类型 $\top$,由于任何类型都是 $\top$ 的子类型,这个检查总是会成功。$\top$ 类型没有提供任何有用的约束信息,所以规则允许我们直接切换到综合模式,推导出 $e$ 的具体类型 $T$ 即可。


11. 综合 - 应用 - 底类型 (Synthesis-App-Bot)

$$ \frac{\Gamma \vdash f \Rightarrow \bot \quad \Gamma \vdash \overline{e} \Rightarrow \overline{S}}{\Gamma \vdash f [\overline{T}] (\overline{e}) \Rightarrow \bot} \quad (\text{S-App-Bot}) $$

这是处理函数类型为 $\bot$ (底类型) 时的特殊情况。$\bot$ 类型代表那些永不返回的表达式(如抛出异常)。

  • 如果一个函数 $f$ 的类型被推导为 $\bot$,那么无论它被应用于何种参数,整个应用表达式的结果类型也是 $\bot$。
  • 这是因为 $\bot$ 是所有类型的子类型,包括所有函数类型。因此,一个类型为 $\bot$ 的表达式可以被当作任何函数来应用。

12. 检查 - 应用 - 底类型 (Checking-App-Bot)

$$ \frac{\Gamma \vdash f \Rightarrow \bot \quad \Gamma \vdash \overline{e} \Rightarrow \overline{S}}{\Gamma \vdash f [\overline{T}] (\overline{e}) \Leftarrow R} \quad (\text{C-App-Bot}) $$

这是在检查模式下,函数类型为 $\bot$ 的情况。

  • 同样,如果函数 $f$ 的类型为 $\bot$,那么应用的结果类型也是 $\bot$。
  • 因为 $\bot$ 是任何类型 $R$ 的子类型,所以这个检查总是成功的。

最后的实现即是落到 synthesischeck 两个关键函数上, 这是本文最重要的一个练习, 强烈建议读者自己尝试实现这两个函数,来体会双向检查的精妙之处, 并从中学习将类型规则转化为代码的技巧。

8.8.2. Bidirectional Typing Code [blog/lti/bidi_code]

pub fn synthesis(self : Expr, gamma : Context) -> Type raise {
  match self {
    EVar(v) => gamma[v]
    EAbs(xs, vs, body) => {
      let ctx = gamma.append_vars(xs).append_binds(vs)
      let body_ty = body.synthesis(ctx)
      TyFun(xs, vs.map(xS => xS.1), body_ty)
    }
    EAppI(f, e) => {
      let t = f.synthesis(gamma)
      guard !(t is TyBot) else { TyBot }
      guard t is TyFun(xs, t, r) else { raise SynthesisError }
      // guard !xs.is_empty() else { raise NotFound }
      let es = e.map(_.synthesis(gamma))
      let cs = es.zip(t).map(z => { l: z.0, r: z.1 }.generate(xs, Set::new()))
      let sigma = meets(cs).solve(r)
      sigma.map(s => r.apply_subst(s)).or_error(SynthesisError)
    }
    EApp(f, ty, e) => {
      let t = f.synthesis(gamma)
      guard !(t is TyBot) else { TyBot }
      guard t is TyFun(xs, ss, r) else { raise SynthesisError }
      let subst = mk_subst(xs, ty)
      e.zip(ss).each(es => es.0.check(es.1.apply_subst(subst), gamma))
      r.apply_subst(subst)
    }
    _ => raise SynthesisError
  }
}

pub fn check(self : Expr, ty : Type, gamma : Context) -> Unit raise {
  match (self, ty) {
    (_, TyTop) => ()
    (EVar(v), t) => {
      let gx = gamma[v]
      guard gx.subtype(t) else { raise CheckError }
    }
    (EAbs(xs, vs, body), TyFun(xsP, t, r)) if xs == xsP => {
      let ctx = gamma.append_vars(xs)
      guard t.zip(vs.map(xS => xS.1)).iter().all(z => z.0.subtype(z.1)) else {
        raise CheckError
      }
      body.check(r, ctx.append_binds(vs))
    }
    (EAbsI(xs, vs, body), TyFun(xsP, ss, t)) if xs == xsP &&
      ss.length() == vs.length() =>
      body.check(t, gamma.append_vars(xs).append_binds(vs.zip(ss)))
    (EAppI(f, e), u) => {
      let t = f.synthesis(gamma)
      guard !(t is TyBot && u is TyBot) else { () }
      guard f.synthesis(gamma) is TyFun(xs, t, r) else { raise CheckError }
      guard !xs.is_empty() else { () }
      let es = e.map(_.synthesis(gamma))
      let cs = es.zip(t).map(z => { l: z.0, r: z.1 }.generate(xs, Set::new()))
      let d = { l: r, r: u }.generate(xs, Set::new())
      guard meets(cs).meet(d).satisfiable() else { raise CheckError }
    }
    (EApp(f, ty, e), u) => {
      let t = f.synthesis(gamma)
      guard !(t is TyBot && u is TyBot) else { () }
      guard t is TyFun(xs, ss, r)
      let subst = mk_subst(xs, ty)
      e.zip(ss).each(es => es.0.check(es.1.apply_subst(subst), gamma))
      guard r.apply_subst(subst).subtype(u) else { raise CheckError }
    }
    _ => raise CheckError
  }
}

最后一个关键目标是局部变量绑定的设计, 这要求我们引入新的语法结构 ELet,但其规则是显然的:

$$ \frac{\Gamma \vdash e \Rightarrow S \quad \Gamma, x:S \vdash b \Rightarrow T}{\Gamma \vdash \textbf{let } x = e \textbf{ in } b \Rightarrow T} \quad (\text{S-Let}) $$

$$ \frac{\Gamma \vdash e \Rightarrow S \quad \Gamma, x:S \vdash b \Leftarrow T}{\Gamma \vdash \textbf{let } x = e \textbf{ in } b \Leftarrow T} \quad (\text{C-Let}) $$

实现留作习题。

8.9. Conclusion and Future [blog/lti/conclusion]

至此,我们循着 Pierce 与 Turner 的足迹,完整地剖析了一套精巧而强大的局部类型推断机制。 通过将局部类型参数合成双向类型检查这两项核心技术相结合, 我们最终完成了一个真正强大的类型检查器的设计。 它不仅能在理论上驾驭如 System $F_{\le}$ 这样兼具子类型化与非直谓多态的强大类型系统, 更在实践中,精准地解决了由多态、 高阶编程与纯函数式风格所引发的最为普遍和恼人的类型标注问题。 这套完全基于「局部性」原则的算法,其行为可预测、 易于实现且错误提示友好,堪称是连接艰深理论与日常编程实践的一座典范之桥。

当然,本文所探讨的,仅是这篇经典论文的核心部分。原文的疆域更为广阔, 其中最重要的扩展,便是对有界量化(Bounded Quantification)的支持。 有界量化,即形如 $\forall (X \lt: T_2, Y \lt: T_2, \cdots) . e$ 的多态, 它允许类型参数本身受到其超类型的约束。这一特性对于精确建模面向对象语言中的继承等高级特性至关重要,是通往更强大表达能力的必由之路。 原文第五章详细阐述了如何将本文介绍的局部推断技术扩展至支持有界量化的系统。该扩展使得算法,尤其是约束的生成与求解,将变得更为精妙和复杂, 特别是在处理 $\bot$ 类型与类型边界的相互作用时, 引入了新的挑战。限于篇幅,对这一部分的深入剖析,或许只能留待未来的文章再行探讨。 此外,本文的另一大遗憾是「形式证明」的缺失。我们关注的重点,在于阐明算法的设计动机与直觉, 并以一种接近实际代码实现的方式来呈现其逻辑。为此,我们省略了诸多严谨的数学证明细节, 例如约束生成算法的可靠性与完备性证明,仅以提要的形式一笔带过。

最后,值得一提的是,本文对类型系统代数性质的倚重——例如,确保任意类型间的最小上界(join)与最大下界(meet)总是存在——揭示了一条深刻的设计原则:一个具有良好代数结构的类型系统,往往更能催生出简洁而强大的类型推断算法。自这篇论文发表以来,寻求更优美的子类型化代数理论的探索从未停止。后续的研究,如 Stephen Dolan 等人提出的「代数子类型」(Algebraic Subtyping), 正是沿着这一思想路径,对子类型关系的形式化进行了更为深刻的抽象与简化, 在笔者看来,它是真正改变子类型研究的天才之作。 当然,对这些更前沿工作的介绍,已然超出了对这篇 2000 年经典论文本身进行解读的范畴, 我们把它留给未来的文章。