stlc 教程

本教程对简单类型 lambda 项做类型检查、解释类型错误、对良类型项做范式化，并判定两个项在 beta 和 eta 意义下是否相等。项使用共享的 @syntax.Term[@stlc.Atom]，因此你从 syntax 学到的一切都适用。

快速入门

moon add Luna-Flow/type_theory@0.2.0

import {
  "Luna-Flow/type_theory/core",
  "Luna-Flow/type_theory/syntax",
  "Luna-Flow/type_theory/rewrite",
  "Luna-Flow/type_theory/stlc",
}

用 $A \to A$ 检查恒等函数：

test "quick start: λx. x : A → A" {
  let x = @core.Name::new("x")
  let a = @stlc.Ty::Base(@core.Name::new("A"))
  let id : @stlc.Term = Bind(x, Variable(x))
  let result = @stlc.check(
    @stlc.Signature::empty(),
    @stlc.TypeContext::empty(),
    id,
    @stlc.Ty::Arrow(a, a),
  )
  assert_eq(result, Ok(()))
}

日常任务

以下辅助函数让示例保持简短：

fn sn(s : String) -> @core.Name {
  @core.Name::new(s)
}

fn base(s : String) -> @stlc.Ty {
  @stlc.Ty::Base(sn(s))
}

fn arrow(a : @stlc.Ty, b : @stlc.Ty) -> @stlc.Ty {
  @stlc.Ty::Arrow(a, b)
}

fn tv(s : String) -> @stlc.Term {
  @syntax.Term::Variable(sn(s))
}

fn tc(s : String) -> @stlc.Term {
  @syntax.Term::Value(@stlc.Atom::Const(sn(s)))
}

fn tlam(s : String, body : @stlc.Term) -> @stlc.Term {
  @syntax.Term::Bind(sn(s), body)
}

fn tapp(f : @stlc.Term, args : Array[@stlc.Term]) -> @stlc.Term {
  @syntax.Term::Apply(f, args)
}

声明常量和变量

Signature 为语言中的常量指定类型，TypeContext 为被检查项的自由变量指定类型。这样应用的类型就可以推断出来：

test "infer the type of an application" {
  let nat = base("Nat")
  let sig = @stlc.Signature::empty()
    .extend_with(sn("zero"), nat)
    .extend_with(sn("succ"), arrow(nat, nat))
  let ctx = @stlc.TypeContext::empty().extend_with(sn("n"), nat)
  let term = tapp(tc("succ"), [tapp(tc("succ"), [tv("n")])])
  assert_eq(@stlc.infer(sig, ctx, term), Ok(nat))
}

解释类型错误

每次拒绝都是一个 TypeError 值，你可以对它做模式匹配并报告：

fn explain(e : @stlc.TypeError) -> String {
  match e {
    UnboundVariable(x) => "unbound variable \{x.text()}"
    UnknownConstant(c) => "unknown constant \{c.text()}"
    CannotInferLambda => "a lambda needs an expected type"
    ExpectedFunction(_) => "applying a non-function"
    TypeMismatch(..) => "type mismatch"
    EmptyApplication => "application without arguments"
    ScopeError(_) | NormalizationError(..) => "internal error"
  }
}

test "report errors" {
  let sig = @stlc.Signature::empty().extend_with(sn("zero"), base("Nat"))
  let ctx = @stlc.TypeContext::empty()
  let errors = [
    @stlc.infer(sig, ctx, tv("y")),
    @stlc.infer(sig, ctx, tlam("x", tv("x"))),
    @stlc.infer(sig, ctx, tapp(tc("zero"), [tc("zero")])),
  ].map(r => match r {
    Ok(_) => "ok"
    Err(e) => explain(e)
  })
  inspect(
    errors.join("; "),
    content="unbound variable y; a lambda needs an expected type; applying a non-function",
  )
}

用类型检查函数

lambda 是被检查的，而不是被推断的：给出期望类型，检查器会把它推入函数体。

test "check a higher-order function" {
  let a = base("A")
  let b = base("B")
  // twice = λf. λx. f (f x) : (A → A) → A → A
  let twice = tlam("f", tlam("x", tapp(tv("f"), [tapp(tv("f"), [tv("x")])])))
  let empty_sig = @stlc.Signature::empty()
  let empty_ctx = @stlc.TypeContext::empty()
  assert_eq(@stlc.check(empty_sig, empty_ctx, twice, arrow(arrow(a, a), arrow(a, a))), Ok(()))
  assert_true(
    @stlc.check(empty_sig, empty_ctx, twice, arrow(arrow(a, b), arrow(a, b))) is Err(TypeMismatch(..)),
  )
}

范式化良类型项

normalize_eta_long 返回规范形式：beta 范式，且每个函数类型的子项都写成 lambda。

test "normalize to eta-long form" {
  let a = base("A")
  let sig = @stlc.Signature::empty().extend_with(sn("g"), arrow(a, arrow(a, a)))
  let ctx = @stlc.TypeContext::empty()
  // (λh. h) g  normalizes to  λx. λx_1. g x x_1
  let term = tapp(tlam("h", tv("h")), [tc("g")])
  let expected = tlam("p", tlam("q", tapp(tapp(tc("g"), [tv("p")]), [tv("q")])))
  match @stlc.normalize_eta_long(sig, ctx, term, arrow(a, arrow(a, a))) {
    Ok(normal) => assert_true(@syntax.alpha_equal(normal, expected))
    Err(_) => fail("well typed")
  }
}

可约式 $(\lambda h.\,h)\,g$ 的类型通过给 h 赋予 g 的类型来推断。

判定 beta-eta 相等

两个同类型的良类型项 $\beta\eta$ -相等，当且仅当它们的 η-长形式范式 α-等价：

fn beta_eta_equal(
  sig : @stlc.Signature,
  ctx : @stlc.TypeContext,
  ty : @stlc.Ty,
  s : @stlc.Term,
  t : @stlc.Term,
) -> Bool {
  match (@stlc.normalize_eta_long(sig, ctx, s, ty), @stlc.normalize_eta_long(sig, ctx, t, ty)) {
    (Ok(ns), Ok(nt)) => @syntax.alpha_equal(ns, nt)
    _ => false
  }
}

test "eta and beta equalities" {
  let a = base("A")
  let ctx = @stlc.TypeContext::empty().extend_with(sn("f"), arrow(a, a))
  let sig = @stlc.Signature::empty()
  let wrapped = tlam("x", tapp(tv("f"), [tv("x")]))
  assert_true(beta_eta_equal(sig, ctx, arrow(a, a), tv("f"), wrapped))
  let composed = tlam("x", tapp(tlam("y", tapp(tv("f"), [tv("y")])), [tv("x")]))
  assert_true(beta_eta_equal(sig, ctx, arrow(a, a), composed, tv("f")))
  let twice = tlam("x", tapp(tv("f"), [tapp(tv("f"), [tv("x")])]))
  assert_false(beta_eta_equal(sig, ctx, arrow(a, a), twice, tv("f")))
}

进阶

带轨迹的操作式范式化

normalize_checked 先做类型检查，再运行无类型的正规序 beta-eta 归约器，它给出 eta-短的结果和步数。需要参考语义时使用它：

test "operational normalization" {
  let u = @stlc.Ty::Unit
  let unit_value = @syntax.Term::Value(@stlc.Atom::UnitLit)
  let k = tlam("x", tlam("y", tv("x")))
  let term = tapp(k, [unit_value, unit_value])
  assert_eq(
    @stlc.normalize_checked(@stlc.Signature::empty(), @stlc.TypeContext::empty(), term, u, 10),
    Ok(NormalForm(term=unit_value, steps=2)),
  )
}

要获得完整轨迹，请自行检查项，并用 @lambda.beta_eta_rule 调用 @eval.trace。

在带类型的项上使用底层库

由于 @stlc.Term 就是 @syntax.Term[@stlc.Atom]，代换、自由变量和重写都可原样使用。用类型正确的良类型项代换变量会保持类型（类型化演算的代换引理），因此你可以用 @substitution.Substitution 实例化带类型的模板，再重新检查。

常见陷阱

推断 lambda。 对 lambda 调用 infer 会以 CannotInferLambda 失败。请用带期望类型的 check。
Unit 的 eta。 Unit 类型的中性项（例如变量 u : Unit）不会被替换为 ()。f u 和 f () 的范式不同。
多参数可约式中的参数名。 在 $(\lambda x.\,b)\,a_1\,a_2$ 中，如果 $a_2$ 提及一个同样叫 $x$ 的自由变量，infer 会用参数的类型为它定型（已知问题）。请使用不在后续参数中自由出现的参数名。
用 == 比较范式。 生成的绑定子是 x、x_1、…；请用 @syntax.alpha_equal 比较。

后续步骤

stlc API：所有类型、错误和函数。
stlc 设计：定型规则、η-长形式范式，以及带类型 NbE 的正确性论证。
utlc/nbe 教程：无类型、受燃料限制的对应物。