elab API 参考

elab 包（src/elab，导入路径 Luna-Flow/stella/elab）是 stella 的内核：包含依值类型论的语法、将语法求值为值、将值读回为范式，以及一个双向类型检查器。其接口文件为 src/elab/pkg.generated.mbti。

项使用德布鲁因索引：Bound(0) 是由最近的外层绑定子绑定的变量。绑定子只有 Lam，以及 Pi、Sigma 和 W 的第二个参数。完整的类型规则见设计说明。

本页中的示例是某个包中的测试，该包的 moon.pkg 如下：

import {
  "Luna-Flow/stella/elab",
  "moonbitlang/core/list",
}

并通过以下方式将类型引入作用域：

using @elab {type TermChk, type TermInf, type Value}

语法

`Name`

Name 标识一个自由变量。

pub(all) enum Name {
  Global(String)
  Local(Int)
  Quote(Int)
} derive(Eq, @debug.Debug)
pub fn Name::equal(Self, Self) -> Bool

构造子	含义
`Global(name)`	由用户在类型上下文中声明的常量，例如一个公设的类型 `A`。
`Local(level)`	类型检查器进入绑定子时引入的变量；`level` 从外向内计数绑定子，从 0 开始。
`Quote(level)`	`quote` 读回函数体时引入的变量；`quote` 会将其还原为 `Bound` 索引。

用户代码通常只创建 Global 名字。Name::equal 是提升后的 Eq 方法；请优先使用 ==。

`TermInf`

TermInf 是检查器能够推断其类型的项的类型。

pub(all) enum TermInf {
  Bound(Int)
  Free(Name)
  UnitType
  Universe(Int)
  Ann(TermChk, TermChk)
  Pi(TermChk, TermChk)
  App(TermInf, TermChk)
  Sigma(TermChk, TermChk)
  Fst(TermInf)
  Snd(TermInf)
  Id(TermChk, TermChk, TermChk)
  JElim(TermChk, TermChk, TermChk, TermChk, TermChk, TermInf)
  W(TermChk, TermChk)
  WRec(TermChk, TermChk, TermChk, TermChk, TermInf)
} derive(Eq, @debug.Debug)
pub fn TermInf::equal(Self, Self) -> Bool

构造子	记法	含义
`Bound(i)`	$\#i$	由第 $i$ 个外层绑定子绑定的变量，从 0 开始计数。
`Free(x)`	$x$	自由变量，在类型上下文中查找。
`UnitType`	$\mathbf 1$	单位类型。
`Universe(i)`	$\mathcal U_i$	层级为 $i \ge 0$ 的宇宙。
`Ann(t, T)`	$(t : T)$	以类型 `T` 标注的可检查项 `t`。
`Pi(A, B)`	$\Pi_{x : A} B$	依值函数类型；`B` 位于一个绑定子之下。
`App(f, t)`	$f\,t$	函数应用。
`Sigma(A, B)`	$\Sigma_{x : A} B$	依值对类型；`B` 位于一个绑定子之下。
`Fst(p)`, `Snd(p)`	$\pi_1\,p$ , $\pi_2\,p$	对的投影。
`Id(A, x, y)`	$\mathrm{Id}_A(x, y)$	恒等类型。
`JElim(A, x, P, d, y, p)`	$J$	基于点的路径消去子：由 `d : P x (refl x)` 和 `p : Id(A, x, y)` 得到 `P y p` 的一个项。`P` 是类型为 $\Pi_{y : A} \mathrm{Id}_A(x, y) \to \mathcal U_k$ 的函数项。
`W(A, B)`	$W_{x : A} B$	良基树类型；`B` 位于一个绑定子之下。
`WRec(A, B, P, s, w)`	$\mathrm{wrec}$	对 `w : W(A, B)` 进行递归，目标为动机 `P`。与 `W` 中不同，这里的 `B` 是类型为 $A \to \mathcal U_k$ 的函数项。

TermInf::equal 按结构比较项，由于变量是德布鲁因索引，这正是 $\alpha$ -等价；请优先使用 ==。

`TermChk`

TermChk 是检查器对照已知类型进行检查的项的类型。

pub(all) enum TermChk {
  Inf(TermInf)
  UnitElement
  Lam(TermChk)
  Pair(TermChk, TermChk)
  Rfl(TermChk)
  Sup(TermChk, TermChk)
} derive(Eq, @debug.Debug)
pub fn TermChk::equal(Self, Self) -> Bool

构造子	记法	含义
`Inf(e)`	$e$	在需要可检查项的位置使用的可推断项。
`UnitElement`	$\star$	单位类型的元素。
`Lam(t)`	$\lambda.\,t$	函数抽象；`t` 位于一个绑定子之下。定义域不需写出，它来自期望类型。
`Pair(t, u)`	$(t, u)$	依值对。
`Rfl(t)`	$\mathrm{refl}\,t$	$\mathrm{Id}_A(t, t)$ 的自反性证明。
`Sup(a, f)`	$\sup(a, f)$	W 类型的节点，标签为 `a`，子节点函数为 `f`。

类型写作 TermChk，但大多数类型规则会推断类型的类型，因此类型位置必须包含 Inf(...)，例如 Inf(UnitType)。

test "syntax" {
  // the identity on the unit type, (λx. x) : 1 → 1
  let id_unit = TermInf::Ann(Lam(Inf(Bound(0))), Inf(Pi(Inf(UnitType), Inf(UnitType))))
  assert_true(id_unit == Ann(Lam(Inf(Bound(0))), Inf(Pi(Inf(UnitType), Inf(UnitType)))))
  debug_inspect(
    id_unit,
    content="Ann(Lam(Inf(Bound(0))), Inf(Pi(Inf(UnitType), Inf(UnitType))))",
  )
}

值

`Value`

Value 是语义域：求值到弱头范式的项，其中绑定子表示为 MoonBit 函数。

#alias(Type)
pub(all) enum Value {
  VNeutral(Neutral)
  VUnitType
  VUnitElement
  VUniverse(Int)
  VLam((Value) -> Value)
  VPi(Value, (Value) -> Value)
  VSigma(Value, (Value) -> Value)
  VPair(Value, Value)
  VId(Value, Value, Value)
  VRfl(Value)
  VW(Value, (Value) -> Value)
  VSup(Value, (Value) -> Value)
} derive(@debug.Debug)

每个构造子对应一个项构造子。绑定子的体变成函数 (Value) -> Value：VPi(a, b) 即 $\Pi_{x : a} b(x)$ ，VLam(f) 即函数 $x \mapsto f(x)$ 。值也被用作类型，Type 是 Value 的别名，包在这一角色中使用它。由于值包含函数，Value 没有 Eq；请用 def_eq 比较值，或比较它们经 quote 得到的范式。Debug 将函数打印为 <function: ...>。

`Neutral`

Neutral 是卡在自由变量上的计算。

pub(all) enum Neutral {
  NFree(Name)
  NApp(Neutral, Value)
  NFst(Neutral)
  NSnd(Neutral)
  NJElim(Value, Value, Value, Value, Value, Neutral)
  NWRec(Value, (Value) -> Value, Value, Value, Neutral)
} derive(@debug.Debug)

中性项是一个自由变量后跟一串无法归约的消去：变量的应用、变量的投影，或作用于变量的 J 或 wrec。中性项通过 VNeutral 成为值。

`Context`, `Env`

Context 为自由变量指定类型；Env 为约束变量指定值。

pub type Context = @list.List[(Name, Value)]
pub type Env = @list.List[Value]

Context 从头部开始查找，因此后面的声明会遮蔽前面的声明。在 Env 中，头部是 Bound(0) 的值，下一个元素是 Bound(1) 的值，依此类推。

求值

`eval_inf`, `eval_chk`

eval_inf 和 eval_chk 在环境中对项求值。

pub fn eval_inf(TermInf, @list.List[Value]) -> Value
pub fn eval_chk(TermChk, @list.List[Value]) -> Value

它们计算弱头范式，即设计说明中的 $\llbracket t \rrbracket_\rho$ ：标注被擦除，绑定子变成捕获环境的闭包，消去通过下面的 val_ 函数归约。求值不做类型检查。对于类型错误的项，它可能 panic，例如对非函数进行应用，或 Bound(i) 在环境中没有对应条目时。

test "evaluate" {
  let id_unit = TermInf::Ann(Lam(Inf(Bound(0))), Inf(Pi(Inf(UnitType), Inf(UnitType))))
  let v = @elab.eval_inf(App(id_unit, UnitElement), @list.empty())
  debug_inspect(v, content="VUnitElement")
}

`val_var`

val_var 是自由变量的值。

pub fn val_var(Name) -> Value

val_var(x) 即 VNeutral(NFree(x))。

`val_app`, `val_fst`, `val_snd`

这些函数应用函数值并投影对值。

pub fn val_app(Value, Value) -> Value
pub fn val_fst(Value) -> Value
pub fn val_snd(Value) -> Value

它们实现 $\beta$ 规则 $(\lambda f)\,v = f(v)$ 、 $\pi_1 (v, w) = v$ 和 $\pi_2 (v, w) = w$ 。对中性参数，它们扩展中性序列；对其他任何值则 panic。

`val_j_elim`

val_j_elim 对路径消去子求值。

pub fn val_j_elim(Value, Value, Value, Value, Value, Value) -> Value

val_j_elim(a, x, p, d, y, e) 在 e 为 VRfl(_) 时返回 d（即规则 $J(A, x, P, d, x, \mathrm{refl}\,x) = d$ ），在 e 为中性时扩展中性序列，其他情况下 panic。

`val_w_rec`

val_w_rec 对 W 递归求值。

pub fn val_w_rec(Value, (Value) -> Value, Value, Value, Value) -> Value

对于 w = VSup(l, f)，val_w_rec(a, b, p, s, w) 计算

\mathrm{wrec}(\sup(l, f)) = s\; l\; (\lambda z.\, f\,z)\; \bigl(\lambda z.\, \mathrm{wrec}(f\,z)\bigr),

即将步进函数应用于标签、子节点以及对子节点的递归结果。当 w 为中性时扩展中性序列，其他情况下 panic。

`val_max_univ`

val_max_univ 返回两个宇宙中较大的一个。

pub fn val_max_univ(Value, Value) -> Value

val_max_univ(VUniverse(i), VUniverse(j)) 即 VUniverse(max(i, j))。任何其他参数都会 panic。检查器用这条规则计算 $\Pi$ 、 $\Sigma$ 或 $W$ 类型的层级，但并不调用该函数。

范式

`quote`, `neutral_quote`

quote 将值读回为范式项；neutral_quote 对中性项做同样的事。

pub fn quote(Int, Value) -> TermChk
pub fn neutral_quote(Int, Neutral) -> TermInf

quote(l, v) 要求 l 为值所处的绑定子个数，通常为 0。为读回闭包，它将闭包应用于新变量 Quote(l)，并在 l + 1 处读回函数体。neutral_quote 将变量 Quote(k) 转为索引 Bound(l - k - 1)，其他名字保留为 Free(x)。项 $t$ 的范式是 quote(0, eval_chk(t, @list.empty()))；范式相等的两个项是 $\beta$ -相等的。

test "normalise under a binder" {
  let id_unit = TermInf::Ann(Lam(Inf(Bound(0))), Inf(Pi(Inf(UnitType), Inf(UnitType))))
  // λy. (λx. x) y  normalises to  λy. y
  let t = TermChk::Lam(Inf(App(id_unit, Inf(Bound(0)))))
  debug_inspect(@elab.quote(0, @elab.eval_chk(t, @list.empty())), content="Lam(Inf(Bound(0)))")
}

类型检查

`TypeError`

TypeError 是类型检查器抛出的错误。

pub suberror TypeError {
  TypeError(String)
}

消息会指出失败的规则，例如 Illegal Application、Expected Pi type for Lambda、Type Mismatch: inferred type is not a subtype of expected type、Rfl endpoints mismatch 或 Unknown Identifier: Global("b")。

`type_inf`, `type_chk`

type_inf 推断项的类型；type_chk 对照类型检查项。

pub fn type_inf(Int, @list.List[(Name, Value)], @list.List[Value], TermInf) -> Value raise TypeError
pub fn type_chk(Int, @list.List[(Name, Value)], @list.List[Value], TermChk, Value) -> Unit raise TypeError

type_inf(l, ctx, env, e) 以值的形式返回 e 的类型；当 t 的类型为 ty 时，type_chk(l, ctx, env, t, ty) 正常返回；否则两者都抛出 TypeError。这些参数描述项所处的位置：

l 是检查器已进入的绑定子个数，Local(l) 是下一个新变量；
ctx 包含用户的 Global 声明，并为每个已进入的绑定子包含一个条目 (Local(k), A_k)；
env 为每个已进入的绑定子包含一个条目 val_var(Local(k))，最内层的在前。

在顶层，传入 0、用户的上下文和空环境。Bound(i) 先通过 env 再通过 ctx 解析，因此 env 只能包含在 ctx 中声明过的变量；其他任何值都会引发内部错误。在检查模式下，只能推断的项在其推断类型是期望类型的子类型时被接受（累积性，参见 def_eq）。

test "check and infer" {
  let poly_id_ty = TermChk::Inf(Pi(Inf(Universe(0)), Inf(Pi(Inf(Bound(0)), Inf(Bound(1))))))
  let poly_id = TermInf::Ann(Lam(Lam(Inf(Bound(0)))), poly_id_ty)
  let ty = @elab.type_inf(0, @list.empty(), @list.empty(), poly_id)
  debug_inspect(@elab.quote(0, ty), content="Inf(Pi(Inf(Universe(0)), Inf(Pi(Inf(Bound(0)), Inf(Bound(1))))))")
  @elab.type_chk(0, @list.empty(), @list.empty(), Inf(UnitType), VUniverse(1))
}

`type_inf_0`

type_inf_0 在由全局声明组成的上下文中推断闭项的类型。

pub fn type_inf_0(@list.List[(Name, Value)], TermInf) -> Value raise TypeError

type_inf_0(ctx, e) 即 type_inf(0, ctx, @list.empty(), e)。通过向 ctx 添加 (Global(name), type) 来声明常量；类型是一个值，例如类型变量用 VUniverse(0)，已声明类型 A 的元素用 VNeutral(NFree(Global("A")))。

test "global declarations" {
  let ctx : @elab.Context = @list.List([
    (Global("a"), VNeutral(NFree(Global("A")))),
    (Global("A"), VUniverse(0)),
  ])
  let ty = @elab.type_inf_0(ctx, Free(Global("a")))
  debug_inspect(@elab.quote(0, ty), content="Inf(Free(Global(\"A\")))")
  let err = try @elab.type_inf_0(ctx, App(Free(Global("a")), UnitElement)) |> ignore catch {
    TypeError(msg) => msg
  } noraise {
    _ => "no error"
  }
  inspect(err, content="Illegal Application")
}

`def_eq`

def_eq 判定在空上下文中一个类型是否为另一个类型的子类型。

pub fn def_eq(Int, Value, Value) -> Bool

当 $s \le t$ 在设计说明中的累积子类型关系下成立时，def_eq(l, s, t) 返回 true：对 $i \le j$ 有 $\mathcal U_i \le \mathcal U_j$ ， $\Pi$ 类型在定义域上逆变、在陪域上协变， $\Sigma$ 类型在第一分量上不变、在第二分量上协变，其他所有类型按转换（conversion）比较。尽管名字如此，该关系并不对称：def_eq(0, VUniverse(0), VUniverse(1)) 为 true，而 def_eq(0, VUniverse(1), VUniverse(0)) 为 false。

test "cumulativity" {
  assert_true(@elab.def_eq(0, VUniverse(0), VUniverse(1)))
  assert_false(@elab.def_eq(0, VUniverse(1), VUniverse(0)))
  let narrow = Value::VPi(VUniverse(0), _ => VUniverse(0))
  let wide = Value::VPi(VUniverse(1), _ => VUniverse(0))
  assert_true(@elab.def_eq(0, wide, narrow))
}

已弃用

下列提升方法为保持源码兼容而保留。它们不出现在接口文件中，从其他包调用时会产生警告。

方法	替代
`Name::not_equal`, `TermChk::not_equal`, `TermInf::not_equal`	`a != b`
`Name::to_repr`, `TermChk::to_repr`, `TermInf::to_repr`, `Neutral::to_repr`, `Value::to_repr`	`Repr(x)`、`@debug.to_string(x)` 或 `debug_inspect(x)`

在迁移到 MoonBit 0.10 之前，Name、TermChk、TermInf、Neutral 和 Value 实现了 Show。这些实现已被移除：对这些类型，inspect(x)、x.to_string() 和 "\{x}" 不再能通过编译。请改用 Debug 形式。

elab API 参考

语法

Name

TermInf

TermChk

值

Value

Neutral

Context, Env

求值

eval_inf, eval_chk

val_var

val_app, val_fst, val_snd

val_j_elim

val_w_rec

val_max_univ

范式

quote, neutral_quote