kindとtype

備忘録というか勉強メモを書いておく事にした。

檜山さんが「Catyの型システムにkind入れたい」と言い出し、ってかそもそもkindってなんじゃと言うのが今回の話。

kindについて大雑把に 

現在のCatyはsets as types(実際はsetoidだったはず)の立場である。sets as typesの場合の型というのはインスタンスの集合であり、あるデータ領域Dのとある型はPow(D)の要素である。例えばJSONにおけるDとPow(D)は以下のようになる。

D = {..., -2, -1, 0, 1, 2...,
     ..., -0.2, -0.1, 0.0, 0.1, 0.2...,
     "", "a", "ab", "abc"...,
    {}, {"a": 1}...,
    []、[1], [1, 2]...,
    true, false,
    null}

Pow(D) = { {0}, {0, 1}, {0, 1, 2}...
           {""} {"", "a"}, {"", "a", "ab"}...
}

この場合、integer型はPow(D)の要素のうちすべての整数を含む要素であり、string型はすべての文字列を含む要素、などとなる。もちろんすべての整数+nullみたいなものを考えることもでき、恐らくそちらの方が多くのプログラミング言語の実装からするとわかりやすいのかもしれない(俺はinteger型の変数に何もせずともnullが代入できるのは大変なクソだと思っているのだが)。

そしてkindの話なのだが、これはtypeがインスタンスの集合なのに対してkindはtypeの集合となり、要するに型の型。あるデータ領域DにおけるkindとはPow(Pow(D))の要素である。いちいち要素を列挙するのが非常にかったるいので適当に端折るが、

D = {..., -2, -1, 0, 1, 2...,
     ..., -0.2, -0.1, 0.0, 0.1, 0.2...,
     "", "a", "ab", "abc"...,
    {}, {"a": 1}...,
    []、[1], [1, 2]...,
    true, false,
    null}

Pow(D) = {integer, string, number, boolean, object, array, null...}

Pow(Pow(D)) = { {}, {integer}, {integer, string}, {integer, string, object}... }

となる。

Catyにおけるkind 

ところでCatyスキーマではリストは以下のように定義できる。

type list<X> = [X*];

このlistは型パラメータXを受け取り、Xのみを含む0以上の長さの配列という型を返すのであるが、もしもkindのような概念がない場合、このlistのような型パラメータを受け取るものをtyping(正確にはkinding?)できず、「Xとしてinteger、stringといったスカラー型のみを受け取るlist」のようなものが書けないわけだ。

もしもkindがあるなら、このように定義できる。

kind scalar = integer | string | boolean | number | null;
type scalar-list<X of scalar> = [X];

これは以下のような定義とはまったく異なる。

type scalar-list2 = [(integer | string | boolean | number | null)*];

scalar-listが型パラメータは渡された時点でそのパラメータのみを包含するリストになるのに対して、scalar-list2は常にすべてのスカラー型を包含しうるリストになる。

集合=述語=バリデータ=型 

Catyにおいては型というのはあるインスタンスに対するバリデータ(booleanを返す述語)として働き、あるコマンドf:A->Bが入力iに対して実行可能であるということは、ある型Aへのバリデータをaと置けば、a(i)が真かつb(f(i))が真であるということになる。この時aとAは以下のように1対1に対応する。

A = {x | a(x) = true}
a(x) = if x∈A then true else false

さてkindによって型の型が扱えるようになったわけだが、この手の話はレベル、あるいは階層が一個上がった話だ。kindを持たないCatyの世界では、存在するのはコマンド(関数だと思って)と型だけで、型の中には型パラメータを取る総称型ものもあったが、そのパラメータは特に型付けされていなかった。

だがkindを導入した場合は型パラメータも型付けできるようになったので、型そのものを扱う関数について考えられるようになった。じゃあCatyの世界で型その物を扱う関数とはなんだというと、これは総称型になる。つまり、kindについて考えない世界とkindを導入して階層を一つ上がった世界との間には、次のような関係がある。

without kind with kind
インスタンス
kind
コマンド(関数) 総称型
入力 型パラメータ

総称型の型パラメータを型付けするものは、kindであり、kindもまた集合であり、つまり同じように述語、バリデータとして働くようにすればいいわけだ。これにより、ある総称型T<P1 of K1, P2 of K2...>が実際の型X, Y...で実体化可能であるという事は、同様にk1(X)が真かつk2(Y)が真かつ……という事になる。

というわけで俺はそのうちこれを実装するわけだが、上記のような単純な例ならともかく、実際にはある型が別の型に包含されうるかの判定など、要するに今まで手の回ってなかった部分に手を入れなければならず、非常にマゾい開発が予想される。いやまあ、まずは構文上の対応だけでもいいと言われてはいるのだが。

更新履歴 

2011-04-14
公開