再帰的多相バリアントそぞろ歩き

これはML Advent Calendar 2020の1日目の記事です。

---

S式をバリアント（代数データ型）として定義する場合、どのような定義にするのがよいだろうか。

とりあえず、シンボル、ベクタ、ドット対、空リストだけを考えることにして定義してみよう。

type t =
  | Symbol of string
  | Vector of t array
  | Cons of t * t
  | Nil

とはいうものの、リストをパターンマッチするときに Cons の入れ子を書くのはダルい気がするので、 OCaml のリストにしてしまおう。

type t =
  | Symbol of string
  | Vector of t array
  | List of t list

これだと、 (a b . c) のような非真正リストが表現できなくなってしまうので、 DottedList を別に追加する¹。

type t =
  | Symbol of string
  (** [Symbol "foobar"] = foobar *)
  | Vector of t array
  (** [Vector [| Symbol "a"; Symbol "b" |]] = #(a b) *)
  | List of t list
  (** [List [Symbol "a"; Symbol "b"]] = (a b) *)
  | DottedList of t list * t
  (** [DottedList ([Symbol "a"; Symbol "b"], Symbol "c")] = (a b . c) *)

これでとりあえずの用は足りるのだけど、ふたつ気になることがある。

1. DottedList ([], Symbol "a") のような、S式としては不正なデータが存在してしまう。
2. List [Symbol "a"; Symbol "b"] と DottedList ([Symbol "a"], List [Symbol "b"]) のように、 (a b) に対応する表現が複数存在してしまう（Lisp的には、 (a . (b)) や (a . (b . ())) は read 時に (a b) に正規化されるのでこのようなことは起きない）。

前者に関しては、 DottedList の定義を DottedList of t * t list * t のようにでもすればいいだろう。

後者に関しては、型をアトムとそれ以外に分けて、 DottedList の後ろにはアトムしか来られないようにすることが考えられる。

type atom =
  | Symbol of string
  | Vector of t array
and t =
  | Atom of atom
  | List of t list
  | DottedList of t list * atom

が、アトムを毎回 Atom で包むのは面倒でやっていられない。多相バリアントを使うとどうだろうか。

type atom =
  [ `Symbol of string
  | `Vector of t array
  ]
and t =
  [ atom
  | `List of t list
  | `DottedList of t list * atom
  ]

これならよさそうだ。

しかし、これは The type constructor atom is not yet completely defined というエラーでコンパイルが通らない²。多相バリアントを拡張する場合、拡張される側の型は、参照される時点で定義が完了していないといけないからだ。

このあたりを調べていると、 Correct mutually recursive types are rejected by the type-checker · Issue #8511 · ocaml/ocaml というissueに行きあたる。

ここでは、2つのワークアラウンドが紹介されている。再帰モジュールを使う方法と、補助的な型を使う方法だ。

再帰モジュールを使う方法

先程定義しようとした型の問題は、相互再帰的な多相バリアントで、定義の完了していない型を参照しようとしたことだった。

再帰モジュールを使う方法では、型自体はばらばらに定義しておき、再帰部分をモジュールレベルに追い出すことにする。

module type S = sig
  module T : sig
    type t
  end

  open T
  type atom =
    [ `Symbol of string
    | `Vector of t array
    ]
  type t =
    [ atom
    | `List of t list
    | `DottedList of t list * atom
    ]
end

module rec M : (S with module T := M) = M

let xs : M.t = `List [`Symbol "a"]
let ys : M.t = `DottedList ([`Symbol "a"], `Symbol "b")
(*
let bad : M.t = `DottedList ([`Symbol "a"], `List [`Symbol "b"])
Error: This expression has type [> `List of [> `Symbol of string ] list ]
       but an expression was expected of type M.atom
       The second variant type does not allow tag(s) `List
 *)

モジュール型 S で、内部モジュール T に t 型があるものとしておき、最終的に欲しい t 型と atom 型はこれを使って定義するようにしておく。これだけでは、定義される型は再帰的な定義にならないので、 with module をつかって T の実体が自分自身を指すようにする³。

`DottedList の末尾に M.atom 型の値以外を入れようとすると型エラーになるようにできた。

ただし、現在（OCaml 4.08以降。この記事の時点で最新の4.11も）は Do not allow recursive modules in with module by lpw25 · Pull Request #1626 · ocaml/ocaml の変更で、モジュール型制約の with module の右辺で再帰モジュールが使えなくなってしまったため、この方法はもう使えない。

OCaml 4.07.1での M のシグネチャ:

module rec M :
  sig
    type atom = [ `Symbol of string | `Vector of M.t array ]
    type t =
        [ `DottedList of t list * atom
        | `List of t list
        | `Symbol of string
        | `Vector of M.t array ]
  end

OCaml 4.08.0 でコンパイルした場合:

18 | module rec M : (S with module T := M) = M
                                        ^
Error: Illegal recursive module reference

補助的な型を使う方法

補助的な型使う方法も方針は同じで、再帰部分を他の型に追い出し、その型経由でばらばらに定義した型を組み合わせる。違うのは、型パラメータで型を組み合わせることだ。

再帰モジュールの方で t を外に出していたので、それを型パラメータにする。

type 't atom =
  [ `Symbol of string
  | `Vector of 't
  ]

type 't s =
  [ 't atom
  | `List of 't list
  | `DottedList of 't list * 't atom
  ]

type t = t s

let xs : t = `List [`Symbol "a"]
let ys : t = `DottedList ([`Symbol "a"], `Symbol "b")
(*
let bad : t = `DottedList ([`Symbol "a"], `List [`Symbol "b"])
16 | let bad : t = `DottedList ([`Symbol "a"], `List [`Symbol "b"])
                                               ^^^^^^^^^^^^^^^^^^^
Error: This expression has type [> `List of [> `Symbol of string ] list ]
       but an expression was expected of type t atom
       The second variant type does not allow tag(s) `List
 *)

上記の型パラメータ 't が再帰用のパラメータで、その型を経由して再帰をする。 t 型が型定義の実体で、ここで自分自身を参照することで再帰を実現する。

こちらも、 `DottedList の末尾に t atom 型な値以外を入れようとすると型エラーになる。

この例では再帰する型は t だけなのでそのまま渡しているが、複数の型で相互再帰する場合には、関連する型をタプルやオブジェクトに詰めてパラメータとして渡すと型パラメータをひとつにまとめられて便利だ。

例えば、上では 't のみを型パラメータで渡しているが、（必要もなく） 'atom も型パラメータで渡すようにすると、

type ('t, 'atom) atom_ =
  [ `Symbol of string
  | `Vector of 't
  ]

type ('t, 'atom) s =
  [ ('t, 'atom) atom_
  | `List of 't list
  | `DottedList of 't list * 'atom
  ]

type t = (t, atom) s
and atom = (t, atom) atom_

のように、型パラメータが増えてしまうが、オブジェクト型と constraint を使うと、下のように型パラメータをひとつにまとめられる。

type 'dict atom =
  [ `Symbol of string
  | `Vector of 't
  ] constraint 'dict = <t: 't; atom: 'atom>

type 'dict s =
  [ 'dict atom
  | `List of 't list
  | `DottedList of 't list * 'atom
  ] constraint 'dict = <t: 't; atom: 'atom>

type dict = <t : dict s; atom : dict atom>
type t = dict s

こちらの方法は現在のOCamlでも問題なく使える。

追記: さらに短かく

と、最初は type t = t s のあたりで満足していたのだけれど、この s はそのまま展開してしまえるのだった。

type 't atom =
  [ `Symbol of string
  | `Vector of 't
  ]

type t =
  [ t atom
  | `List of t list
  | `DottedList of t list * t atom
  ]

これなら、当初の書きたかった定義とほぼ同じ長さなので使うのにも抵抗がない。

謝辞

この記事の内容は @zehnpaard さんとtwitterでお話しているうちに生まれたものです。ありがとうございます。

zehnpaardさんの記事: OCamlでの相互再帰的なPolymorphic Variantに関するメモ - Arantium Maestum

---

1. 真正リストと処理が共通化しにくくなるが、真正リストを期待しているところにドットリストが来てそれが最後になってわかるよりは、最初から分けてしまった方が便利だと思う。 ↩

2. atom の定義を t の中に展開すれば通るが、メンテナンス性が下がるのでやりたくない。 ↩

3. シグネチャ部分の括弧は必要ないが、 module rec M : S with module T := M = M だと目が滑るので読みやすさのために括弧をつけた。 ↩