stlc API

stlc パッケージは、共有の名前付き構文上の単純型付きラムダ計算である。型、型付き定数のシグネチャ、型文脈、双方向の型推論と型検査、ステップ数に上限のある操作的正規化、そして β 正規形・η 長形式への型付き評価による正規化（NbE）を提供する。

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

項は @syntax.Term[Atom] である。Bind(x, b) は $\lambda x.\,b$ （型注釈なし）、Apply は適用、Variable は変数であり、Value は Atom を保持する。型付け規則と NbE アルゴリズムは stlc の設計に記載されている。

構文

`Atom`

Atom はこの計算体系の定数である。

pub(all) enum Atom {
  UnitLit
  Const(@core.Name)
} derive(Eq, @debug.Debug)
pub fn Atom::equal(Self, Self) -> Bool

UnitLit は単位値 $()$ である。Const(c) は型が Signature で宣言された定数である。

`Term`

Term は STLC の項の型である。

pub type Term = @syntax.Term[Atom]

これは別名なので、syntax、substitution、rewrite のすべてが STLC の項に適用できる。

`Ty`

Ty は単純型である。

pub(all) enum Ty {
  Base(@core.Name)
  Unit
  Arrow(Ty, Ty)
} derive(Eq, @debug.Debug)
pub fn Ty::equal(Self, Self) -> Bool

Base(b) は解釈されない基本型、Unit は単位型、Arrow(a, b) は関数型 $a \to b$ である。型は構造的に比較される。

シグネチャと文脈

`Signature`

Signature は定数に型を割り当てる。

pub struct Signature {
  entries : Array[(@core.Name, Ty)]
} derive(Eq, @debug.Debug)
pub fn Signature::empty() -> Self
#alias(extend, deprecated)
pub fn Signature::extend_with(Self, @core.Name, Ty) -> Self
pub fn Signature::lookup(Self, @core.Name) -> Ty?
pub fn Signature::to_array(Self) -> Array[(@core.Name, Ty)]
pub fn Signature::equal(Self, Self) -> Bool

extend_with(c, ty) は c : ty を追加した新しいシグネチャを返す。同じ名前に対する後の項目は前の項目を隠し、lookup は最新のものを返す。to_array は項目のコピーを挿入順で返す。

`TypeContext`

TypeContext は自由変数に型を割り当てる。

pub struct TypeContext {
  entries : Array[(@core.Name, Ty)]
} derive(Eq, @debug.Debug)
pub fn TypeContext::empty() -> Self
#alias(extend, deprecated)
pub fn TypeContext::extend_with(Self, @core.Name, Ty) -> Self
pub fn TypeContext::lookup(Self, @core.Name) -> Ty?
pub fn TypeContext::to_array(Self) -> Array[(@core.Name, Ty)]
pub fn TypeContext::equal(Self, Self) -> Bool

同じ隠蔽規則が適用される。型検査器はラムダに入るときに文脈を拡張するので、名前に対して最も近い束縛子が優先される。

test "signatures and contexts" {
  let c = @core.Name::new("c")
  let x = @core.Name::new("x")
  let a = @stlc.Ty::Base(@core.Name::new("A"))
  let sig = @stlc.Signature::empty().extend_with(c, @stlc.Ty::Arrow(a, a))
  let ctx = @stlc.TypeContext::empty().extend_with(x, a).extend_with(x, @stlc.Ty::Unit)
  assert_eq(sig.lookup(c), Some(@stlc.Ty::Arrow(a, a)))
  assert_eq(ctx.lookup(x), Some(@stlc.Ty::Unit))
  assert_eq(ctx.to_array().length(), 2)
}

エラー

`TypeError`

TypeError は項が拒否された理由を報告する。

pub(all) enum TypeError {
  UnboundVariable(@core.Name)
  UnknownConstant(@core.Name)
  CannotInferLambda
  ExpectedFunction(Ty)
  TypeMismatch(expected~ : Ty, actual~ : Ty)
  EmptyApplication
  ScopeError(@debruijn.ScopeError)
  NormalizationError(message~ : String)
} derive(Eq, @debug.Debug)
pub fn TypeError::equal(Self, Self) -> Bool

ケース	意味
`UnboundVariable(x)`	`x` が文脈にない。
`UnknownConstant(c)`	`c` がシグネチャにない。
`CannotInferLambda`	型を推論しなければならない位置にラムダが現れた。
`ExpectedFunction(ty)`	関数型でない型 `ty` の項が適用された。
`TypeMismatch(expected, actual)`	推論された型が期待される型と異なる。
`EmptyApplication`	`Apply(head, [])` に引数がない。
`ScopeError(e)`	de Bruijn のスコープ失敗のために予約されている。現在の関数はこれを生成しない。
`NormalizationError(message)`	型付き NbE の内部不変条件が破れた。検査済みの入力では起こらないはずである。

型検査

`infer`

infer は項の型を合成する。

pub fn infer(Signature, TypeContext, @syntax.Term[Atom]) -> Result[Ty, TypeError]

単位リテラルの型は Unit であり、定数と変数は宣言された型を持つ。適用 f a_1 … a_n は、各引数を対応する定義域に対して検査した後の f の結果型を持つ。単独のラムダは推論できない（CannotInferLambda）。引数に直接適用されたラムダは、最初の引数の型を推論し、その仮定の下で本体を推論することで推論される。

`check`

check は項を型に対して検査する。

pub fn check(Signature, TypeContext, @syntax.Term[Atom], Ty) -> Result[Unit, TypeError]

ラムダは矢印型に対して、パラメータに定義域を与えたうえで本体を値域に対して検査することで検査される。それ以外の項はすべて型を推論し == で比較する。異なれば TypeMismatch となる。

test "infer and check" {
  let x = @core.Name::new("x")
  let f = @core.Name::new("f")
  let a = @stlc.Ty::Base(@core.Name::new("A"))
  let id : @stlc.Term = Bind(x, Variable(x))
  let sig = @stlc.Signature::empty()
  let ctx = @stlc.TypeContext::empty()
  assert_eq(@stlc.check(sig, ctx, id, @stlc.Ty::Arrow(a, a)), Ok(()))
  assert_eq(@stlc.infer(sig, ctx, id), Err(@stlc.TypeError::CannotInferLambda))
  let ctx_f = ctx.extend_with(f, @stlc.Ty::Arrow(a, a))
  let bad : @stlc.Term = Apply(Variable(f), [Value(@stlc.Atom::UnitLit)])
  assert_eq(
    @stlc.infer(sig, ctx_f, bad),
    Err(@stlc.TypeError::TypeMismatch(expected=a, actual=@stlc.Ty::Unit)),
  )
}

正規化

`normalize_checked`

normalize_checked は項を型に対して検査し、その後、型なしの βη 簡約器で正規化する。

pub fn normalize_checked(Signature, TypeContext, @syntax.Term[Atom], Ty, Int) -> Result[@rewrite.NormalizationResult[Atom], TypeError]

型エラーの場合は簡約せずに Err を返す。そうでなければ Ok(@lambda.normalize(term, max_steps)) を返す。これはステップ上限付きの正規順序 βη 簡約である。その正規形は β 正規かつ η 短形式である。

`normalize_eta_long`

normalize_eta_long は項を型に対して検査し、その β 正規・η 長形式を返す。これは型付きの評価による正規化で計算される。

pub fn normalize_eta_long(Signature, TypeContext, @syntax.Term[Atom], Ty) -> Result[@syntax.Term[Atom], TypeError]

結果において、矢印型の部分項はすべてラムダであり、すべての適用は頭部に変数または定数を持つ。文脈の変数とシグネチャの定数はそのまま保たれ、それぞれの型に従って η 展開される。ステップ上限は不要である。型の付く項は常に正規化されるからである。新しい束縛子の名前は x、x_1、… であり、項と文脈のすべての名前を避けるように選ばれる。

test "beta-normal eta-long form" {
  let f = @core.Name::new("f")
  let x = @core.Name::new("x")
  let a = @stlc.Ty::Base(@core.Name::new("A"))
  let ctx = @stlc.TypeContext::empty().extend_with(f, @stlc.Ty::Arrow(a, a))
  let sig = @stlc.Signature::empty()
  // f is eta-expanded to λx. f x
  let expected : @stlc.Term = Bind(x, Apply(Variable(f), [Variable(x)]))
  match @stlc.normalize_eta_long(sig, ctx, Variable(f), @stlc.Ty::Arrow(a, a)) {
    Ok(normal) => assert_true(@syntax.alpha_equal(normal, expected))
    Err(_) => fail("well typed")
  }
  // the operational normalizer contracts the redex but does not expand
  let redex : @stlc.Term = Apply(Bind(x, Variable(x)), [Variable(f)])
  assert_eq(
    @stlc.normalize_checked(sig, ctx, redex, @stlc.Ty::Arrow(a, a), 10),
    Ok(NormalForm(term=Variable(f), steps=1)),
  )
}

非推奨

非推奨	代替
`Signature::extend`	`Signature::extend_with`
`TypeContext::extend`	`TypeContext::extend_with`

このパッケージの型にある隠されたメソッド形式 not_equal と to_repr は非推奨である。!= と Repr(x) を使うこと。