OCamlのGADTでVariadic Function（Stack Overflowより）

このStack Overflow問答が大変面白かったのでメモ：

サンプルコードは少し（自分にとっては）わかりやすいように変えてある。

何をしたいか

第一引数によって、それ以降幾つの引数をとるかが変化するような可変長引数関数を書きたい。

例えば

let g = f 1;;
val g : int -> string = <fun>

let h = f 2;;
val h : int -> int -> string = <fun>

のような関数fが書けるだろうか？

結論から言ってしまえば、このように「引数の数がintの値に依存するような関数」は書けない。（それこそ依存型の出番じゃないか？）

しかし第一引数にGADTな値を当てることで引数の数をコントロールすることはできる。

GADT

というわけで引数の数を表すGADTを定義してみる：

type input = int
type output = string

type _ arity =
  O : output arity
| I : 'a arity -> (input -> 'a) arity

各引数の型であるinputと最終的な出力の型outputを使ってGADTの_ arityを定義していて、例えばI (I O)という値は(input -> input -> output) arityという型になる。ADTの値によって多引数な関数の型が表されているのがわかる。

複数のinput型引数をまとめるアキュミュレータに当たるデータの型accと、そのアキュミュレータの初期値acc_init、逐次アキュミュレートするための関数accumulate、そして最終的にoutput型に変換して返すための関数processを定義する：

type acc = int list

let acc_init = []
let accumulate x xs = x::xs
let process xs = string_of_int @@ List.fold_left (+) 0 xs

これらを使って可変長引数関数を作れる。

まずはアキュミュレータを明示的に使ったf_auxを定義し、それとacc_initを使ってfを定義する：

let rec f_aux : type f. acc -> f arity -> f =
  fun acc arity -> (match arity with
    O -> process acc
  | I a -> (fun x -> f_aux (accumulate x acc) a))

let f arity = f_aux acc_init arity

f_auxではlocally abstract type（かつpolymorphic syntax）を使ってacc -> f arity -> fな関数型を定義している。これでI (I O) : (int -> int -> string)な値を渡されればint -> int -> stringな関数（つまりint型の引数を２つとってstringを返す関数）を返すような高階関数ができる。

使ってみる：

utop # let g = f (I O);;
val g : input -> output = <fun>

utop # let h = f (I (I O));;
val h : input -> input -> output = <fun>

成功。

モジュール化

OCamlなのでモジュール・ファンクタで抽象化してみる。

まずはファンクタの引数のシグニチャ：

module type S = sig
  type input
  type output

  type acc
  val acc_init : acc
  val accumulate : input -> acc -> acc
  val process : acc -> output
end

引数のモジュールは

引数と戻り値の型
複数の引数をどう集めてどう最終的に変換するのか

を提供することになる。

ファンクタ本体：

module F (X : S) = struct
  include X
  
  type _ arity =
  | O : output arity
  | I : 'a arity -> (input -> 'a) arity

  let rec f_aux : type f. acc -> f arity -> f =
    fun acc arity -> (match arity with
      | O -> process acc
      | I a -> (fun x -> f_aux (accumulate x acc) a))

  let f arity = f_aux acc_init arity
end

ファンクタ部分にtype _ arityとf_aux/fを入れているので、可変長引数に関する部分はすべてファンクタ側で持っている。

とりあえず先ほどの例と同じintとstringでやってみる：

module M = struct
  type input = int
  type output = string

  type acc = int list
  let acc_init = []
  let accumulate = List.cons
  let process xs = string_of_int @@ List.fold_left (+) 0 xs
end

module MV = F(M)

使ってみる：

utop # let g = let open MV in f (I O);;
val g : int -> string = <fun>

utop # let h = let open MV in f (I (I O));;
val h : int -> int -> string = <fun>

成功。

これで引数・戻り値の型と複数の引数の組み合わせ方をモジュールで定義すれば、あとはファンクタ適用だけで可変長引数な関数を作成できるようになった。

GADTの限界

限界というと言い過ぎかもしれないが、GADTを使って可変長引数を実現したとしても「引数の数は静的に解決できなくてはいけない」という制約は残る。つまり実行時にI (I (I O))のような任意の値を構築してfに渡してやるようなことはできない。

let make_arity n =
  if n = 0 then O
  else if n = 1 then I O
  else if n = 2 then I (I O)
  else if n = 3 then I (I (I O))
  else failwith "n out of range in make_arity"

のような関数を書いたとして

Line 3, characters 21-24:
Error: This expression has type (input -> 'a) arity
       but an expression was expected of type output arity
       Type input -> 'a is not compatible with type output

こんな感じに怒られてしまう。

ポイントはmake_arityの型がint -> ??? arityになってしまうこと。OとI OとI (I O)とI (I (I O))はすべて型が違うので、同じ型の引数で戻り値の型を変えられないのでmake_arity関数は定義できない。

それでもこの手法は実際にPrintfなどの実装で役に立っているらしい（詳細は元のStack Overflow記事を参照）。GADTの利用法についてはもっといろいろと調べていきたい。

Arantium Maestum

プログラミング、囲碁、読書の話題

OCamlのGADTでVariadic Function（Stack Overflowより）

何をしたいか

GADT

モジュール化

GADTの限界