Luna Flow
日本語

アダプタのチュートリアル

このチュートリアルでは、独自の式の型を type_theory に接続する。小さな AST に対して @syntax.BindingSyntax を実装し、Term[T] に変換することなく、その上で汎用の自由変数計算、捕獲回避代入、書き換えを利用する。最後にアダプタの法則をテストする。

クイックスタート

moon add Luna-Flow/type_theory@0.2.0
import {
  "Luna-Flow/type_theory/core",
  "Luna-Flow/type_theory/syntax",
  "Luna-Flow/type_theory/substitution",
  "Luna-Flow/type_theory/rewrite",
}

以下は、数値、演算子記号、変数、呼び出し、束縛子 Fun(x, body) を持つ式言語と、そのアダプタである。

priv enum Expr {
  Num(Int)
  Sym(String)
  Var(@core.Name)
  Call(Expr, Array[Expr])
  Fun(@core.Name, Expr)
} derive(Eq, Debug)

impl @syntax.BindingSyntax for Expr with fn project(self) {
  match self {
    Num(_) | Sym(_) => Opaque
    Var(x) => Variable(x)
    Call(f, args) => Apply(f, args)
    Fun(x, body) => Bind(x, body)
  }
}

impl @syntax.BindingSyntax for Expr with fn variable(x) {
  Var(x)
}

impl @syntax.BindingSyntax for Expr with fn apply(f, args) {
  Call(f, args)
}

impl @syntax.BindingSyntax for Expr with fn bind(x, body) {
  Fun(x, body)
}

test "quick start: free variables of an Expr" {
  let x = @core.Name::new("x")
  let y = @core.Name::new("y")
  let e = Fun(x, Call(Sym("+"), [Var(x), Var(y)]))
  let fv = @syntax.generic_free_variables(e)
  assert_true(fv.contains(y))
  assert_false(fv.contains(x))
}

数値と演算子記号は変数を含まないので Opaque に射影される。この例は単一のパッケージ内にあるので型は priv である。AST をエクスポートするライブラリでは型を pub(all) にし、昇格させるメソッドを pub extend で宣言する。呼び出しの演算子はその頭部なので、呼び出しを再構築しても演算子は保たれる。

日常的な作業

捕獲なしで代入する

GenericSubstitution::apply_once は自由変数を置き換え、必要に応じて Fun 束縛子の名前を付け替える。

test "capture-avoiding substitution on Expr" {
  let x = @core.Name::new("x")
  let y = @core.Name::new("y")
  let e = Fun(y, Call(Sym("+"), [Var(x), Var(y)]))
  let s = @substitution.GenericSubstitution::singleton(x, Var(y))
  let y1 = @core.Name::new("y_1")
  assert_eq(s.apply_once(e), Fun(y1, Call(Sym("+"), [Var(y), Var(y1)])))
}

部分評価する

既知の値を代入し、残りは記号のまま保つ。

test "partial evaluation on Expr" {
  let x = @core.Name::new("x")
  let y = @core.Name::new("y")
  let e = Call(Sym("*"), [Var(x), Var(y)])
  let known = @substitution.GenericSubstitution::singleton(x, Num(3))
  assert_eq(known.apply_once(e), Call(Sym("*"), [Num(3), Var(y)]))
}

書き換え規則で簡約化する

独自の型に対して規則を書き、それが適用できる位置は汎用の走査に見つけさせる。

fn fold_add(e : Expr) -> Expr? {
  match e {
    Call(Sym("+"), [Num(a), Num(b)]) => Some(Num(a + b))
    _ => None
  }
}

test "constant folding on Expr" {
  let x = @core.Name::new("x")
  let e = Call(Sym("*"), [Var(x), Call(Sym("+"), [Num(1), Call(Sym("+"), [Num(2), Num(3)])])])
  let rule = @rewrite.RuleName::unsafe_new("fold_add")
  assert_eq(
    @rewrite.generic_normalize(e, rule, fold_add, 10),
    NormalForm(term=Call(Sym("*"), [Var(x), Num(6)]), steps=2),
  )
  match @rewrite.generic_top_down_once(e, rule, fold_add) {
    Reduced(path~, ..) =>
      assert_eq(path.to_array(), [@rewrite.ApplyArgument(1), @rewrite.ApplyArgument(1)])
    NoStep => fail("expected a step")
  }
}

このパスは、* の第 2 引数、次に外側の + の第 2 引数を表す。

束縛子の名前を付け替える

generic_alpha_rename_bound は束縛子の本体にある変数の名前を付け替え、すでに使われている名前は拒否する。

test "rename a Fun parameter" {
  let x = @core.Name::new("x")
  let y = @core.Name::new("y")
  let z = @core.Name::new("z")
  let body = Call(Sym("+"), [Var(x), Var(y)])
  assert_true(@syntax.generic_alpha_rename_bound(body, x, y) is None)
  assert_eq(
    @syntax.generic_alpha_rename_bound(body, x, z),
    Some(Call(Sym("+"), [Var(z), Var(y)])),
  )
}

さらに進んで

アダプタの法則をテストする

汎用アルゴリズムが正しいのは、project とコンストラクタが整合している（アダプタの設計のビュー法則）場合に限られる。代表的なノードでテストすること。

fn rebuild(e : Expr) -> Expr {
  match @syntax.BindingSyntax::project(e) {
    Opaque => e
    Variable(x) => @syntax.BindingSyntax::variable(x)
    Apply(f, args) => @syntax.BindingSyntax::apply(f, args)
    Bind(x, body) => @syntax.BindingSyntax::bind(x, body)
  }
}

test "view laws" {
  let x = @core.Name::new("x")
  let samples = [
    Num(1),
    Sym("+"),
    Var(x),
    Call(Sym("+"), [Var(x), Num(2)]),
    Fun(x, Var(x)),
  ]
  for e in samples {
    assert_eq(rebuild(e), e)
    if @syntax.BindingSyntax::project(e) is Opaque {
      assert_eq(@syntax.generic_free_variables(e).length(), 0)
    }
  }
}

一つのビューケースに属する複数の演算子

すべての呼び出しは Apply に射影され、演算子は頭部に載って運ばれるので、apply(head, args) は任意の呼び出しを再構築できる。AST に Add(a, b) や Mul(a, b) のような別々のノード種別がある場合は、種別を識別する頭部を与えること（ここでの Sym のように）。そうしないと apply はどのノードを再構築すべきか分からない。

独自の変数型を橋渡しする

AST が独自の変数型を持つ場合は、project でそれを @core.Name に単射的に写し（異なる変数には異なる名前）、variable で逆に写す。

よくある落とし穴

  • 不透明なノードの中の変数。 Opaque に射影されるノードが探索されることはない。変数を含んでいると、代入はそれらを見落とす。
  • ドット構文でトレイトのメソッドを呼び出す。 @syntax.BindingSyntax::project(e) と書くこと。メソッド形式は昇格されていない。
  • apply でノード種別が失われる。 二つのノード種別が Apply に射影され、頭部がどちらであるかを示さない場合、再構築によって AST が変わってしまう。
  • 繰り返しの代入を期待する。 apply_once は一度だけ代入する。置換項が定義域の名前に言及する場合は自分で反復すること。

次のステップ