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

これは[ML Advent Calendar 2020](https://qiita.com/advent-calendar/2020/ml)の1日目の記事です。

----

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

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

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

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

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

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

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

```ocaml
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` の後ろにはアトムしか来られないようにすることが考えられる。

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

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

```ocaml
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` というエラーでコンパイルが通らない[^no-dup]。多相バリアントを拡張する場合、拡張される側の型は、参照される時点で定義が完了していないといけないからだ。

このあたりを調べていると、 [Correct mutually recursive types are rejected by the type-checker · Issue #8511 · ocaml/ocaml](https://github.com/ocaml/ocaml/issues/8511) というissueに行きあたる。

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

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

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

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

```ocaml
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` の実体が自分自身を指すようにする[^note-sig]。

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

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

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

```ocaml
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` を外に出していたので、それを型パラメータにする。

```ocaml
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` も型パラメータで渡すようにすると、

```ocaml
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` を使うと、下のように型パラメータをひとつにまとめられる。

```ocaml
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` はそのまま展開してしまえるのだった。

```ocaml
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](https://zehnpaard.hatenablog.com/entry/2020/11/26/081131)

[^no-dup]: `atom` の定義を `t` の中に展開すれば通るが、メンテナンス性が下がるのでやりたくない。
[^note-sig]: シグネチャ部分の括弧は必要ないが、 `module rec M : S with module T := M = M` だと目が滑るので読みやすさのために括弧をつけた。