ソートと指標と型、実例をまじえて - 檜山正幸のキマイラ飼育記 (はてなBlog)

このダイアリーでは、型（タイプ）の話題をけっこう取り上げています。例えば：

僕のスタンスは"Types as Theories"、つまり型とはセオリー（形式的理論）だとみなす立場です。で、その"Types as Theories"を説明するとき、指標（signature）って概念が必要なんです。指標にはソート（sort）って概念が含まれます。そのソートの説明をするとき僕は「まー、型みたいなもんだと思ってください」なんて言ってしまいます。ちょっと待て、

型を定義するには、セオリーの概念が必要
セオリーを定義するには、指標の概念が必要
指標を定義するには、ソートの概念が必要
ソートとは、型みたいなもんです。

って、循環しているじゃねーか！これじゃダメだ。補足と言い訳が必要ですね。

ソートは値の集合を表すつもりの記号

「ソートとは、型みたいなもんです」と思わず言ってしまう背景には、原初的・素朴な型概念があります。それは、"Types as Sets"という立場で、型とはデータ／値の集合だと把握する態度です。"Types as Sets"でもある程度のことは説明できますし、このような理解が型概念のスタートラインとなります。

ですから、「ソートとは、型みたいなもんです」のココロは、「ソートとは"Types as Sets"の意味での型、つまり、データ／値の集合みたいなもんです」ってことになります。それでもまだ「みたいなもん」がついているのは、ソートが実際の集合を表すとは限らないからです。ソートは単なる記号（あるいは名前）です。最初から特定の集合に結びついてはいません。ソートが記号であることを強調したいときはソート記号と呼ぶこともあります。

それでは、ソートがいつでも単なる記号かというと、そこは微妙で、具体的な集合を表すこともあります。そもそも記号というものはそういうもので、実体と結びついてない状態もあるし、実体と同一視できる状況もあります。

指標の具体例：MLとJava

ソートが集合を表すつもりの記号なら、演算子（operator）は関数／写像を表すつもりの記号です*1。ソートと演算子を必要なだけ寄せ集めたもの一式が指標です。「指標（シグニチャ）」という言葉は、全然別な意味で使われることもありますが、型理論や仕様技術では、今説明した意味で使われることが多いようです。

幸いにも、ML系プログラミング言語では指標（signature）という用語をそのまま使っています。文字列を出し入れするスタックの指標は次のように書けます。

signature STACK = sig
  type stack
  val newStack : unit -> stack
  val top : stack -> string
  val pop : stack -> stack
  val push : stack -> string -> stack
end

typeって書いてあるところがソートの宣言です。あらら、ソートを表すキーワードがtypeになっているわ。まー、「ソートとは、型みたいなもんです」からね :-) valではじまる行は演算子の宣言です。

指標の代わりにインターフェースという言葉を使う言語／文化もあります。スタックの例をJavaのインターフェースで書くなら：

interface Stack {
  String top();
  void pop();
  void push(String data);
}

インターフェースの名前Stackがソート（記号）を兼ねています。演算子（Javaではメソッド名）の引数／戻り値がMLの場合と異なるのは、暗黙の第1引数thisと副作用による暗黙の戻り値（状態遷移後の状態）が省略されているからです。それと、Javaのインターフェースではコンストラクを記述できないので書いてありません。

セオリーが書ける言語はないのかな

さて、セオリーとは指標にさらに制約条件が付いたものです。制約条件（公理系と呼ばれることもある）は論理式で書きます。EiffelやD言語では、メイヤー先生の契約駆動プログラミングをサポートする表明機構を備えています。でもこれは、セオリーと呼ぶにはもの足りない。

プログラミング言語ではありませんが、実行可能仕様記述言語であるCafeOBJならセオリーを書き下せませす*2（まー、そういう目的の言語だから当然だけど）。

module STACK {
 [Stack String]

 op newStack : -> Stack
 op top : Stack -> String
 op pop : Stack -> Stack
 op push : Stack String -> Stack

 var Stk : Stack
 var X : String
 eq top(push(Stk, X)) = X . -- 条件1 --
 eq pop(push(Stk, X)) = Stk . -- 条件2 --
}

最初にあるブラケットで囲まれた記号（StackとString*3）がソートです。opは演算子の宣言、varは制約条件（等式）を書くときに使う変数の宣言、そしてeqの後に等式が書いてあります。等式による制約の意味は：