Arantium Maestum

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

型システムのカインドという概念についてのメモ

Types and Programming Languagesの最後のほうに「カインド」という概念が出てくる。

System Fをさらに拡張したSystem Fωという型システムが存在していて、その「拡張の方向」がカインドだということらしい。(ちなみにSystem FωはF-ing Modules論文のベースになっているシステム)

いろいろややこしいので、自分の理解をまとめるためにメモっておく。

カインドとは

カインドとは型の型である。

という説明は簡潔かつ正確(多分)だが、これだけでは意味がわからない。

まず、一般的に(そしてTaPLでもカインドの話が出てくるまで)「型」と呼んでいるようなものは

  • unit, int, bool, string
  • (int, int), string -> bool
  • int list, string option
  • ∀X(X -> X), {∃X, {x:X, f:X->bool}}

などである。

これらのうち、例えばint list, string optionをみると、これらは'a listや'a optionといった型コンストラクタにintやstringなどの型を当てはめたものだ。

つまりlistやoptionというのは型をとり型を返す関数のようなもの、と考えられる。

('a, 'b)や'a -> 'bも型を二つとって新しい型を返す型レベルの関数と見做せる。

(余談だがML系言語の型コンストラクタ付き型の表記法がHaskellなどに比べて微妙だと言われるのは、値レベルの関数と型レベルの関数の表記の揺れが理由なのだと最近ようやくわかった)

ここで一つ考えを転換する必要が出てくる。(少なくとも私にとっては)

今まではunit, (int, int), int listなどのみを型と呼んでいたのだが、listや(,)などの型コンストラクタも型だ、あるいは今まで型と呼んできたものは0引数型コンストラクタだ、と「intとlistを同じカテゴリのもの」として認識しなおすのだ。

これは結構理解するのに時間がかかったのだが、考えてみればラムダ計算が値レベルで行った「関数も値の一種」という転換を型レベルで行っていると考えると納得できた。

つまり値レベルの世界で1, true, ()などとλx.x+1が同列で存在しているのと同じように、型レベルので世界ではint, bool, unit, int->intと同列にlist, option, (,)などが存在しているわけだ。

しかしint listは組み合わせ方として妥当だがint bool listやlist unit optionなどは非適当である、というように型レベルのものは組み合わせられるものとそうでないものがある。値レベルで関数適用できるものとできないものがあるように。

値レベルで組み合わせの妥当性を表現したものが型だ。同じように型レベルで組み合わせの妥当性を表現したものがカインドである。

カインドの形

カインドは

K := * | K => K

という形を持つ。例としては*, *=>*, *=>*=>*, (*=>*)=>*など(=>は値レベルの->と同じく右結合)

*はgroundとも呼ばれ、0引数型コンストラクタのカインドである。つまりint, unit, bool list, (string, int option)など「今まで型だと考えていたものたち」。これらはproper typeとも呼ばれ、原則的に何らかの値が属しえる型(voidはuninhabitedだが・・・)。proper typeって日本語で何ていうんだろう。型システム入門買おうかな・・・

*=>*はlistなど、単一のproper typeをとって新しいproper typeを返す型コンストラクタのカインド。

*=>*=>*は(,)など、二つのproper typeをとって新しいproper typeを返す型コンストラクタのカインド。原則的に*=>*=>*=>...*=>*とどんどん引数の数を増やすことが可能なのは値レベルの関数と同じ(ペアではないタプルを考えれば良い)

(*=>*)=>*は1引数の型コンストラクタを引数にとりproper typeを返すようなコンストラクタ。いわゆるHigher Kinded Typeで、これについては別途メモを書きたい。

カインドという概念の有用性

ここまでの説明でわかる通り、「カインド」という概念自体はジェネリクス的なデータ型があるプログラミング言語(=ほとんどの静的型付き言語)の機能との関連で説明できる。しかしそういった言語のコンテキストでは概念の説明はできても有用性は見えてこないと思う。「カインド」という次元が見えてきたところで、その次元である程度自由に動ける(≒高階)ようになってはじめて概念の便利さがわかるのではないか。こういうところは少しFlatlandを連想してしまう。

なので有用性についての話は前述の通りHigher Kinded Typesについてのメモに持ち越し。