ソートと指標と型、実例をまじえて

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

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

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

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

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

「ソートとは、型みたいなもんです」と思わず言ってしまう背景には、原初的・素朴な型概念があります。それは、"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の後に等式が書いてあります。等式による制約の意味は:

  1. スタックStkにXをプッシュした直後のトップはXである。
  2. スタックStkにXをプッシュした直後にポップすると、もとに戻る。

これで、スタックの振る舞いまで制限できますね。

CafeOBJのようにセオリーを書けて、さらに普通のプログラミングもできる言語があればいいのに、と思うのですけど、いまのところ見かけませんね。めだたないだけで、どこかに存在してるのかな?

*1:このあたりの用語法はバラバラで統一はされてません。演算子と関数と写像は人/場合により区別したり同義語だったり、記号と実体の区別をしたりしなかったり。

*2[追記]最初、ビックリマーク付きのmodule!を使ってましたが、あえてビックリを付けることもなさそうなのでビックリは取りました。[/追記]

*3:ここに出現するStringは実際の文字列データ型を表現するわけではなくて、単なる記号です。

コメント
0件
トラックバック
3件
ブックマーク
0 users
m-hiyama
m-hiyama