考えなおそう

カインドを肥大させないように禁欲的に考えてたが、どうもこれがよくないかも。ブール半環の構造を持たせてもいいかもしれない。

カインドKに対して、最大値 max(K) の存在を要請するのは無理がある。極大元の集合をtops(K)として、tops(K)が有限集合ならいいことにしよう。これは、カインドをブール半環にすることと矛盾しない。

静的型解析と実行時チェックはかなり違う。カインドKの情報で、実行時に使えるのは型 sup(K) だけ。max(K)が存在しなくてもsup(K)は常に存在するし、tops(K)が有限だから計算可能だ。max(K)の存在にこだわるのが間違いだったようだ。

実行時に何が必要か？ と冷静に考える必要があるな。型情報のほとんどは実行時には意味が無い、高階の情報があっても使いがようがない。実行時には、型概念のレベルにおいて、レベル0の判断しかできないので、レベル1（型）、レベル2（カインド）の情報が役に立たない。

それと、「総称は具体化しなくてはならない」という原則（ドグマ）も疑ったほうがいいかも。具体化は手段だから、もし具体化せずにうまくいくなら無理に具体化する必要はない。絶対に具体化が必要なところがあるかどうか？ 具体化しても、実行時情報としては無意味だとしたら？

もうひとつのドグマは、「いわゆる型推論」で、推論していいことあるのか？ と考える必要がある。推論することが目的ではない。実行時の安全性を保証することが目的で、確定した型宣言を求めることが目的ではない。「実行時安全性を保証する」ことと「静的に型宣言を確定する」ことがほんとに因果関係を持つのか？ 持つと信じてきたが、具体的な因果の糸をたどってない。

インスタンスとカインドのあいだには1レベル分のギャップがある。我々の型制約（type constraints）は等式的ではない。ギャプがなく等式的な状況における議論をそのまま適用するのは的外れの可能性がある。