この記事はML Advent Calendar 2020 5日目の記事です。
OCamlにそろそろ入りそうな機能を紹介します。
今回は、Allow to name existentials in pattern-matching by garrigue · Pull Request #9584 · ocaml/ocaml を紹介します。
OCamlでは（他の言語でも同じように？）、言語機能が追加されたときに、処理系は正しく型づけするが、ユーザーが項の型を書けなかったり、かなりまわりくどい書き方をしないと型を明示できないことがたまに起こる。過去に第一級モジュールが追加されたときにも、何かユーザーがうまく型を書けないケースがあったような気がする（あやふや）。
今回紹介するAllow to name existentials in pattern-matching by garrigue · Pull Request #9584 · ocaml/ocamlは、パターンマッチ時にGADTで導入される存在型を参照するための構文を追加する。
具体例で説明しよう。
OCamlには存在型を扱う構文がふたつある。
ひとつはモジュールで、「ある型tと、その値value」をシグネチャで表現すると次のようになる。
module type S = sig
type t
val value : t
end
もうひとつはGADTで、同様のものを表現すると次のようになる。
type t = Value : 'a -> t
前者から後者への変換は簡単で、次のような関数で書ける。
let module s_to_t (module M : S) = Value M.value
逆はけっこう面倒だ。
単純に考えると次のようになりそうだが、これは型チェッカーに文句を言われる。
let t_to_s = function
| Value (v : 'a) ->
(module struct
type t = 'a
let value = x
end : S)
(*
11 | | Value (v : 'a) ->
^^^^^^^^
Error: This pattern matches values of type 'a
but a pattern was expected which matches values of type $Value_'a
The type constructor $Value_'a would escape its scope
*)
これは、 v の型は Value の分岐でしか使えないはずなのに、 'a は function 全体がスコープになることが原因だ。
今はこんな風に書く必要がある。
let t_to_s = function
| Value v ->
let f (type a) (x : a) =
(module struct
type t = a
let value = x
end : S)
in
f v
ここでは、一旦ローカル関数で局所抽象型 a を導入し、それを使って第一級モジュールをつくっている。
これはあまりにも面倒なので、Allow to name existentials in pattern-matching by garrigue · Pull Request #9584 · ocaml/ocamlでは、次のように書ける構文を導入する。
let t_to_s = function
| Value (type a) (v : a) ->
(module struct
type t = a
let value = x
end : S)
ちょうど、最初のプログラムと局所抽象型を使ったプログラムの間の子のような感じで、GADTで導入される存在型を (type a) の形でバリアントタグのあとに書けるようになる。
次のOCaml 4.12は既にfeature freezeされているので、この機能は4.13あたりで入るだろう。