再帰型の実装に関して悩んでいること２ equi-recursive対iso-recursive

TaPLを読むと再帰型の理論と実装について、equi-recursiveとiso-recursiveという二つの流儀があると書いてある。

equi-とiso-については以下の記事でも少し触れた：

zehnpaard.hatenablog.com

しかし実際どういう違いなのかをメモった上でどちらにするのかを決めていきたい。

前回に続いて

type intlist = Nil | Cons of int * intlist

という再帰型を考える。これを「環境なしで」表そうと思うと内部的に不動点コンビネータを使っていると見做せる「μ」を利用してこう書ける：

type intlist = μt.Nil | Cons of int * t

さて、ここでintlistに対するパターンマッチについて考える：

let rec sum xs = match xs with
| Nil -> 0
| Cons(x, xs') -> x + sum xs'

この場合xsの型は何か。当然intlistつまりμt.Nil | Cons of int * tであるのだが、同時にmatch xs with | Nil -> 0 | Cons(x, xs') -> x + sum xs'の部分を見ると

Nilというタグを持つ
Consというタグを持ち、その保有する型はintと「sumの引数の型」すなわちμt.Nil | Cons of int * t

というバリアントになる。つまりNil | Cons of int * (μt.Nil | Cons of int * t)だ。

この型はμt.Nil | Cons of int * tのimplicitなFixを一回展開している形で、つまり(λt.Nil | Cons of int * t) (μt.Nil | Cons of int * t)の結果だ。

さてこの展開した形であるNil | Cons of int * (μt.Nil | Cons of int * t)と元のμt.Nil | Cons of int * tがどのような関係にあるか、というのがequi-recursiveとiso-recursiveの観点の違いだ。

equi-recursiveな立場をとるとこの二つの型はまったく同一のものとなる。

type intlist = Nil | Cons of int * intlist

という定義からすれば、右辺のintlistを一回展開してNil | Cons of int * (Nil | Cons of int * intlist)にしても同一性が保たれる、というのは納得できる理屈である。ということは型検査や単一化などの処理で再帰型の扱いは特殊化して、このような形の違う型が同一だと判定したり単一化できたりしないといけない。

それに対してiso-recursiveな立場だとこれら二つの型は同型ではあるが別物と考えられる。そのままでは同一と判定したり単一化したりできない。

うまく単一化させるためにはFoldやUnfoldが正しいところに挟まれていないといけない。これはかなりめんどくさそうではあるが、実際にはプログラマが手動でFoldやUnfoldを書く必要はなくパースから型検査の間のどこかでFold/Unfoldを自動で挿入するステップがあればいい。コンストラクタの適用時に自動的にFoldが追加され、パターンマッチなどで代数的データ型が分解されるときに自動的にUnfoldが追加されるようになる。

例えば

Cons(0, xs)

という式はそのままだと0がint、xsがμt.Nil | Cons of int * tなのでNil | Cons of int * (μt.Nil | Cons of int * t)な型となる。しかしこの式をAST化する時に自動的にFoldを入れる：

EFold(ETag("Cons", [EInt 0; EVar "xs"]))

（実際にはEFoldにはintlistの型定義も入るのだがややこしいので割愛）

逆にパターンマッチの

let rec sum xs = match xs with
| Nil -> 0
| Cons(x, xs') -> x + sum xs'

でも、match xs with ...のxsの部分の周りにUnfoldがつくことでその式の型がNil | Cons of int * (μt.Nil | Cons of int * t)になる。これでパターンマッチの各ケースに直接対応する形になる。

なので「 Iso-recursiveだとFold/Unfoldを明示的にプログラマが書く必要が生じて煩雑」ということはない。

ただしFold/Unfoldがコンストラクタやパターンマッチによって自動的に挿入される都合上、再帰型を導入するためにはコンストラクタを導入するバリアントを使う必要がある。ただのタプルを使った再帰型、例えば

type t = (int * t)

といった型は定義できない。

OCamlやHaskellなどは基本的にIso-recursiveな再帰型が実装されている。上記の制限が実際のプログラムで大きな問題になることはなさそうで、その上で理論・実装の両面からIso-recursiveな方がEqui-recursiveより単純なようだ。

というわけで私の実装もIso-recursiveでやっていきたい。

Arantium Maestum

プログラミング、囲碁、読書の話題

再帰型の実装に関して悩んでいること２ equi-recursive対iso-recursive