GADTで実行時型情報を表現する

Java には実行時にも型情報があるので、下のような、型だけ見ると引数をそのまま返すように見せかけて、 `String` に対してのみ `null` を返すようなメソッドが書ける。

```java
class Hoge {
    public static <A> A foo(A x) {
        if (x instanceof String)
            return null;
        return x;
    }

    public static void main(String[] args) {
        System.out.println(foo("Hello"));      // -| null
        System.out.println(foo(42));           // -| 42
        System.out.println(foo(new Object())); // -| java.lang.Object@15db9742
    }
}
```

この例については、静的型から予想される挙動を裏切るようなプログラムが書けるだけで何も嬉しくないけれど、時には実行時型情報が便利な場合もある。

## 型を表す値

世の中には実行時型情報のあるジェネリクスを「真のジェネリクス」などと呼ぶ界隈もあるそうだけれど、 OCaml は、ジェネリクス（パラメトリック多相）に限らず、（現在の処理系では）実行時には型情報がすべてなくなってしまう。

だが、 OCaml 4.00 から導入された GADT（[Generalized Algebraic Data Type](https://en.wikipedia.org/wiki/Generalized_algebraic_data_type)。一般化代数データ型）を使うと実行時型情報を安全に表現することができる。

まずは**型を表す値**の型を GADT で定義する。

```ocaml
type _ typ =
  | Unit : unit typ
  | Int : int typ
  | Float : float typ
  | String : string typ
  | Pair : ('a typ * 'b typ) -> ('a * 'b) typ
  | Arrow : ('a typ * 'b typ) -> ('a -> 'b) typ
```

`a typ` 型の値は `a` 型の実行時型情報を表現する値で、それぞれのデータコンストラクタ `Unit`, `Int`, ... がそれぞれ `unit` 型、 `int` 型、……の型情報を表現する。

ふつうの代数データ型（OCaml のバリアント型）とは異なり、コンストラクタごとに `a typ` の型変数 `a` を異なる型に具体化することができる。また、 `Pair` や `Arrow` はそれぞれ、ある型 `'a`, `'b` に対して `('a * 'b) typ` や `('a -> 'b) typ` のように、コンストラクタごとに型変数を持つことができる。

## 実行時型情報で分岐する

次に、 実行時型情報を使う関数を定義する。 `a typ` 型の値は `a` 型の値に暗黙に付加されるものではないので、自分で陽に渡してやる必要がある。

```ocaml
let foo : type a. a typ -> a -> a =
  fun ty v ->
    match ty with
    | Int -> 42
    | _ -> v

let () =
  Printf.printf "%d\n" @@ foo Int 30;          (* -| 42 *)
  Printf.printf "%f\n" @@ foo Float 30.0;      (* -| 30.000000 *)
  Printf.printf "%s\n" @@ foo String "foobar"; (* -| foobar *)
  ()
```

関数 `foo` はある型 `a` に対して `a typ` で表現される型情報と `a` 型の値を受け取り、引数をそのまま返す。ただし、 `a` = `int` の場合は常に `42` を返す。

GADT は別名に equality-qualified type とあるように、内部に等式を持っている。 `a typ` 型の値では、 `Unit` なら `a` = `unit` だし、 `Int` なら `a` = `int` だ。 `a typ` 型の値をパターンマッチすると、この等式で静的型情報が詳細化される。そのため、上の `foo` の `| Int ->` の右側では `a` は `int` であることがわかっているので、 `42` という `int` 型の値を返すことができる（Java の例では、 `x` の実行時型情報が `String` であることがわかっても、静的型情報は変化しないので、 `null` 以外の `String` として意味のある値は返せない（と思う））。 `_ ->` の方では、型情報は詳細化されず、 `a` 型の値は引数以外ないので、それをそのまま返すことしかできない。

Java で暗黙に渡っていた型情報は、引数として陽に渡ってくるようになったので、型を見ただけで、 `foo` は実行時型情報を使うことがわかるようになった。

`foo` の呼び出し側で `foo Float "a"` のように型情報と異なる値を渡そうとしたり、実装側で（詳細化された） `a` と異なる値を返そうとすると、型検査時にエラーになる。また、 `a typ` 型のパターンマッチで、取り得る実行時型を網羅していないとコンパイル時に警告される。網羅的に実行時型検査することをコンパイル時に強いられるのだ（！）。

もうひとつ、 OCaml を使い始めたときに多くの人が悩む、任意の型の値の文字列化も（一応）書ける。

```ocaml
let show_typ typ =
  let rec show : type a. a typ -> bool -> string =
    fun ty paren ->
      let p x = if paren then Printf.sprintf "(%s)" x else x in
      match ty with
      | Unit -> "unit"
      | Int -> "int"
      | Float -> "float"
      | String -> "string"
      | Pair (ty1, ty2) ->
          p @@ Printf.sprintf "%s * %s" (show ty1 true) (show ty2 true)
      | Arrow (ty1, ty2) ->
          p @@ Printf.sprintf "%s -> %s" (show ty1 true) (show ty2 false)
  in show typ false

let rec show : type a. a typ -> a -> string =
  fun ty v ->
    match ty with
    | Unit -> "()"
    | Int -> string_of_int v
    | Float -> string_of_float v
    | String -> v
    | Pair (ty1, ty2) ->
        Printf.sprintf "(%s, %s)" (show ty1 @@ fst v) (show ty2 @@ snd v)
    | Arrow (ty1, ty2) ->
        Printf.sprintf "<fun> : %s" @@ show_typ ty

let ( %* ) x y = Pair (x, y)

let ( @-> ) x y = Arrow (x, y)

let () =
  let f g = g 1 in
  Printf.printf "%s\n" @@ show Int 0;   (* -| 0 *)
  Printf.printf "%s\n" @@ show (Int %* String @-> Int) fst; (* -| <fun> : (int * string) -> int *)
  Printf.printf "%s\n" @@ show (Int @-> Int @-> Int) (+);   (* -| <fun> : int -> int -> int *)
  Printf.printf "%s\n" @@ show ((Int @-> Int) @-> Int) f;   (* -| <fun> : (int -> int) -> int *)
  Printf.printf "%s\n" @@ show_typ ((Int %* Int) %* Int);   (* -| (int * int) * int *)
  Printf.printf "%s\n" @@ show_typ (Int %* (Int %* Int));   (* -| int * (int * int) *)
  ()
```

型情報を渡すところが面倒だけれど、ここは暗黙の引数が OCaml に導入されるのを待ちたい。

## 動的型を真似する

ここまでは値と型情報を別々に扱っていたが、 GADT を使うと、動的型付き言語のように値自体に型情報を持たせ実行時にその型で分岐するようなプログラムも書ける。

まずは型の等しさを判定する関数を定義する。

```ocaml
type (_, _) eq = Eq : ('a, 'a) eq

let rec eq_typ: type a b. a typ -> b typ -> (a, b) eq option =
  fun a b ->
    match a, b with
    | Unit, Unit -> Some Eq
    | Int, Int -> Some Eq
    | Float, Float -> Some Eq
    | String, String -> Some Eq
    | Pair (a1, a2), Pair (b1, b2) ->
        begin match eq_typ a1 b1, eq_typ a2 b2 with
        | Some Eq, Some Eq -> Some Eq
        | _ -> None
        end
    | Arrow (a1, a2), Arrow (b1, b2) ->
        begin match eq_typ a1 b1, eq_typ a2 b2 with
        | Some Eq, Some Eq -> Some Eq
        | _ -> None
        end
    | _ -> None
```

ここで、 `eq_typ` の戻り値型は `bool` にはでき**ない**。 `bool` はあくまで実行時の真偽を表す値で、型の等しさという型検査時の静的な情報は持っていない。ふたつの型の等しさを GADT の `eq` 型で表現し、等しい場合はそれを `Some` でくるんで返し、そうでない場合は `None` を返す。

`eq_typ` の実装中には `Some Eq` が複数現れるが、それぞれ異なるものであることに注意。例えば、 `| Pair (a1, a2), Pair (b1, b2) ->` の分岐の `| Some Eq, Some Eq -> Some Eq` の最初の `Some Eq` は、ペアの第一要素の型が等しいことを表わす値であり、ふたつ目のものは第二要素の型が等しいことを表す。それらをもとに最後の `Some Eq` でペア全体の型が等しいことを表す。部分の `eq_typ` の戻り値をパターンマッチして型環境を詳細化しつつ、詳細化された型環境で `Eq` を書くことで、全体の等しさを示す。

さらに、実行時型情報と値を組にした値を定義する。

```ocaml
type dyn = Dyn : 'a typ * 'a -> dyn

let try_cast : type a. a typ -> dyn -> a option =
  fun typ (Dyn (ty, v)) ->
    match eq_typ typ ty with
    | Some Eq -> Some v
    | None -> None
```

`dyn` は存在型（existential type）で実際の型を隠蔽する。 `'a` の部分が外に表れないので、異なる型の値をまとめて扱うことができる。

`dyn` で包まれた値を使うには `try_cast` で適当な型にキャストしてから使う。

```ocaml
let dyn_int_plus x y =
  match try_cast Int x, try_cast Int y with
  | Some a, Some b -> Dyn (Int, a + b)
  | _, _ -> invalid_arg "dyn_int_plus: arguments must be int"
```

OCaml の標準ライブラリの [`Marshal.from_string`](http://caml.inria.fr/pub/docs/manual-ocaml/libref/Marshal.html#VALfrom_string) は `string -> int -> 'a` という危ない型をしている（例えば、 `(int * string)` を `Marshal.to_string` したものを `(float * string)` に `Marshal.from_string` することもできてしまう）のだが、常に `dyn` 型を経由することにすれば、型安全にマーシャリングをすることができる。

```ocaml
let marshal_to_string: type a. a typ -> a -> string =
  fun ty v ->
    Marshal.to_string (Dyn (ty, v)) []

let unmarshal_from_string: type a. a typ -> string -> a option =
  fun ty s ->
    try_cast ty @@ Marshal.from_string s 0

let () =
  let t1 = Int %* String in
  let t2 = Float %* String in
  let b = marshal_to_string t1 (42, "foo") in
  let pr t = function
    | Some v -> Printf.printf "Some %s\n" @@ show t v
    | None -> print_endline "None"
  in
  pr t1 @@ unmarshal_from_string t1 b;  (* -| Some (42, foo) *)
  pr t2 @@ unmarshal_from_string t2 b   (* -| None *)
```

## もっと実行時型情報

先程の `show` は分岐を関数内に持っていたが、それを [`Hashtbl.t`](http://caml.inria.fr/pub/docs/manual-ocaml/libref/Hashtbl.html#TYPEt) のようなデータ構造内に持つこともできる。

```ocaml
type dtyp = Dtyp : 'a typ -> dtyp

let tbl : (dtyp, dyn) Hashtbl.t = Hashtbl.create 16;;
```

型としては、 `Hashtbl.t` のキーと値、それぞれの対応関係について、ある型 `a` が存在して、 `a typ` と `a -> string` の組であればよいような気がするが、 `Hashtbl.t` ではそのような型の関係を表現することはできない。そもそも `Hashtbl.t` の実装は GADT のことは何も知らない。

キーの方も `'a typ` の外に出ている型変数が邪魔なので、それを内側に隠す `dtyp` 型を定義する（もっとよい書き方がある？ 未考）。

キーと値の関係は `Hashtbl.t` の外側、ゲッターとセッターで保証することにする。実際に使うときは `tbl` を隠蔽すべきだろう。

```ocaml
let printer_ty x = x @-> String

let register_printer : type a. a typ -> (a -> string) -> unit =
  fun ty printer ->
    Hashtbl.add tbl (Dtyp ty) (Dyn (printer_ty ty, printer))

let get_printer : type a. a typ -> (a -> string) option =
  fun ty ->
    match Hashtbl.find tbl (Dtyp ty) with
    | v -> try_cast (printer_ty ty) v
    | exception Not_found -> None
```

## さらに先へ

今回の話は概ね [OCaml のリファレンスマニュアル](http://caml.inria.fr/pub/docs/manual-ocaml/)の GADT の節に載っている話である。

ここでは、 `unit`, `int`, `float`, `string`, 対、関数といった、 OCaml で扱える型のうちのごく一部だけを扱った。バリアントやレコード、オブジェクトといった、より多くの型を `a typ` 方式で表現する方法は [Runtime Types in OCaml](https://www.lexifi.com/files/resources/runtime_types.pdf) などを参照。 [OPAM](http://opam.ocaml.org/) に登録されている実行時型情報を扱うライブラリには [typerep](https://github.com/janestreet/typerep) 等がある。 [ppx_typerep_conv](https://github.com/janestreet/ppx_typerep_conv) は typerep の型情報を自動生成するライブラリである。

また、 OCaml で引数を暗黙に渡す研究については Modular Implicits などを参照。