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

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

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。一般化代数データ型）を使うと実行時型情報を安全に表現することができる。

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

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 型の値に暗黙に付加されるものではないので、自分で陽に渡してやる必要がある。

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 を使い始めたときに多くの人が悩む、任意の型の値の文字列化も（一応）書ける。

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 を使うと、動的型付き言語のように値自体に型情報を持たせ実行時にその型で分岐するようなプログラムも書ける。

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

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 を書くことで、全体の等しさを示す。

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

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 で適当な型にキャストしてから使う。

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 は string -> int -> 'a という危ない型をしている（例えば、 (int * string) を Marshal.to_string したものを (float * string) に Marshal.from_string することもできてしまう）のだが、常に dyn 型を経由することにすれば、型安全にマーシャリングをすることができる。

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 のようなデータ構造内に持つこともできる。

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 を隠蔽すべきだろう。

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 のリファレンスマニュアルの GADT の節に載っている話である。

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

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