elab 教程
本教程介绍如何将 stella 类型论的项写成 MoonBit 值、向内核询问它们的类型、对照你给出的类型检查它们，以及计算它们的范式。教程从恒等函数开始，以一个路径归纳证明结束。每一步背后的类型规则见设计说明。
快速开始
将模块添加到你的项目：
moon add Luna-Flow/stella@0.1.2在 moon.pkg 中导入该包以及提供上下文和环境的 list 包：
import {
"Luna-Flow/stella/elab",
"moonbitlang/core/list",
}最小的有用程序对单位类型上的恒等函数做类型检查并应用它：
using @elab {type TermChk, type TermInf}
test "quick start" {
// (λx. x : 1 → 1)
let id_unit = TermInf::Ann(Lam(Inf(Bound(0))), Inf(Pi(Inf(UnitType), Inf(UnitType))))
let ty = @elab.type_inf_0(@list.empty(), id_unit)
debug_inspect(@elab.quote(0, ty), content="Inf(Pi(Inf(UnitType), Inf(UnitType)))")
let v = @elab.eval_inf(App(id_unit, UnitElement), @list.empty())
debug_inspect(@elab.quote(0, v), content="UnitElement")
}这里出现了三个要点。函数 Lam 没有定义域标注，因此内核无法推断其类型；Ann 提供了类型。type_inf_0 以值的形式返回类型，quote(0, _) 将值转回可打印的项。eval_inf 进行计算，应用归约为 UnitElement。
日常任务
读写德布鲁因索引
变量是数字：Bound(0) 是最近外层绑定子的变量，Bound(1) 是再外一层的，依此类推。绑定子是 Lam 以及 Pi、Sigma 和 W 的第二个参数。多态恒等函数 写法如下：
fn poly_id() -> TermInf {
// Π(A : U0). Π(x : A). A — inside the inner Π, A is Bound(1)
let ty = TermChk::Inf(Pi(Inf(Universe(0)), Inf(Pi(Inf(Bound(0)), Inf(Bound(1))))))
Ann(Lam(Lam(Inf(Bound(0)))), ty)
}
test "polymorphic identity" {
let ty = @elab.type_inf_0(@list.empty(), poly_id())
debug_inspect(
@elab.quote(0, ty),
content="Inf(Pi(Inf(Universe(0)), Inf(Pi(Inf(Bound(0)), Inf(Bound(1))))))",
)
// instantiate A := 1 and apply to ⋆
let app = TermInf::App(App(poly_id(), Inf(UnitType)), UnitElement)
debug_inspect(@elab.quote(0, @elab.type_inf_0(@list.empty(), app)), content="Inf(UnitType)")
debug_inspect(@elab.quote(0, @elab.eval_inf(app, @list.empty())), content="UnitElement")
}在类型中，内层 的定义域是 Bound(0)，即外层 绑定的 ；其陪域又多处于一个绑定子之下，因此同一个 在那里是 Bound(1)。应用的类型通过代换计算：内核将陪域闭包应用于参数的值。
在上下文中声明常量
上下文列出名为 Global(...) 的自由变量的类型。用它来公设一个类型及其一个元素：
fn ctx_a() -> @elab.Context {
// A : U0, a : A (the head of the list is searched first)
@list.List([(Global("a"), VNeutral(NFree(Global("A")))), (Global("A"), VUniverse(0))])
}
test "constants" {
let ty = @elab.type_inf_0(ctx_a(), Free(Global("a")))
debug_inspect(@elab.quote(0, ty), content="Inf(Free(Global(\"A\")))")
}a 的类型是项 A 的值，即中性变量 VNeutral(NFree(Global("A")))。
使用对
对是对照 类型检查的，投影则从中推断各自的类型：
test "pairs" {
let ty_a = TermChk::Inf(Free(Global("A")))
let a = TermChk::Inf(Free(Global("a")))
// (a, ⋆) : Σ(x : A). 1
let pair = TermInf::Ann(Pair(a, UnitElement), Inf(Sigma(ty_a, Inf(UnitType))))
debug_inspect(@elab.quote(0, @elab.type_inf_0(ctx_a(), Fst(pair))), content="Inf(Free(Global(\"A\")))")
debug_inspect(@elab.quote(0, @elab.type_inf_0(ctx_a(), Snd(pair))), content="Inf(UnitType)")
debug_inspect(@elab.quote(0, @elab.eval_inf(Fst(pair), @list.empty())), content="Inf(Free(Global(\"a\")))")
}处理类型错误
检查器抛出 TypeError，其消息指出失败的规则。像捕获任何 MoonBit 错误一样捕获它：
fn infer_or_message(ctx : @elab.Context, e : TermInf) -> String {
try @elab.type_inf_0(ctx, e) catch {
TypeError(msg) => msg
} noraise {
ty => "type: \{Repr(@elab.quote(0, ty))}"
}
}
test "errors" {
inspect(infer_or_message(ctx_a(), App(Free(Global("a")), UnitElement)), content="Illegal Application")
inspect(infer_or_message(ctx_a(), Free(Global("b"))), content="Unknown Identifier: Global(\"b\")")
inspect(infer_or_message(ctx_a(), Universe(0)), content="type: Inf(Universe(1))")
}使用宇宙与累积性
Universe(i) 的类型是 Universe(i + 1)， 中的类型在每个更大的宇宙中也被接受：
test "universes" {
debug_inspect(@elab.type_inf_0(@list.empty(), Universe(0)), content="VUniverse(1)")
// 1 : U0, and therefore also 1 : U1
@elab.type_chk(0, @list.empty(), @list.empty(), Inf(UnitType), VUniverse(1))
// a function type lives in the larger universe of its parts
debug_inspect(
@elab.type_inf_0(@list.empty(), Pi(Inf(UnitType), Inf(Universe(0)))),
content="VUniverse(1)",
)
assert_true(@elab.def_eq(0, VUniverse(0), VUniverse(1)))
assert_false(@elab.def_eq(0, VUniverse(1), VUniverse(0)))
}def_eq 是检查器所用的子类型测试，而不是对称的相等关系。
深入
用路径归纳证明命题
消去子 JElim(A, x, P, d, y, p) 将 P x (refl x) 的证明 d 和路径 p : Id(A, x, y) 转为 P y p 的证明。动机 P 必须是可推断的函数，因此要对其标注。这里动机是常函数 ， 沿 refl a 传输 a：
test "path induction" {
let ty_a = TermChk::Inf(Free(Global("A")))
let a = TermChk::Inf(Free(Global("a")))
// P : Π(y : A). Id(A, a, y) → U0, P = λy. λp. A
let motive_ty = TermChk::Inf(
Pi(ty_a, Inf(Pi(Inf(Id(ty_a, a, Inf(Bound(0)))), Inf(Universe(0))))),
)
let motive = TermChk::Inf(Ann(Lam(Lam(ty_a)), motive_ty))
let path = TermInf::Ann(Rfl(a), Inf(Id(ty_a, a, a)))
let j = TermInf::JElim(ty_a, a, motive, a, a, path)
debug_inspect(@elab.quote(0, @elab.type_inf_0(ctx_a(), j)), content="Inf(Free(Global(\"A\")))")
// J computes on refl: J(A, a, P, d, a, refl a) = d
debug_inspect(@elab.quote(0, @elab.eval_inf(j, @list.empty())), content="Inf(Free(Global(\"a\")))")
}归一化项并比较
项的范式是其值的读回。归一化会在绑定子之下归约，因此它能判定项的 -相等：
fn normal_form(t : TermChk) -> TermChk {
@elab.quote(0, @elab.eval_chk(t, @list.empty()))
}
test "normal forms" {
let id_unit = TermInf::Ann(Lam(Inf(Bound(0))), Inf(Pi(Inf(UnitType), Inf(UnitType))))
// λy. (λx. x) y and λy. y have the same normal form
let t1 = TermChk::Lam(Inf(App(id_unit, Inf(Bound(0)))))
let t2 = TermChk::Lam(Inf(Bound(0)))
assert_true(normal_form(t1) == normal_form(t2))
}比较使用 TermChk 派生的 Eq，由于名字是索引，它就是 -等价。
自己在绑定子之下检查
type_inf_0 处理闭项。要检查含有自由 Bound 变量的项，请以检查器在这些绑定子之下会具有的状态调用 type_inf 或 type_chk：层级，以及每个绑定子一个上下文条目 (Local(k), type) 和一个环境条目 val_var(Local(k))，最内层的在前。
test "under a binder" {
// under x : 1, the term x has type 1
let ctx : @elab.Context = @list.List([(Local(0), VUnitType)])
let env : @elab.Env = @list.List([@elab.val_var(Local(0))])
debug_inspect(@elab.type_inf(1, ctx, env, Bound(0)), content="VUnitType")
}常见陷阱
- 类型位置必须可推断。 类型是
TermChk，但形成规则会推断类型所在的宇宙，因此凡是需要类型的地方都写Inf(UnitType)，而不是裸的Lam或Pair。 - 函数需要标注才能被推断。
Lam(...)只能被检查。用Ann(lam, Inf(Pi(...)))包裹它，才能在应用中或作为动机使用。 W和WRec对族的写法不同。 在W(A, B)中，B是绑定子之下的体；在WRec(A, B, ...)中，B是类型为 的可推断函数项。def_eq有方向且不依赖上下文。 它测试的是子类型；并且由于不知道f的类型，它按读回结果比较f x这样的中性应用，不会对参数使用 。- 求值信任其输入。
eval_inf和val_函数在类型错误的项上会 panic；请先做类型检查。 - 用
Debug打印。 内核类型派生的是Debug而非Show：请使用debug_inspect、Repr(x)或@debug.to_string(x)。闭包会打印为<function: ...>，因此打印值之前先对其 quote。