高カインド型(Higher-Kinded Types; HKT)とその表記について勉強したのでメモ。高階関数を知っているレベルからHKTをどう表記するかまでメモする。プログラミング言語として主にScalaを用いているが、Scalaでしか分からない概念は極力排している。知ってる部分は飛ばしてよい。理解が間違っている箇所があったらブコメなどで教えてください。
追記: Higher-Kinded Typesという用語はちょっと奇妙な響きがありつつも使われていて、Kindという用語は型理論としてのちゃんとした用語とのこと。
まず用語がアレ、という話https://t.co/UkxfCy9OFq
— Kenji Yoshida (@xuwei_k) 2023年10月9日
自信ないけど、もし上記tweetで言及してるようにScalaが初？だとしたらblog内の「Scalaでしか分からない概念は極力排している」と言いつつ、blogタイトル実は当初Scala独自用語！(だけど他でも使われるようになった？)みたいな超面倒事情があり〜
Kindはもちろんですが、higher kindも、Scalaよりはるか昔からある型システム用語なのは確実です。ご参考まで。
— S (ﾂｲｰﾄはｽﾚｯﾄﾞ全体をご確認ください) (@esumii) 2023年10月10日
詳細はこちら。
高階性
プログラミング言語において、高階関数という概念がある。ふだん目にするような関数は「値を引数に取り、値を返す」ようなものだが、プログラミング言語の発展により「関数を引数に取ったり、関数を返したり」ができるようになった。これらの著名な例は、JavaScriptでも使えるsort()だ。sortは値を比較するために関数を1つ受け取り、その返り値によって並べ替えを行う。
[1,5,2,5,7].sort((a, b) => a - b); // => [1, 2, 5, 5, 7]
他にも配列の値全てに関数を適用するmapや、非同期処理を行うためのコールバックも、関数を関数に渡したり/もらったりすることで実現している技法だといえる。
このような、「関数を引数として受け取る関数」「関数を返す関数」を高階関数と呼ぶ。高階関数では、関数をあたかも値のように扱うことができる*1。
高階関数では値や関数が引数・返り値として錯綜し、自然言語では表現しづらいことから、多くの言語では関数の型を表現するための型記法を持っている。
例えばScalaの場合:
Intを受け取り、Stringを返す関数Int => String
DoubleとIntを受け取り、Stringを返す関数Double => Int => String
Intのリストと、Intを受け取りStringを返す関数を受け取り、Stringのリストを返す関数List[Int] => (Int => String) => List[String]
ここではざっくり、「X自体が、Xを引数・返り値として扱える」という性質のことを高階性と呼ぶことにする(厳密な定義ではない)*2。
型が引数を持つことがある
前項の例にも少し現れているが、型が引数のようなもの(型パラメータ)を持つことがある。例えばListはStringを渡すことで具体的な型として使えるようになる。他にもMapはキーとなる型と値となる型を渡すことでMap[Int, String]のような具体的な型になる。
List- このままでは普通の型として使えない
List<String>(Java) /List[String](Scala)- 具体的な型として使える
これは、型が関数のように「型がパラメータを取って型を返している」と考えることができる。ScalaやHaskellなどの関数型言語では、このような操作がよく見られる。関数型言語では一般に、型をパラメータに取って別の型を返すような型のことを型コンストラクタと呼ぶ(Scalaの場合「パラメータ化された型」がこれに相当する具体的な言語機能である)。型を組み立てて作るのでこのような名前になっている。型コンストラクタの例として、前述したListやMapに加えて、OptionやTupleなどが挙げられる。
型コンストラクタは、型を受け取って型を返すという点において、従来の関数に見立てることができる。
ここで、ListとList[String]などを区別していることに気を付けてほしい。List[String]は型パラメータを全て埋めきっているので普通の型である一方、Listは型パラメータを1つ取る型コンストラクタであって、具体的な普通の型ではない。
ある型が型コンストラクタで、型パラメータを取ることを明示すると便利であることから、型コンストラクタを表現するときはF[_, _]のようにアンダースコアを用いたプレースホルダを使って型パラメータの個数を表記することが多い。これは、「あるFという型は2つの型パラメータを受け取る型コンストラクタである」ことを表現している。
型においても高階性を考えることができる
さてここで高階関数のことを思い出そう。高階関数とは、「関数を引数や返り値として扱うことができる関数、またはそれが可能なプログラミング言語上の性質」のことであった。関数について高階関数を考えることができ、型コンストラクタが関数のようなものであるならば、型でも高階関数のようなことが行えないか？というのが今回の主題である。
言い換えると、「型コンストラクタを受け取り、型を返すような、型コンストラクタ」を考えられないか？ということである。そしてそれは存在しており、具体的には例えばFunctorという型クラスはFunctor[F[_]]というScalaの型表記で表現できる。これは、「型パラメータを1つ取るようななんらかの型コンストラクタを1つ受け取るような、Functorという型コンストラクタ」である。
このような高階的な型は型クラスという概念で非常にしばしば出現する。
Higher-Kinded Type (HKT)
型コンストラクタを取って型を返すといった、型における"高階関数"のことを、高カインド型(Higher-Kinded Type; HKT)と呼ぶ。このとき、高階関数でもそうであったように、そのHKTがどのような"形"の型をパラメータとして取るのかが関心事の一つになる。関数が織り成す"形"を表現するために型という存在があるように、HKTが織り成す"形"を表現するために、カインドと呼ばれる存在が導入される。カインドはこうだと直接表現するのは難しいので、どのように言葉を使うかを以下に示す:
- それ自体が型として使える普通の型
- 「プロパーなカインドを持つ型」「普通の型」
- いくつかの型パラメータをとる型コンストラクタ
- 「一階のカインドを持つ型」
- 型パラメータとして型コンストラクタを取るような型コンストラクタ
- 「高階カインドを持つ型(Higher-kinded type)、高カインド型」
具体的には、IntやString、Double => Stringは何らの型パラメータも取らないのでプロパーな型だ。MapやList、Tryはいくつかの型パラメータを取る型コンストラクタであり*3、カインドの用語を使うと「一階のカインドの型」だ。そしてCatsライブラリにおけるFunctorやArrow、FunctionKはこうした一階カインドの型をとる高階カインドの型だ。
良い図があったので以下のページから借用する。
カインドにおいては、型パラメータがどのように取られるかだけに関心が集中し、具体的な型が何であるかや型パラメータの数は完全に捨象されていることが特長だ。
カインドの記法
さて、カインドという概念があると「型自体の形」を表現することができて便利ということはわかった。特に型クラスといった技術は型を抽象化して扱いたいので、HKTがあると嬉しいのだ。
ところが、型でも同じことが起こったように、具体的なカインドをどう書いて表現すればよいのかが問題になってくる。「こういう感じの高階カインド型があって」と説明したいときに、便利な表記法がないと困る。
そういうわけで満を持してカインド記法が登場する(正式な名称は特にないが、「カインドの記法」「カインド記法」「*記法」などで通る)。カインド記法は以下のようにカインドを記述する:
- プロパーな型
*
- 一階の型 --
->で型コンストラクタを表現する- 例: 1つの型パラメータを取る場合
* -> *(List[_]など) - 例: 2つの型パラメータを取る場合
* -> * -> *(Map[_]など)
- 例: 1つの型パラメータを取る場合
- 高階カインド型 --
()でくくって高階を表現する- 例:
(* -> *) -> *(Functor[F[_]]など) - 例:
(* -> * -> *) -> *(Arrow[F[_, _]]など) - 例:
(* -> *) -> (* -> *) -> *(FunctionK[F[_], G[_]]など)
- 例:
このようにカインド記法を用いることで、いわば「型の型」を表現できるようになる。
