無限展開される再帰的型定義の検出

実装したのは結構前だが、なんかメモとして残しておいた方が良いような気がするので、大雑把なメモ書きながら書いておく。例によって檜山さんよりのレクチャーが元。檜山さんのブログのメモ編にもいろいろ書かれてる(末尾に記載)。

Catyの型システムはstructual subtypingなのだが、そこで再帰的な型が無限展開されてしまうと型同士の包含関係の判定が面倒なので、無限展開されるような型定義はひとまず禁止したい。

例えば次の型定義は無限展開されないのでOK。

type cons<X> = {
    "a": X,
    "b": cons<X> | null,
};

"b"の値は型定義の左辺の形と同じなので、型をグラフで表現するとすれば、そのまま"b"からルートノードへの参照を張ればそれで終わり。

それに対して、次のような型定義は無限展開されるのでNG。

type cons2<X> = {
    "a": X,
    "b": cons2<[X, X]> | null,
};

無限展開の様子を書き下すとこうなる。

type cons2<X> = {
    "l": X,
    "r": null | cons2<[X, X]> = {
        "l": [X, X],
        "r": null | cons2<[[X, X], [X, X]]> = {
            "l": [[X, X], [X, X]],
            "r": ...
        }
    }
};

この問題は「未知関数を含む代数方程式が、有限個の従属変数を導入して、可解な連立方程式に書き直せるか」という言葉で言い直すことも出来る。例えば最初に出した型定義は、次のような方程式が対応する。

f1(x) = x*(1 + f1(x))

これは具体的なxが与えられればf1(x)の解は求められる。それに対して二番目の型定義はこうだ。

f2(x) = x*(1 + f2(x*x))

これは具体的なxが与えられてもf2(x)の値が常に求まるわけではない。

あるいは、再帰関数定義を末尾再帰に限定して認めるというのも似たような話だ。もしくは、再帰的型定義の作るグラフをオートマトンだと捉え、それが静的に一つの有限オートマトンに定まるのであれば、その型定義は無限展開されないと言える。


圏論の言葉で言い表してみる。先の型定義の作るグラフGからP(G)によって作られる自由圏Dがあり、Fを圏Dから圏Vへの関手と定義する。F(P(G))=Vだが、面倒なのでFはGからVへの関手という事にして話を進める。このときtをGの頂点、Cをtが始点となるサイクル、c1,c2...cnをCに含まれる辺とする。F(C)=F(c1);F(c2);...F(cn)であり、なおかつサイクルなのでF(C):F(t)->F(t)である。ここでV上の自己関手Eを考えれば、E(F(t)):F(t)->F(t)なので、F(C)はE(F(t))に入る。E(F(t))=M, F(C)=mとすれば、任意の圏Xと対象x∈Xについてhom(x, x)はモノイドなので、Mはモノイドであり、mはモノイドの元であり、mはVの射である、

モノイドMに対してmの冪乗をm0, m1, m2...mnと書き、このmの冪乗の集合P={mn| n = 0, 1, 2...}において、mn+1=mp(0≦p≦n)という関係が成立するならば、Pは有限集合となる。Pが有限集合であるということは、グラフGのサイクルCを繰り返すと適当なところで循環するということである。


というような理屈を踏まえた上で、どうやって無限展開される型定義を検出するのかという話に移る。先に出したcons2のように、型パラメータが1つであり尚且つそれが複合型で使われている場合、それは無限展開される。cons1のように複合型に使われていない場合は有限回数で展開は止まる。

型パラメータが複数の場合、仮にtype T<X, Y>というパラメータだとすれば、tの右辺に出現するTにおいて、T<Y, X>は明らかに2回の展開でT<X, Y>に戻る。この場合は先のmn+1=mpにおいて、n=1でp=0のケースである。T<X, Y>は1回で左辺と同じ形になるので、n=0でp=0のケースである。ここで複合型Fを導入する。T<F, ?>でFにXが含まれる場合、これは先のcons2同様に無限展開される。FにYのみが含まれる場合、?にXが含まれないならば無限展開はされない。型パラメータが3個以上の場合も同様に計算できる。

この無限展開されるケースを図で書いてみると、大体の感覚が掴めると思う。


というわけで型パラメータを取る再帰的型定義の無限展開の問題は片付いたように思えるが、T<T<X>>みたいなケースは考えていなかったりする。というか何かもうこんな定義使うのかよという気がするので、今のところこれは禁止ということになってる。

以下、参考資料。

更新履歴 

2011-08-03
公開