今風の型理論入門（本編） - 檜山正幸のキマイラ飼育記 (はてなBlog)

前ふりは「型→代数→…それから：型理論入門（の前半）」にあります。これは本編（後半）。1回読み切り（長いけど）で、比較的新しい*1 型理論を紹介します。「入門（門に入る）」というよりは門の外から中を覗いてみる程度。

説明用コードはJavaの構文を使います。ただし、パッケージ宣言は書かないし、publicはなるべく省略。

内容：

インターフェースなんて、所詮こんなもの
心理的効果とか、人間-人間コミュニケーションとかは、別問題
わけわからんインターフェースに制約を付加する
もっと制約を足してみる
謎のインターフェースに意図されたもの
で、それが型理論にどうつながるの？

インターフェースなんて、所詮こんなもの

まず、次のインターフェースを見てください。

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

これスゴイでしょ。何がスゴイって、これを見てもなんのことやらサッパリわからないところがスゴイ。

インターフェースってのは、本来的・原理的に「見ても何もわからない」ものです。よって、どう実装しようがまったく勝手です。例えば：

class MyABImpl implements AB {
  public int a() {
    return 0;
  }
  public void b() {
  }
}

これは当然にリッパな実装です、なんか文句ある？少なくともコンパイラは文句言いません。

大事なことだから繰り返すけど、インターフェースは実装を何も規定しないのです。もちろん、メソッド（関数）の名前、引数の型、戻り値の型、ときに例外とかの構文的な制限は課すけど、それ以上のものではありません。

心理的効果とか、人間-人間コミュニケーションとかは、別問題

今度は次のインターフェース：

import java.io.*;

interface TotalCalc {
 int calcTotal(int[] items);
 void writeResult(int result, String label, Writer out);
}

こいつは、実装者に相当のプレッシャーをかけます。普通の人は、メソッドcalcTotalにおいて、渡された整数配列の全項目を足し合わせて戻すべきだろうと想像するし、そうしないといけない気分にもなるでしょう。writeResultも同様な心理的な効果があります。

が、勇気ある人なら次の実装に躊躇はしないはずです。（※[追記]コード内に消し忘れたゴミがあったの削除[/追記]）

import java.io.*;

class MyTotalCalcImpl implements TotalCalc {
  public int calcTotal(int[] items) {
    return 0;
  }
  public void writeResult(int result, String label, Writer out) {
  }
}

もっとも、こういう勇気は蛮勇とも呼ばれ、社会的（あるいは会社的）制裁を受けることもあります。特に、インターフェースとは別に文書があったときは、「おまえは、この文書を読んでないのか」と怒られます。「俺はプログラマだぞ、コンパイラに読めないような文書は俺も読めん！」と逆ギレするのもひとつの対処ですが、それが良い方法かどうかは保証しません。

いずれにしても、インターフェースが実装内容を規定するように思えるのは、名前からの連想による心理的効果とか、インターフェースそのものとは別に文書がある、口頭で言い渡されたなんて事情であって、これらはすべて、計算現象やプログラミング言語機構とは何の関係もありません。

わけわからんインターフェースに制約を付加する

「処理系（コンパイラより広い意味）に読めないような文書は俺も読めん！」を貫き通す精神を、形式手法（formal method）と言います。前節で触れたように、これは社会的（会社的）制裁を受けるもので、それゆえ当然に、長いこと弾圧され忌避されてきたのです（半分ウソ）。

形式手法にのっとり、最初に挙げた“わけわからんインターフェースAB”（interface AB）に仕様（形式仕様）を書きましょう。この仕様は、機械可読（処理系が作れる）であり、人間にも分かるものでなくてはなりません。ここでは、次の2種類の制約式を使って仕様を書くことにします。

不変制約（不変条件）：インターフェースの実装が常に満たすべき制約。1つの論理式として書く。
ホーア制約： “事前条件、実行文、事後条件”の3つ組。もし事前条件が満たされていれば、実行後に事後条件も満たされることを要請する。事前条件、事後条件は論理式、実行文はメソッド呼び出しの列。

ホーア制約は、（オリジナルの記法とは波括弧の使い方が逆だけど）「(事前条件){実行文}(事後条件)」という形にします。

まずは不変制約を一発：

制約1 (-1 <= a() && a() <= 255)

この制約（条件）により、a()の値が-10になったり300になるような実装は即刻排除できます。（&&を使わずに、2つの制約に分けてもかまいませんし、そのほうが望ましいこともあります。）

さらに、メソッドa()に対して次のホーア制約を課します。

制約2 (a() == x) {} (a() == x)

実行文は空文なので、これは、(a() == x)の状態から何もしないなら、やっぱり(a() == x)であることを意味します。ここで出てきた変数xは、制約を書くために導入した変数で、論理学では全称束縛変数とか難しい呼び名がありますが、気にしなくていいです。通常のプログラムコードでこの制約を書くなら：

boolean constraint2() {
  int x;
  x = a();
  return (a() == x);
}

もっと制約を足してみる

前節までの制約で次のことが保証できます。

a()の値は、-1以上255以下である。
a()を続けて2回呼び出すと同じ値が返る。したがって、何度続けて呼び出しても同じ値が返る。

ここで注意すべきは、(a() == x) {b();} (a() == x)という制約はないことです。よって、b()の呼び出しによってa()の値が変化する可能性はあります。

a()の値とb()の実行のあいだの関係としては、次の制約を入れておきましょう。

制約3: (a() == -1) {b();} (a() == -1)

つまり、一度a()の値が-1になってしまうと、b()を呼び出しても-1しか返ってこなくなるのです。念のため、まとめておくと：

a()が-1以外のときは、b()呼び出し後のa()の値は事前に予測できない。
a()が-1のときは、b()呼び出し後のa()の値は-1である。

謎のインターフェースに意図されたもの

さて、制約式を書いているうちに、“わけわからんインターフェースAB”がだいぶ“わけわかって”きました。さらに、心理的にわけわかった気分にするために、aをpeekにbをnextにリネームしましょう。それで制約をもう一度列挙。制約式の形をそろえるため、不変制約もホーア制約の形で書きます。

/* 制約1 */
 (true) {} (-1 <= peek() &amp;&amp; peek() <= 255);

/* 制約2 */
Any(int x) // 「整数xの値が何であれ」という意味
 (peek() == x) {} (peek() == x);

/* 制約3 */
 (peek() == -1) {next();} (peek() == -1);

さらに気分を高める(?)ために、readという便利メソッドを書いておきましょう。

int read() {
 int x = peek();
 next();
 return x;
}

もう種明かししますが、僕の“つもり”としては、“謎のインターフェースAB”は入力可能なバイトスリームです。peek()（もとの名前はa()）が-1を返すとEnd Of Streamです。-1以外の値は、バイトの符号なし整数表現だと解釈できます。

ここで注目して欲しいのは、僕（仕様を書く人間）があなた（実装者としましょう）に“つもり”を伝えるために、クラス名／メソッド名でプレッシャーをかけたり、自然言語の文書や口頭指示を一切使ってないことです。使っているのは、論理式と実行文であり、これらはプログラミング言語の構文の一部をそのまま借用しています。

で、それが型理論にどうつながるの？

型理論には、実にいろいろな流儀・流派・スタイルがありますが、そのひとつに、「型とは、インターフェース＋制約だ」とみなすものがあります。僕は、この考え方が割と実情（現在のプログラミング言語／実行環境）にあっていると思っています。

ここで、制約とは“いくつかの制約式の集まり”で表現されます。「いくつかの」には0個も含まれるので、制約を一切持たない単なるインターフェースも型とみなせます（もちろん、そのインターフェースの実装は好き勝手になる）。「インターフェース＋制約」は仕様と呼んでもいいので、この流儀は"types as specifications"の立場と呼ばれます。また、“制約式（論理式）の集まり”のことを、論理学ではセオリーと呼ぶので、"types as theories"の立場とも呼びます。

このような型概念（types as specifications/theories）に基づき、サブタイプ／スーパータイプ、型強制／型変換などの議論ができます。このような立場からは、型とクラスはまったくの別物です。クラスから標準的に型を定義する方法は確かにありますが、それなりの段取りが必要です。通常の継承や委譲からは、正しい型階層が作れない（正しさが保証できない）こともわかります。パラメータ化された型（generics）の（ある程度は納得できる）意味論も構成できます。

いずれにしても、仕様（制約）を論理式で書き下すことが基本的・本質的です。現実にそれが出来る／出来ないは別にして、「論理式を通じて型が定義される」と想定しないと、論理学の成果がなにも適用できないので、単に曖昧・朦朧な繰り言に終始するだけで、一歩も前に進めません。精密な議論は全然できません。仕様を論理式で書かないと、文字通りハナシニナラナイのです。自分の趣味嗜好や主義主張、あるいは信仰告白（例：多重継承万歳！多重継承死ね！）を声を荒げて言いつのっても、どうせ何の結論も出ませんよ（少なくとも、ロジカルに意味のある結論が出る見込みはない）。

まーもっとも、形式化が僕の趣味嗜好に合致しているのであり、それゆえ、「可能なら形式化すべき」との主義主張に至り、「形式化が明晰性をもたらす」という信仰を抱いているわけだから、天に唾を吐いているのは僕ですけどね。

*1:GoguenとBurstallがインスティチューションを導入したのは1984ですから、実は20年以上もたってます。