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

ここには 3 つの考え方が現れています。関数 Lam には定義域の注釈がないため、カーネルはその型を推論できません。Ann が型を与えます。type_inf_0 は型を値として返し、quote(0, _) は値を表示可能な項に戻します。eval_inf は計算を行い、適用は UnitElement に簡約されます。

日常的なタスク

de Bruijn インデックスの読み書き

変数は数値です。Bound(0) は最も近い外側の束縛子の変数、Bound(1) はその外側のもの、という具合です。束縛子は Lam と、Pi、Sigma、W の第 2 引数です。多相恒等関数 $\lambda A.\,\lambda x.\,x : \Pi_{A : \mathcal U_0} \Pi_{x : A} A$ は次のように書きます。

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

型の中で、内側の $\Pi$ の定義域は Bound(0)、すなわち外側の $\Pi$ が束縛する $A$ です。その余域はさらに 1 つ多くの束縛子の下にあるので、同じ $A$ はそこでは 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"))) です。

ペアを扱う

ペアは $\Sigma$ 型に対して検査され、射影はそこから型を推論します。

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) であり、$\mathcal U_i$ の型はそれより大きいすべての宇宙でも受理されます。

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 は推論可能な関数でなければならないので、注釈を付けます。ここではモチーフは定数 $P = \lambda y.\,\lambda p.\,A$ であり、$J$ は a を refl 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\")))")
}

項を正規化して比較する

項の正規形はその値の読み戻しです。正規化は束縛子の下でも簡約するので、項の $\beta$ 等価性を判定できます。

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 を使います。名前がインデックスなので、これは $\alpha$ 同値です。

束縛子の下で自分で検査する

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 ですが、形成規則は型の宇宙を推論するため、型を置く場所には裸の Lam や Pair ではなく Inf(UnitType) のように書きます。
• 関数を推論させるには注釈が必要。 Lam(...) は検査しかできません。適用の中やモチーフとして使うには Ann(lam, Inf(Pi(...))) で包みます。
• W と WRec では族の書き方が異なる。 W(A, B) では B は束縛子の下の本体ですが、WRec(A, B, ...) では B は型 $A \to \mathcal U_k$ の推論可能な関数項です。
• def_eq は向きがあり、コンテキストを持たない。 部分型を判定するものであり、f の型を知らないため、f x のような中立適用は読み戻しの結果で比較し、引数に $\eta$ は使わない。
• 評価は入力を信頼する。 eval_inf と val_ 関数は型の誤った項で panic します。先に型検査をしてください。
• Debug で表示する。 カーネルの型は Show ではなく Debug を導出しています。debug_inspect、Repr(x)、@debug.to_string(x) を使ってください。クロージャは <function: ...> と表示されるので、値は表示する前に quote してください。

次のステップ

• API リファレンスにはすべてのコンストラクタと関数が載っています。
• 設計ノートでは、型付け規則を推論規則の記法で示し、評価による正規化を説明しています。
• 概要からリンクされている論考は、型なしラムダ計算から出発してこの型理論を展開しています。