KuwataさんがCatyのカインドの話を書いています。Catyのカインド（kind、種）は「型の型」ですが、高階の型としてはやたらに簡単な定義になっています。
Catyでは、JSONデータからなるデータ領域Dを固定して、Dの部分集合を型と考えています（Sets-as-Types解釈）。このため、型の型と言っても、ベキ集合を1回取るだけでモデルが作れます*1。これはどういうことかと言うと：
- 「値に関する概念」を、そのまま1レベル上げるだけで「型に関する概念」が得られる。
「1レベル上げる」作業は、ほとんど機械的と言えるくらいに単純です。
内容：
値と型、定数と関数
擬似言語で定数と関数を定義してみます。
/** 定数の定義 */ const two = 2; /** 右辺に算術演算を含んだ定数の定義 */ const four = 2*2; /** 関数の定義 */ function double(x) = 2*x; /** 関数呼び出しを使った定数の定義 */ const six = double(3);
const, function の前に type を付けると型に関する概念を意味するとします。つまり、type const は型定数、type function は型関数です。型定数とか型関数とか知らないって？ 見ればわかりますって。
/** 型定数の定義 */ type const Text = string; /** 右辺に型構成演算を含んだ型定数の定義 */ type const StrPair = [string, string]; /** 型関数の定義 */ type function Pair<X> = [X, X]; /** 型関数呼び出しを使った型定数の定義 */ type const IntPair = Pair<integer>;
見ればわかりますよね。[..., ...] という記法だけ説明しておきます； JSONでは、配列を [2, 3] のように書きます。ブラケット（大括弧）が配列の構成子（コンストラクタ）となっています。値の構成子記号であるブラケットをそのまま型の構成子にも流用して、文字列からなる長さ2の配列型は [string, string] のように書きます*2。
値に関する用語の前に形容詞「型」を機械的に付けると型に関する概念になります。しかし、現実には別系統の用語法が使われているのでそれをまとめておきます*3。
| 値に関する用語 | 型に関する用語 |
|---|---|
| 定数 | 型（型名） |
| 関数 | 総称型 |
| 仮引数 | 型パラメータ |
| 実引数 | 具体型、基礎型 |
| 関数への実引数渡し | 総称型の具体化 |
値の集合、型の集合
カインドは型の集合ですが、値の集合から説明をします。集合の記述や構成には色々な方法がありますが、ここでは関数を使って集合を定義する方法を紹介します。
f:A→B が関数（写像）だとします。Bの部分集合を、{f(x) | x∈A} という形で定義することはよくあります。例えば、偶数の全体からなる集合は、{double(x) | x∈integer} と定義されます。これを擬似言語で書いてみると次のよう。
/** 関数の定義 */ function double(x) = 2*x; /** 関数を使った集合の定義 */ set evenNumber = forall(x) double(x);
forall(x) double(x) で、変数xは暗黙に整数変数と仮定してますが、xの変域を明示的に書くなら forall(x in integer) double(x) です。foreach文とかリスト内包表記と似ているので分かると思います。
同じ方法で型の集合を定義してみます。
/** 型関数の定義 */ type function Pair<X> = [X, X]; /** 型関数を使った型集合の定義 */ type set PairType = forall<X> Pair<X>;
型関数（type function）を“総称型”と特別な呼び方をしたのと同じように、型集合（type set）を“カインド”と呼んでいるのです。
関数と集合の使い方をもう少し
値の集合を表現する forall(x in integer) double(x) は、すべての偶数からなる集合を意味します。負の偶数からなる集合を表現するにはどうしたらいいでしょうか？ 次はその方法を示しています。
/** 関数の定義 */ function double(x) = 2*x; /** 集合の定義 */ set negative = less(0); /** 関数を使った集合の定義 */ set negativeEvenNumber = forall(x in negtive) double(x);
ここで出てきた less は、整数の引数を渡されて集合を作り出す関数で、less(a) = {x | x ＜ a} と定義されます（変数xは暗黙に整数変数と仮定）。
同じような発想で、スカラー成分のペア型（長さ2の配列型）を定義してみます。
/** 型関数の定義 */ type function Pair<X> = [X, X]; /** 型集合の定義 */ type set ScalarType = lower<scalar>; /** 型関数を使った型集合の定義 */ type set ScalarPairType = forall<X in ScalarType> Pair<X>;
ここで、scalarは型定数で、具体的な型（値の集合）を意味します。lower<A> は、型（値の集合）Aの部分集合全体からなる型集合（つまりカインド）を意味します*4。型であるscalarとカインドであるScalarTypeを混同しないでください。この違いは、整数値である0と整数の集合negativeの違いに相当します*5。
構文が悩みの種
以上に説明したように、Catyのカインドは、「値に関する概念をレベルアップすればそれでOK」という原理が成立しているので、意味論は簡単です。しかし、カインドの記述や構成を行う書き方（構文）には悩んでしまいます。
- どんな演算記号やキーワードを使うべきか。
- 例えば、X in ScalarType と X of ScalarType のどっちがいいだろう*6。
- lower<scalar> の山形括弧を毎回付けるのは面倒ではないか。
- そもそもlowerってキーワードがいいのか。subとかinferiorはどうかな？
- forallの構文は書くのに長すぎてイヤだ。もっと短い略記はないか。
- あまり略記をすると、意味が分かりにくくなるのではないか。
- 書くのは1回、読むのは多数回だから、記述的な長い名前や記法がいいのか。
- 既に決めてしまった型定義の構文との整合性をとらないと。
困ったことには、構文の選択には趣味嗜好が影響し、あまり合理的な判断基準がありません。キーボードを打ったときの感触とか、図形としての見た目とか、（可読性というよりは）視認性*7とか、とっても感覚的な基準ばっかり。
*1:型がDのベキ集合Pow(D)の要素なので、型の型はPow(Pow(D))に入っています。
*2:これは、後で出てくるforallを使っていて、foall(x in string, y in string) [x, y] の略記が [string, string] です。
*3:歴史的な経緯からしょうがないことですが、型定数、型関数、型集合のような用語だったらスッキリと分かりやすかったんですけどねぇ。
*4:型A自身もカインドlower<A>に入ります。
*5:不等号にイコールが入るかどうか、とかの違いはドーデモイイとします。
*6:最初'of'としたのですが、最近「'in'のほうが自然そう」と思ってます。
