Luna Flow
日本語

stlc チュートリアル

このチュートリアルでは、単純型付きラムダ項を型検査し、型エラーを説明し、型の付く項を正規化し、2 つの項が 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→AA \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",
  )
}

関数をその型に対して検査する

ラムダは推論されるのではなく検査される。期待される型を与えると、検査器がそれを本体へと押し込む。

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 正規形であり、関数型の部分項はすべてラムダとして書かれる。

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")
  }
}

簡約基 (λh. h) g(\lambda h.\,h)\,g は、h に g の型を与えることで推論される。

beta-eta 等価性を判定する

同じ型を持つ 2 つの型の付く項が βη\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 で型付きテンプレートを具体化し、再検査できる。

よくある落とし穴

  • ラムダの推論。 ラムダに対する infer は CannotInferLambda で失敗する。期待される型とともに check を使うこと。
  • Unit の eta。 Unit 型の中立項（たとえば変数 u : Unit）は () に置き換えられない。f u と f () の正規形は異なる。
  • 複数の引数を持つ簡約基の仮引数名。 (λx. b) a1 a2(\lambda x.\,b)\,a_1\,a_2 において、a2a_2 が同じく xx という名前の自由変数に言及していると、infer はそれに仮引数の型を付けてしまう（既知の問題）。後続の引数に自由に現れない仮引数名を使うこと。
  • == による正規形の比較。 生成される束縛子は x、x_1、… である。@syntax.alpha_equal で比較すること。

次のステップ