D言語で作ってみる定理証明支援系(3) 関数を定義する 実装編

目次

• D言語で作ってみる定理証明支援系(1) 型を作る
• D言語で作ってみる定理証明支援系(2) 関数を定義する
• D言語で作ってみる定理証明支援系(3) 関数を定義する 実装編(本記事)

リポジトリはこちら(随時開発中)
https://github.com/outlandkarasu/poet

あらすじ

前回でとりあえず関数の定義についての妄想を広げました。

今回は、その妄想を現実にします。つまり実装を行います。

基本的なデータ構造の準備

さて、関数定義本体の実装に入る前に、ごく基本的なデータ構造を実装しておきます。

D言語にはもちろん組み込みの動的配列や連想配列や、標準ライブラリのコンテナがあるのですが、それらはimmutableでは使いづらいです。
(ふつうはそんなimmutableにこだわらない……)

今回はなるべくimmutableでやっていくという方針なので、ごく簡単なデータ構造を自作します。

不変リスト

不変なデータ構造といえばリストです。
とりあえずテストを貼っておきます。

source/poet/utils/list.d

///
nothrow pure @safe unittest
{
    // 整数123を先頭(head)に持つ長さ1のリストを作る。
    immutable l = list(123);
    assert(l.head == 123);

    // このリストの後ろ(tail)には何もない。
    assert(l.tail is null);
    assert(l.end);

    // リストに1234を追加
    immutable l2 = l.append(1234);

    // 先頭は1234
    assert(l2.head == 1234);

    // 後ろは123
    assert(l2.tail is l);
    assert(l2.tail.head is 123);
    assert(!l2.end);
}

ソースコードはこちら
https://github.com/outlandkarasu/poet/blob/master/source/poet/utils/list.d

格納値であるheadと後続の要素を指すtailのペアからなる、ごく単純なデータ構造です。単純なので実装の話は省略します……。

このデータ構造のすごいところは、不変なまま要素を追加していけるというところです。新しい要素を追加する場合、新しい要素のtailで既存のリストを指し、headに格納値を設定すれば終わりです。
既存のリストは何も変わりません。

今回大いに活用するもう一つの特性があって、この不変リストは途中で分岐できます。分岐といっても、先頭から辿る限りは一本道なのですが、頭をいくつも生やすことができます。

///
nothrow pure @safe unittest
{
    // 整数123
    immutable l = list(123);
    assert(l.head == 123);

    // この先に1〜3の3つの値を生やす。
    immutable l1 = l.append(1);
    immutable l2 = l.append(2);
    immutable l3 = l.append(3);

    // どの要素もtailは共有している。
    assert(l1.tail is l);
    assert(l2.tail is l);
    assert(l3.tail is l);
}

あとで有効活用しますが、この性質を使うと、ある1点の要素さえ保持しておけば、他の処理でどんどんリストが伸ばされても、お互いなんの影響もなく保持した要素から後のリストを使用できます。
保持している要素から新たに別の要素を生やしていくのも自由です。

この性質は何気ないものですが、というか関数型言語とかLISPとかちゃんと使っている人には常識でしょうが、とてもありがたいものでした。

スコープと変数

さて、スコープとかの話に戻ります。

前回で、関数定義を進めていくとスコープが入れ子になり、そこに変数が追加されていく様子が妄想されました。

これからそのスコープなどを実装するに当たって、不変性を保ったままにしておくために、それなりに工夫が必要です。
だいたい以下のような部分が面倒です。

• D言語のimmutableは推移的で、immutableを辿って得られるものはすべてimmutableになっていないといけない。
  • C言語のconst(ポインタがconstでオブジェクトが変更可能などができる)とは違う。
  • 一箇所でもimmutable以外があると、そこから全てが崩れる。
• でも、スコープや変数は追加されたり開始されたり終了したりする。
  • 最上位のDefinitionは可変のオブジェクトにしておくとして、関連する全ての状態はimmutableなスナップショットとして取る必要がある。

色々考えた末、以下のような感じになりました。

source/poet/definition/definition.d

import std.typecons : Rebindable, Typedef;

/// 変数のスコープ内での位置を示す型
alias VariableIndex = Typedef!(size_t, size_t.init, "VariableIndex");

/// スコープを特定するためのID
alias ScopeID = Typedef!(size_t, size_t.init, "VariableIndex");

/// 変数を指し示す値。どのスコープのどの位置なのかの情報を持つ。
sturct Variable
{
    ScopeID scopeID;
    VariableIndex index;
}

final class Definition
{
// 中略...

private:

    /**
    現在の変数のリスト。
    スコープの開始・終了に合わせて差し替えられる。
    immutableだがこれ自体は差し替えらえるので、Rebindableにする必要がある。
    */
    Rebindable!(List!VariableEntry) variables_;

    /**
    最後のスコープに振ったID。連番付与用。
    */
    ScopeID lastScopeID_;
}

// 以下は実装用コードなので外部公開しない。
private:

/// 関数定義のスコープ情報。
final immutable class CScope
{
    /// スコープを一意に特定するID。
    ScopeID id;

    /// スコープで定義しようとしている関数の型。
    FunctionType target;

    /// スコープ開始直前の位置を示す。
    List!VariableEntry before;
}

alias Scope = immutable(CScope);

/**
変数の情報を持つ構造体。
*/
struct VariableEntry
{
    /// 現在のスコープ。
    Scope currentScope;

    /// 変数の位置
    VariableIndex index;

    /// 変数の型
    Type type;
}

上記のScope・VariableEntryを組み合わせることで、スコープの入れ子と変数の利用を実現します。

auto f = define(F, (d, ab) {
    // 新たなScopeと最初の引数を持つList!VariableEntryを生成し、
    // d.variables_に設定する。
    // 新たなScopeのbeforeには、スコープ生成時点のd.variables_を保持しておく。
    auto bc = d.begin();
      // 同上
      auto a = d.begin();

        // 新たなVariableEntryを生成し、variables_に追加する。
        auto b = d.apply(ab, a);
        auto c = d.apply(bc, b);

      // d.variables_.head.currentScope.beforeを参照し、variables_をスコープ開始前に戻す。
      // その後、定義した関数の型のVariableEntryを生成し、variables_に追加する。
      auto ac = d.end(c);
    // 同上
    auto bcac = d.end(ac);
    return bcac;
});

あとは、begin・apply・endでの型チェックや変数のスコープチェックをちゃんと行えば、とりあえず型のみを使った関数定義は行えるようになります。
(Variableは、そのためにスコープのIDと変数のインデックスを持っています)

スコープ・型のチェック

Definitionの各メンバ関数は、どのような値に対してもどの順番でも呼べるので、ちゃんと実装の中で型チェック・スコープチェックを行う必要があります。
このチェックを行ってはじめて、ちゃんとした型システムだといえます。
どんな強固な型システムを誇るプログラミング言語でも、結局はどこかで誰かが似たようなチェックをやっていると思われます。

ここまでで必要になるチェックは以下のようなものです。実装の説明は退屈なので省略します。

• beginした時
  • 現在のスコープのtargetが関数型であること
  • 関数型でなければbeginできない(妄想の世界に入れない)のでエラー
• applyした時
  • 引数のf・aがスコープから見えていること
    • 現在のスコープの変数か、beforeを再帰的に辿ってたどり着ける変数であること
  • 第1引数のfが関数型であること
  • 第2引数のaがfの引数の型であること
• endした時
  • 引数の変数がスコープから見えていること
  • 引数の変数の型が、スコープのtargetの戻り値の型であること
• defineを終えるとき
  • returnした変数の型が当初の関数型の戻り値の型と一致すること
  • 閉じられていないスコープが残っていないこと

次回予告

今回で、関数型を作るための最低限のシステムはできました。
型および変数のスコープの整合性を担保しつつ、関数の中身がどうなっているかを定義することができるようになりました。

次回は、今回指定できるようになった関数定義の情報を元に、実際に動かせる関数の値を作るところをやってみようと思います。