高カインド型・高階多相についてのメモ
前回に続いてカインドについてのメモ。
TaPLとともに、"Functional Programming with Overloading and Higher-Order Polymorphism"という資料をかなり参考にしている。
高カインド型
高カインド型（Higher Kinded Types）については以下のStack Overflowの返答が非常にわかりやすかった。
ちなみに回答者がF-ing Modulesの著者Andreas Rossbergだ。
- int, bool listなどのproper type（０引数型コンストラクタ）はカインド
*を持ち、このカインドは0階だと考えられる - list, (,)など、1以上の引数を持ち、かつすべての引数のカインドが*な型コンストラクタ（
*=>*=>...=>*のようなカインドを持つ)は一階。*=>*も*=>*=>*も同じ一階であることに注意 - 一階カインドな型を一つでも引数にとる（＆二階以上のカインドな型は一つも引数としてとらない）型コンストラクタが二階。例えば
(*=>*)=>* - 二階カインドな型を一つでも引数にとる（＆三階以上のカインドな型は一つも引数としてとらない）型コンストラクタが三階。例えば
((*=>*)=>*)=>* - 以下同
二階以上のカインドを持つ型コンストラクタのことを高カインド型と呼ぶ。
OCamlのCore言語で無理やり例を書くとしたら：
type t = int (* 0階 *) type 'a u = 'a list (* 1階 *) type 'a v = int 'a (* 2階 *) type 'a w = list 'a (* 3階 *)
tは型パラメータなしの普通の型。uはなんらかのproper typeのリスト。vはlistやoptionなどの型コンストラクタをとり、int list、int optionなどその型コンストラクタをintに適用した型となるようなコンストラクタ。wはvのような「型コンストラクタをとる型コンストラクタ」をとって、listを引数として渡してできる型を返す。例えばv w = int listになる。
ただし上記の例は2階以降はOCamlではエラー。OCamlのCore言語では型コンストラクタに型コンストラクタを渡すことはできない（例えばlistにint optionは渡せるが、optionそのままはどんなコンストラクタにも渡せない）。
モジュール言語でエンコードすることはできそうだが、カインドに十分な制約をつけることができるかは試してみないとわからない・・・。
正直高カインド型もこれだけでは何が嬉しいのかよくわからない。TaPLにも
Unlike higher-order functions at the term level, which are often extremely useful, higher-order type operators are somewhat esotoric.
と書いてある。ただし32章の関数型オブジェクト指向の話では
What we achieve ... is a separation of the varying part (the method interface), where we want to allow subtyping, from the fixed skeleton of objects (the existential packaging, and the pair of state and methods), where we do not because it gets in the way of the repackaging.
We need bounded quantification over a type operator to achieve this splitting because it allows us to pull out the method interface from an object type, even though the interface mentions the existentially bound state type X, by abstracting the method interface itself on X. The interface thus becomes a "parametric parameter".
とあり、ここでは型コンストラクタを引数にとる型コンストラクタが利用されている。
高階多相
TaPLでHigher Order Polymorphismと呼ばれているのはf :: ∀F.∀X.F X -> Intのような多相関数（あるいはそれを可能とする型システム）。
つまり任意のカインド*=>*の型コンストラクタFと、任意のカインド*の型Xに対してF X -> Int型になるような関数が定義できるか、ということ。
f [1;2;3]もf (Some "string")もf (Id ())もすべて型検査を通ってしっかり評価される必要がある。
上記の"Functional Programming with Overloading and Higher-Order Polymorphism"によると型検査でこのような拡張をサポートするのはそう難しくないとのことだ。より重要なのは、どのような実装ならこれが正しく型検査を通るのか、という点。
結論から言ってしまえば、型クラスなどのアドホック多相機構がない場合、こういった高階多相関数は面白くならない。f :: ∀F.∀X.F X -> Intだとfは引数の値に関わらず同じ整数を返す定数関数か、必ずエラーを投げる（ので返り値の型が何でもいい）関数のどちらかにしかなれない。
高階多相が面白くなるのはアドホック多相と組み合わせてから、という話が"Functional Programming with Overloading and Higher-Order Polymorphism"の主眼なので、興味のある方はそちらも読んでいただきたい。今回その詳細は割愛する。ただし高階多相・高カインド型という用語がよく使われるコンテキストというのはHaskellやScalaでアドホック多相との組み合わせで、というのがほとんどなのでこの記事の内容では片手落ちな印象は否めない。
高階多相と高カインド型の定義をまとめると：
高階多相：特定の型システムの属性で、その型システム上で「引数１以上の型コンストラクタ」に対して多相な関数が表現できるか否か
高カインド型：「引数１以上の型コンストラクタ」を引数にとる型コンストラクタのこと
となる。高階多相は関数に、そして高カインド型は型コンストラクタに関する話だ。
高カインド型に対して多相でなくても、１引数の型コンストラクタに対して多相であれば一般的に高階多相だと言えるのがややこしいポイント。しかし高カインド型に対して多相であれば、その型システムは問題なく高階多相だと言っていい。
（これを書いていて「あれ、多相って関数だけじゃなくて型に対しても使う？型コンストラクタってそれ自体が多相？」とふと疑問を抱いた。この点に関しても別の記事で書きたいが、現在の自分のスタンスとしては、特殊な例を除いて「パラメトリック多相」というのは多相関数を許容する型システムのことで、型コンストラクタの存在は付随的かつ不十分だと考えている）
高階とランク・カインド
以前@kmizuさんがこういう記事を書いていた：
個人的に気になるのは、Let多相からシステムFに至るまでに既に「高ランク多相」に拡張している点。
つまり、Let多相で許容されるのは
∀X(X -> X)
のような型を持つ関数だが、ランク２多相になると
(∀X(X -> X))->Int
ランク３多相になると
((∀X(X -> X))->Int)->Bool
といった形の型が許容されるようになる。システムFはこの方向の極限で、どのようなランクの多相でも許容される。（ここらへんの話はImpredicative Typesの記事でも書いた）
これも一つの高階性なのでは？と思えるので、その点で高階多相という単語は何となく曖昧さがあるように感じてしまう。高ランク多相と高カインド多相と言ったほうが高階性の方向が定まっていていいのではないか、と素人考えでは思うのだが・・・
