OCamlのlocally abstract typeに関するメモ１ （基本的な疑問）
「EffectでState実装」の記事で何故Stateエフェクトのためにpolymorphic locally abstract typeが使われる必要があったのかを掘り下げたいと書いた。それに関して@dico_lequeさんからこのようにご教示いただいた（ありがとうございます！）：
loopの型が再帰呼び出しごとに変わるので多相型アノテーションが必要なのと（多相再帰は推論はできないけれど型アノテーションをつければ書ける）、導入した型変数を関数の本体部分でも参照するために局所抽象型が必要だから、かな
— でこれき (@dico_leque) December 26, 2022
明示的な多相の型注釈に関しては自分としても少しはわかるものの、そこにlocally abstract typesが加わるとなかなか追えなくなってしまうのはそもそもlocally abstract types自体の理解があやふやだからだと考えられる。なのでちょっと調べた。
まず公式リファレンスでの説明：
この文章何回か流し読みで読んだことがあるのだが、正直なところイマイチピンときていなかった。冒頭の文
The expression
fun ( type typeconstr-name ) -> exprintroduces a type constructor namedtypeconstr-namewhich is considered abstract in the scope of the sub-expression, but then replaced by a fresh type variable.
について、「なんでいきなりtype constructor？」「considered abstractってどういうこと？」「but thenっていつ？」などと気になる点を放置していたので仕方ない・・・ 今回の記事はこの三つの超基本的な疑問について。
（ちなみにこの公式リファレンスの説明は上記の「locally abstract typesとは何か」そして「locally abstract typesのさまざまな構文」「locally abstract typesはどういう時に使うものか」と論理的には三項目にわかれているのだが、文章構成的にはわかりにくい気がする・・・ 例えば「This construction is useful because ...」で始まる文が直前に論じられていた構文についてではなくてlocally abstract typeすべてについて語っているということは、ある程度読み進めないと判断できない）
Locally abstract typesについての話題はReal World OCamlでも「First Class Modules」の章で出てくる：
こちらでは実例を伴ってよりわかりやすく説明されている：
One of the key properties of locally abstract types is that they’re dealt with as abstract types in the function they’re defined within, but are polymorphic from the outside. Consider the following example:
let wrap_in_list (type a) (x:a) = [x];; val wrap_in_list : 'a -> 'a list = <fun>
The type a is used in a way that is compatible with it being abstract, but the type of the function that is inferred is polymorphic.
If, on the other hand, we try to use the type a as if it were equivalent to some concrete type, say, int, then the compiler will complain.
let double_int (type a) (x:a) = x + x;; Line 1, characters 33-34: Error: This expression has type a but an expression was expected of type int
ちなみにabstract typeについての公式な解説はこれが良さそう：
Abstract type: no equation, no representation. When appearing in a module signature, this definition specifies nothing on the type constructor, besides its number of parameters: its representation is hidden and it is assumed incompatible with any other type.
これを踏まえて基本的な疑問に答えると：
Q: considered abstractってどういうこと？
A: Moduleによって隠蔽されたabstract typeと同じで、他の型と単一化してはいけない独立した型として扱う
Q: "but then replaced by a fresh type variable"の"but then"っていつ？
A: 関数のスコープから出たら。ある関数内で(type t)というlocally abstract typeが導入されている場合、関数外からはその関数の型においてtがすべて型変数'tに置き換えられている（ただし'tはフレッシュな型変数とする）
となる。
残っている「なんでいきなりtype constructor？」という質問に関しては以下のRedditスレッドでGabriel Scherer(gasche)が答えていた：
The OCaml type language distinguishes type variables, like 'a, and type constructors, like t, or list (a parametrized constructor that is not a valid type expression in itself). ... The type-checker would not know how to introduce equations on type variables, and adding this would be a sizeable/invasive change, so we rely on locally-abstract types instead, which are basically constructors that feel like variables.
なるほど・・・ struct type t = int endでtのことを型変数と呼びたくなってしまうが、正確にはこれはtype constructorであってtype variableではない。確かにTaPLでもそんな用語の使い方だったな・・・。type variableはあくまで'aのように単一化（あるいは汎化）を待つものなわけだ。ここら辺はType ConstructorとType Variableのリファレンスにも詳しい。
次回はlocally abstract typeの構文とユースケースについて見ていく。
