elab API リファレンス

elab パッケージ（src/elab、インポートパス Luna-Flow/stella/elab）は stella のカーネルです。依存型理論の構文、その値への評価、値から正規形への読み戻し、そして双方向型検査器を提供します。インターフェースファイルは src/elab/pkg.generated.mbti です。

項は de Bruijn インデックスを使います。Bound(0) は最も近い外側の束縛子が束縛する変数です。束縛子は Lam と、Pi、Sigma、W の第 2 引数だけです。型付け規則の全体は設計ノートにあります。

このページの例は、次の 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` は束縛子 1 つの下にあります。
`App(f, t)`	$f\,t$	関数適用。
`Sigma(A, B)`	$\Sigma_{x : A} B$	依存ペア型。`B` は束縛子 1 つの下にあります。
`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` は束縛子 1 つの下にあります。
`WRec(A, B, P, s, w)`	$\mathrm{wrec}$	`w : W(A, B)` に関する、モチーフ `P` への再帰。`W` の場合とは異なり、ここでの `B` は型 $A \to \mathcal U_k$ の関数項です。

TermInf::equal は項を構造的に比較します。変数が de Bruijn インデックスなので、これは $\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` は束縛子 1 つの下にあります。定義域は書かず、期待される型から得られます。
`Pair(t, u)`	$(t, u)$	依存ペア。
`Rfl(t)`	$\mathrm{refl}\,t$	$\mathrm{Id}_A(t, t)$ の反射律の証明。
`Sup(a, f)`	$\sup(a, f)$	ラベル `a` と子関数 `f` を持つ W 型のノード。

型は 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_ 関数によって簡約されます。評価は型検査を行いません。型の誤った項に対しては、たとえば関数でないものが適用されたときや Bound(i) に対応する環境のエントリがないときに panic することがあります。

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

val_w_rec(a, b, p, s, w) は w = VSup(l, f) に対して次を計算します。

\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 は 2 つの宇宙のうち大きい方を返します。

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())) です。正規形が等しい 2 つの項は $\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 の型を値として返し、type_chk(l, ctx, env, t, ty) は t が型 ty を持つとき正常に戻ります。どちらもそうでなければ TypeError を送出します。引数は項の位置を表します。

l は検査器が入った束縛子の数で、Local(l) は次の新しい変数です。
ctx はユーザーの Global 宣言と、入った束縛子ごとに 1 つのエントリ (Local(k), A_k) を含みます。
env は入った束縛子ごとに 1 つのエントリ 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) です。定数を宣言するには (Global(name), type) を ctx に追加します。型は値で、たとえば型変数なら 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

def_eq(l, s, t) は、設計ノートの累積的部分型付けのもとで $s \le t$ が成り立つとき true を返します。すなわち $i \le j$ に対して $\mathcal U_i \le \mathcal U_j$ 、 $\Pi$ 型は定義域について反変かつ余域について共変、 $\Sigma$ 型は第 1 成分について不変かつ第 2 成分について共変で、その他の型はすべて変換（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

型検査

TypeError

type_inf, type_chk

type_inf_0

def_eq

非推奨