OCamlでできるだけ型注釈を書かずに済ませる

これはAdvent Calendarとか関係なくなんとなく書かれた記事です。

ML系言語で型注釈が必要なケース - Qiita にある通り、OCamlには型注釈なしではコンパイルが通らないケースがいくつかある。

そのような場合でも、別の書き方をすることで型注釈なしで済ませる/より少ない型注釈で済ませる方法を紹介する。

GADTs

type 'a t =
  | Int : int -> int t
  | Bool : bool -> bool t

let f : type a. a t -> int -> bool = fun t y -> match t with
  | Int x -> y >= 2
  | Bool x -> x

このケースでは、型注釈を付けないと、 Int x の時点で f の型が int t -> int -> bool に確定してしまい、 Bool x : bool t ≠ int t で型エラーになってしまう。

これについては、型注釈をなくすことはできないが、Locally abstract typesのpolymorphic syntaxは必要ないので、もう少し見た目を軽くすることはできる。

let f (type a) (t : a t) y = match t with
  | Int x -> y >= 2
  | Bool x -> x

ただし、GADTsを使っているとすぐに多相再帰が必要になるので、polymorphic syntaxで書いておいた方が無難な気はする。

多相再帰

パラメトリック多相な再帰関数で、再帰呼び出し時に異なる型パラメータで自身をインスタンス化するようなものを多相再帰と呼ぶ。下の例で言うと、 depth は呼び出し時は 'a を α でインスタンス化するが、 Nested のケースでは 'a を α list でインスタンス化しようとする。

これは、型注釈もなくせないし、多相型アノテーションを付けるしかない。多相再帰の型推論は決定不能なことが知られている。

type 'a fuga =
  | Leaf of 'a
  | Nested of 'a list fuga

let rec depth : 'a. 'a fuga -> int = function
  | Leaf _ -> 0
  | Nested y -> 1 + depth y

追記: 再帰モジュールやレコードを使う方法

多相型アノテーション以外に再帰モジュールを使う方法もある。

module rec M : sig
  val depth : 'a fuga -> int
end = struct
  let rec depth = function
    | Leaf _ -> 0
    | Nested y -> 1 + M.depth y
end

ただし、再帰モジュールはexperimetal extensionなので、何かが起こったときに自分でどうにかできる人にしかオススメできない。

他にも、下記のようにレコードの多相フィールドを使う方法や、オブジェクトの多相メソッドを使う方法もあるが、記述量的にも多相型アノテーションを使う方が無難だろう。

type depth = { f: 'a. 'a fuga -> int }

let rec depth t =
  let rec d = { f = function
    | Leaf _ -> 0
    | Nested y -> 1 + d.f y
  } in
  d.f t

フォーマット文字列

OCamlでは、文脈上 ('a, 'b, 'c) format 型（format4 や format6 型も含む）の値が求められる場所に書かれた文字列リテラルはフォーマット文字列扱いになる。

これは、 対話環境で以下のようにすると確認できる（OCaml 4.02 からフォーマット文字列の内部表現がGADTsになったのでそれが見えている）。

utop # let s : ('a, 'b, 'c) format = "%s = %d";;
val s : (string -> int -> 'c, 'b, 'c) format =
  CamlinternalFormatBasics.Format
   (CamlinternalFormatBasics.String (CamlinternalFormatBasics.No_padding,
     CamlinternalFormatBasics.String_literal (" = ",
      CamlinternalFormatBasics.Int (CamlinternalFormatBasics.Int_d,
       CamlinternalFormatBasics.No_padding,
       CamlinternalFormatBasics.No_precision,
       CamlinternalFormatBasics.End_of_format))),
   "%s = %d")

ここでの 'a, 'b, 'c は型変数ではなくunification変数なので、多相性が足りないというようなエラーにはならない。 format のように型引数が複雑になる場合は、自分で型を全部書かずに型チェッカーに任せた方が楽だ。

'a, 'b, 'c を型変数にしたい場合は多相型アノテーションを使う。こちらは（もちろん）型エラーになる。

utop # let s : 'a 'b 'c. ('a, 'b, 'c) format = "%s = %d";;
Line 1, characters 40-49:
Error: This definition has type 'b 'c. (string -> int -> 'c, 'b, 'c) format
       which is less general than 'a 'b 'c. ('a, 'b, 'c) format

また、OCaml 4.03.0 から型コンストラクタの引数をまとめて _ で表現することができるようになったので、型注釈はもう少し短かくできる。

utop # let s : _ format = "%s = %d";;
val s : (string -> int -> 'a, 'b, 'a) format =
  CamlinternalFormatBasics.Format
   (CamlinternalFormatBasics.String (CamlinternalFormatBasics.No_padding,
     CamlinternalFormatBasics.String_literal (" = ",
      CamlinternalFormatBasics.Int (CamlinternalFormatBasics.Int_d,
       CamlinternalFormatBasics.No_padding,
       CamlinternalFormatBasics.No_precision,
       CamlinternalFormatBasics.End_of_format))),
   "%s = %d")

レコードフィールドやバリアント構成子

レコードフィールドやバリアント構成子の衝突を防ぐには、モジュールを使うのが常套手段だ。

module Hoge = struct
  type t = { foo : string; bar : int }
end

module Piyo = struct
  type t = { foo : int; bar : string }
end

open Hoge
open Piyo

(* module pathで修飾してどちらのフィールドかわかるようにする *)
let baz x = x.Hoge.foo

module Nyan = struct
  type t =
    | A
    | B
end

module Myon = struct
  type t =
    | A
    | C
end

open Nyan
open Myon

(* module pathで修飾してどちらの構成子かわかるようにする *)
let f = function
  | Nyan.A -> "yes"
  | Nyan.B -> "no"

古（2013年9月以前）のOCamlではこうやって衝突を回避するしかなかった。

OCaml 4.01.0 からtype based disambiguation（型に基づく曖昧性解消）が入ったので、型情報からどのレコードフィールド/バリアント構成子が使われているのかわかれば、module pathを省略できるようになった。

let baz2 (x : Hoge.t) = x.foo

let f2 : Nyan.t -> string = function
  | A -> "yes"
  | B -> "no"

type based disambiguation は値側からも働くので型注釈をなくすこともできる。

(* レコードのフィールドパターンはモジュール修飾できる。
   Hoge.fooで曖昧性解消されたので他のフィールド（bar）はHoge.なしで参照できる *)
let baz3 { Hoge.foo; bar = _ } = foo

let f3 = function
  | Nyan.A -> "yes"
  | B -> "no" (* Nyan.t だとわかっているのでNyan.Bでなくてよい *)

let f4 = function
  | B -> "no"
  | A -> "yes" (* BでNyan.tとわかるのでNyan.Aと書かなくてよい *)

ちなみに type based disambiguation は左から右に働くので、パターンの順番によってエラーになったりならなかったりする。

utop # let f_bad = function
  | A -> "yes" (* open MyonがあるのでこれはMyon.Aになる *)
  | B -> "no" (* BはMyon.tに含まれないのでエラー *)
;;
Line 3, characters 4-5:
Error: This variant pattern is expected to have type Myon.t
       The constructor B does not belong to type Myon.t

おまけ: Rank-N 多相

OCamlはRank-N 多相を直接サポートはしていないが、レコードやオブジェクトやfirst-class moduleのフィールドに多相な値を持つことができるので、間接的に表現することはできる。

type id = { f : 'a. 'a -> 'a }
let f id x y = (id.f y, id.f x)

let _ (* : string * int *) =
  f { f = fun x -> x } 1 "x"

class type id_obj = object method f : 'a. 'a -> 'a end
let f_obj (id : id_obj) x y = (id#f y, id#f x)

let _ (* : string * int *) =
  f_obj (object method f : 'a. 'a -> 'a = fun x -> x end) 1 "x"

module type ID = sig val f : 'a -> 'a end
let f_mod (module M : ID) x y = (M.f y, M.f x)

let _ (* : string * int *) =
  f_mod (module struct let f x = x end) 1 "x"

型注釈はこれ以上減らせない。理論上Rank-2多相までは推論可能なことが知られているが、Rank-3以上の推論は決定不能である。