もっと型理論

「今風の型理論入門（本編）」で説明したサンプル（ByteInputStream）を雑誌記事でも使ったのですが、いかんせん4ページだからたいしたことは書けませんでした（昨日のエントリー参照）。こっち（日記）はこっちで、もう少し先まで話を進めていくことにします。

「今風の型理論入門」では、"types as specifications" または "types as theories"という立場を紹介しました。この立場では、「型＝インターフェース＋制約」と考えます。注意しておきますが、これはあくまでひとつの立場です。"types as sets"（型とは値の集合）で十分なこともあるし、"types as algebras"（型とは代数系）が適切なこともあります。

型理論で重要な概念に型階層があります。つまり、サブタイプ／スーパータイプ（この言葉はカタカナ書きします）の関係ですね。"types as sets"の立場を採用し、値の集合XとYに関してY⊆Xのときに「YはXのサブタイプ」と考えることができますが、これでは説明できないことがたくさんあります（つまり、単純すぎる）。

"types as specifications/theories"の立場では、サブタイプ／スーパータイプの定義は複雑になります。ですが、説明できる現象はずっと増えますから、かける労力は十分に報われます。そういう理由で、"types as specifications/theories"におけるサブタイプ／スーパータイプの説明を目標にしたいと思います。

内容：

インターフェースだけの型＝制約なしの仕様

「インターフェースも型とみなしてよい」と言いましたが、それは「型＝インターフェース＋制約」の制約部分がたまたま空（何もない）とみなすことでした。このことをもっとハッキリとさせておきましょう。

仕様を記述する記法として、spec Name {...}という書き方を採用します。specの一部にインターフェース定義も書くことにします。例えば：

spec AB {
 interface {
  int a();
  void b();
 }
}

specに名前（上の例ではAB）を付けているので、インターフェースは無名でもかまいません（インターフェース名を付けるのを禁止はしませんが）。

"types as specifications"を標榜しているのですから、仕様は型だし、型とは仕様です。この立場では、型と仕様は同義語です。ですから、specというキーワードをtypeに置き換えてもいいですよ。

type AB {
 interface {
  int a();
  void b();
 }
}

これで、インターフェースだけでも型になる事情はハッキリしました。

型をextrendする、そして、型はほんとにextendされているか

Javaでは（他の同類の言語でも）、インターフェースに対してextendsというキーワードを使えます。型（仕様と同義語）に対するextendsも同じ意味で使います。ただし、宣言にextendsキーワードを使わなくても、後から見てextendしていることはあります -- これっ、説明しましょう。

spec ABC {
 interface {
  int a();
  void b();
  void c(int x);
 }
}

spec ABとspec ABCを比べると、ABにcを加えてABCになっているので、ABC extends ABと言ってもいいですよね。しかし、ABCの定義の時点でABC extends ABと宣言はしてません。宣言してなくても、事実としてextendしているなら、ABC extends ABと主張する、あるいは判断してかまいません。つまり、ABC extends ABは、2つの型に関する記述、あるいは判定なのです。

これから問題にするのは、複数の型に関する判定です。これは型（仕様）定義時の宣言（自己申告のようなもの）とは異なります。宣言があってもなくても、判定はそれとは無関係です。むしろ、宣言（本人の主張）が事実と合致するかを客観的に第三者が調べることが判定です。いま出てきたextendsは判定文の動詞となるものです。

制約も考慮したextendsとは

制約も含んだ一般的な仕様（型と同義ですよ）について、extendsを考えてみましょう。

spec AB1 {
 interface {
  int a();
  void b();
 }
 /* 以下に制約 */
 [1] (true){}(-1 <= a() && a() <= 255);
}

これは、spec ABに制約式を１つ加えたものです。制約が加わることもextend（拡張；名詞ならextension）と考えます。つまり、AB1 extends ABと判定していいわけ。

もう1つ例を出します。

spec ABC1 {
 interface {
  int a();
  void b();
  void c(int x);
 }

 [1] Any(int x, int y) (a() == x){c(y); b();}(a() == x);
}

ABC1 extends ABCは分かりますね。それだけでなく、ABC1 extends ABでもあります。ABのインターフェース部分が拡張され（ABCです）、制約も加わってABC1となるので、ABC1 extends ABは正しい判定です。あるいは、次の2つから推論されると考えてもいいです。

• ABC extends AB
• ABC1 extends ABC

extendsでサブタイプ／スーパータイプを定義できるか

まとめておきましょう。一般的に、SとTが型（つまり仕様）だとします。そして、Sのインターフェース部分がI、Tのインターフェース部分がJだとしましょう。このとき、T extends Sの意味は次のことです。

• インターフェースに関して J extends I が成立している。
• Sに含まれる制約式はTにも含まれる。つまり、Tの制約式集合は、Sの制約式集合を拡張している。

T extends Sが「TがSのサブタイプ」の定義になっているのでしょうか。残念ながらそれほど単純ではありません、"types as specifications/theories"におけるサブタイプ／スーパータイプはそれなりに複雑です。しかし、T extends Sが成立しているなら、確かに「TがSのサブタイプ」だとは言えます。問題は、サブタイプ／スーパータイプ概念が、extendsだけで尽きているわけではないことです。まだ説明すべきことが残っているのです。

残っている肝心なことはまた次の機会にします。

[追記]インスティチューションとの関係に興味があれば、http://d.hatena.ne.jp/m-hiyama-memo/20060302/1141280252 にちょっとした補足があります。[/追記]