再帰型の実装に関して悩んでいること１ 再帰する型変数の表現

型システムにどうやって再帰型を追加するかで悩んで手が止まっている。何に悩んでいるのかを書き出して整理していきたい。

今回は「現在、型そのものをtyというバリアント型で表現しているが、その枠組みで再帰型をどう表現するか」について。

そもそも再帰型はOCamlでいうところの

type intlist = Nil | Cons of int * intlist

のような型のことで、左辺で定義されているintlistという型が右辺の定義にも出てくるのがポイント。

ただ、この形だと「型の定義」として独立しておらず、「型が名前付きで存在している環境」とセットでようやくNil | Cons of int * intlistの部分が解釈できる。

再帰関数の場合は

let rec length xs = match xs with Nil -> 0 | Cons(_,xs) -> 1 + length xs

のような関数を

let length = fix (λf.λxs.match xs with Nil -> 0 | Cons(_,xs) -> 1 + f xs)

のようにfixを使って環境に依存することなく再帰的に定義する表記がある。

型レベルでも似たようなやり方があって

type intlist = Nil | Cons of int * intlist

が

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

のように表現できる。μtでtという「再帰的な型変数」を導入してCons of int * tで使っていて、この定義は左辺に出てくる型の名前に依存しない。

じゃあμt.Nil | Cons of int * tをどうやってバリアントとして表現するか。

現在、型を表すバリアントは以下のようになっている：

type ty =
| TVar of tvar ref
...
| TTuple of ty list
...
| TVariant of (string * ty) list
...
and tvar =
| Unbound of int * int
| Link of ty
| Generic of int

一つの素直な考え方としては

type ty =
...
| TRec of string * ty
...
and tvar =
...
| Rec of string

のような形にしてμt.Nil | Cons of int * tは

TRec('t', TVariant [("Nil", TUnit); ("Cons", TTuple [TInt; TVar{contents=Rec "t"}])])

と表現するのも一法。かなり直訳になっている。

しかし∀x.x -> xのような型を

TArrow(TVar{contents=Generic 0}, TVar{contents=Generic 0})

と表現するのと整合性が取りづらい。こちらに寄せるなら

type ty =
...
and tvar =
...
| Rec of int

とTRecは消してμt.Nil | Cons of int * tは

TVariant [("Nil", TUnit); ("Cons", TTuple [TInt; TVar{contents=Rec 0}])]

にしてしまうのが良さそう。あるいは相互再帰のことも考えると

type ty =
...
| TRec of ty list
| TRecNth of ty * int
and tvar =
...
| Rec of int

で

TRec [TVariant [("Nil", TUnit); ("Cons", TTuple [TInt; TVar{contents=Rec 0}])]]

という手もありそう。TVar{contents=Rec 0}の中の数はTRec [...]内での添字を表している。

相互再帰的な型としてはなんだか変な例だが

type t = Tup of s * int * s
and s = Leaf of int | Branch of t

について考えてみる（変というのはtype t = Leaf of int | Branch of t * int * tで事足りるため）。

再帰全体の型は：

TRec
  [ TVariant [("Tup", TTuple [TVar{contents=Rec 1}; TInt; TVar{contents=Rec 1}])]
  ; TVariant [("Leaf", TInt); ("Branch", TVar{contents=Rec 0})]
  ]

そして個別のtとs型はそれぞれ：

TRecNth(
  TRec
    [ TVariant [("Tup", TTuple [TVar{contents=Rec 1}; TInt; TVar{contents=Rec 1}])]
    ; TVariant [("Leaf", TInt); ("Branch", TVar{contents=Rec 0})]
    ],
  0)

と

TRecNth(
  TRec
    [ TVariant [("Tup", TTuple [TVar{contents=Rec 1}; TInt; TVar{contents=Rec 1}])]
    ; TVariant [("Leaf", TInt); ("Branch", TVar{contents=Rec 0})]
    ],
  1)

となる。大変冗長だが相互再帰まで表現できるので、この方法で実装していこうと思う。何が問題が生じて変更するかもしれないが・・・