XMLフレンドリーな型システム
-- 「折れ線の例」から導かれること --

檜山正幸 (HIYAMA Masayuki)
Tue Mar 15 2005:start
Tue Mar 15 2005:draft

「折れ線の例」から導かれることの1つに、型システムとXMLの関係がある。 この記事では、指示対象とそのXML表現がうまく対応するような型システム、 つまり“XMLと相性がいい”型システムについて考えてみる。

目次

1. はじめに

「折れ線の例」という記事に、「この例(折れ 線の例)には重要な意味があると思える」と書いた。実際、「折れ線の例」に は、多くの問題が含まれている。そして、それぞれの問題はけっこう根が深い。 「折れ線の例」の第7節では、「折れ線の例」 に関係した問題を3つ挙げておいた(この3問で、関連するすべてをカバーして いるわけではない!)。その最初の問題は次のものである:

この記事では、上に引用した問題に(ある程度の)答を与えようと思う。

「運がよければ」という言い方は誇張ではなくて、都合がいい条件が色々と 揃っている状況下ではじめて、構文側(字句構文またはXML構文)と指示対象 側がうまく対応する。そこでこの記事で、「都合がいい条件」を明確に述べて、 その条件のもとでの「うまい対応」のメカニズムを探る。

運がよいケースについて分析しておけば、一般の(あまりラッキーではない) ケースと比較することができる。それに僕は、一般性を持たない特殊ケースで あっても、その小さな世界がきれいにまとまっていたり、美しい構造を持てば、 価値があると思っている。まー、趣味的に好きなだけとも言えるけど、「一般 性を持たない特殊」が、意外にも適用範囲が広いことだってあるしね。

2. 型システム

「型(かた)とは何か」という問題は、コンピューティング・サイエンス (*注1)の主要な課題のひとつだろう。さまざまな型概念が提案されているが、 ここでは、"types as sets"の解釈を採用しよう。つまり、型とは、その型に 属する値の集合だと考える。現在では、"types as sets"解釈はあまりに素朴 すぎて、その有効性は限定的であることが知られている(*注2)が、いまの我々 の目的にはこれでも十分である。

注1

僕が、「コンピュータ・サイエンス(計算機科学)」ではなくて、「コンピュー ティング・サイエンス(計算科学)」という言葉を使う理由は、 記事 「ソフトウェア工学について思うこと」(他サイト)の第2節に書いてある。

注2

他の型概念として、"types as algebras"、"types as coalgebras"、"types as propositions"、"types as theories"などがある。

「型とは値の集合」とした上で、いくつかの型をまとめた構造を‘型システ ム’と呼ぶことにする。型システムは、次のような構成素から成り立つとしよ う。

  1. 型の名前:型を識別するために、型の数と同じ個数の名前が必要である。 型の名前は‘ソート’とも呼ぶ。
  2. 型の領域:型の実質である値の集合を、‘型の領域’と呼ぶ。
  3. 型階層:2つの型のあいだに、サブタイプ/スーパータイプの関係がある ことがある。この関係は、全体として階層構造を定義する。この階層構造 を‘型階層’と呼ぶ。

通常、“型の名前”と“型の領域”をいちいち区別しないが、この記事では 区別することがある。例えば、intが単に名前であることを強調する ときは、'int'のように引用符で囲む。また、intの領域は[int]のようにブラ ケットで囲んで明示する。または、intの領域をD(int)とも書く(Dはdomainか ら)。だが、いつでもこれを守るのはシンドイので、文脈でわかるときは厳密 な区別はしない。

さて我々が事例として扱う型は次のものである。

  1. decimal : (整数部もある)有限小数で表現される実数
  2. integer : 整数
  3. point : x座標もy座標もdecimalである平面上の点
  4. latticePoint : x座標もy座標もintegerである平面上の点
  5. polyline : 平面内の折れ線。折れ線の頂点はpointである。

他の型も例として使うが、それは必要になったときに導入することにする。

上の箇条書きによる簡単な説明でも、型の名前と型の領域については了解し てもらえるだろう。型階層を記述するには図示するのが一番だが、毎回図を描 くのも面倒なので、is-subtype-of というキーワードを使って関係を表現する ことにしよう。is-subtype-ofを使った型階層の記述は次のとおり。

3. 型階層

decimal, integer, point, latticePoint, polylineという5つの型を導入し たが、これらにはそれぞれ領域が存在する。型の領域は、[decimal], [integer], [point], [latticePoint], [polyline]と書く約束だった。では、 あらためて問うが、領域とは何だろうか。

我々は、領域を、対象の表現の集合ではなくて、値の集合と考える。例えば、 [integer]のメンバーは、「'+'と'-'、および数字(digit)からなる文字列」 とは考えない。整数表現に使う文字列ではなくて、整数の“値”の集合が [integer]だとする。同様に、[point]、[latticePoint]、[polyline]は幾何学 的な対象からなる集合である。

"types as sets"解釈では、型の階層の定義はきわめて単純である。型の領域 のあいだに包含関係があれば、それを型階層だと考える(*注3)。だから、 「integer is-subtype-of decimal」の根拠は、[integer]⊆[decimal]が成立 することであり、「latticePoint is-subtype-of point」の根拠は、 [latticePoint]⊆[point]である。

注3

型s, tに対して、s is-subtype-of tならば、必ずD(s)⊆D(t)でなければなら ない。だが、逆は要求してない。つまり、D(s)⊆D(t)でも、s is-subtype-of t とはならないケースも認める。

型の領域として、表現の集合を採用しなかったのは、表現についてはサブタ イプと包含関係がうまく対応しないケースが多いからである。例えば、 真偽値を表す型booleanにおいて、真を'1'で、偽を'0で表現したとしよう。 表現のレベルでは、boolean ⊆ integerが成立する。が、通常はbooleanを integerのサブタイプとは考えない(*注4)。また、日付は通常文字列で表現さ れるが、だからといて、dateはstringのサブタイプとも考えない(*注5)

注4

booleanをintegerのサブタイプと考えるケースもあるが、それはbooleanが独 立したデータ型ではなかった名残だろう。booleanはintegerとは独立だと考え た方が自然だ。

注5

XMLの属性値として書くデータは、すべて文字列(字句的)表現を持つ。表現 レベルでの関係を根拠にすると、あらゆる型がstringのサブタイプになってしまう。

4. 表現を持つ型システム

型の領域とは、表現の集合ではないと言った。領域は、数値や幾何学的 対象の集合である。とはいっても、数値も幾何学的対象も表現がなくては、 それらを記述することも議論することもできない(*注6)

注6

そもそも、表現なしの“純粋な”値や点が存在するかどうかはあやしい。僕 は、「表現が先か、概念が先か」と問われれば、迷わず「表現が先」と答える。 では、「表現が指している対象は実在するか」と問われれば、それは「わから ない」。

Chimairaの文脈では、表現しかない(値概念がない)型システムが必要だと 考えている。というのも、Chimairaの(理念的な)出発点は「XMLデータあり き」なので、事前に指示対象を持ち出すことができない(または困難である) からだ。表現しかない型システムについては、第7章で触れておい た。

integerやlatticePointの表現としては、次のような字句的な表現もあるだろ う(字句的構文定義にBNFを使っている)。

/* 
 * Digit(数字)、NonzeroDigit(非零数字)、S(省略可能な空白)
 * の定義は省略する。
 */

PositiveInteger ::= '+'? NonzeroDigit Digit*
NegativeInteger ::= '-' NonzeroDigit Digit*
Zero ::= '0'
Integer ::= PositiveInteger | Zero | NegativeInteger

LatticePoint ::= '(' Integer S ',' S Integer ')'

記事「折れ線の例」では、point、latticePoint、 polylineをXML形式で表現している。例えば、latticePointの表現は次のよう な形にしたのだった。ここに出現するintegerは字句的表現だから、先にBNFで 定義した字句構文だと思ってよい。

LatticePoint ::= <point x=integer y=integer />

さて、先ほど、型システムは「型の名前、型の領域、型階層」からなると言っ たが、さらに、型ごとにその値(インスタンス)の表現法が決まっているよう な型システムを考えよう。そして、型tのインスタンス表現の全体をR(t)とす る(Rはrepresentationから)。例えば、R(integer)は上のBNFで定義した字句 表現で、R(latticePoint)はXML表現、という具合に決まっているケースを考える。 このように、表現まで規定された型システムを‘表現を持つ型システム’と呼 ぶことにしよう。

表現を持つ型システムとは、あらゆる値/対象がシリアライザブルな型シス テムと言ってもよい。シリアライズ(あるいはエンコーディング)構文は字句 構文のときもあるし、XML構文のときもある。我々の文脈では、人間可読なテ キストにシリアライズできるケースに限定してよいだろう(*注7)

注7

データベースにダイレクトに格納するようなケースもあるだろうが、そうい うのは、あんまり考えたくない。

5. 忠実な表現

s is-subtype-of t のとき、D(s)⊆D(t)であるのは、型階層の決まり(お 約束)である。しかし、s is-subtype-of t から、R(s)⊆R(t)が導かれる とは限らない。例えば仮に、decimal(十進数)の表現(字句表現)に必ず小 数点を入れるという規則があったとしよう。すると、 整数値も'1.0'、'0.0'のように書く必要がある。一方、intの表現には小数点 は入らない。よって、R(int)⊆R(decimal)は成立しない(あくまで架空の話だ けど)。

そこで、s is-subtype-of t なら必ずR(s)⊆R(t)となっているような表現を 特に、‘忠実表現’と呼ぶことにしよう(*注8)。忠実表現を備えた型システ ムは、‘忠実表現を持つ型システム’と呼ぶ。(詳しくは次節で整理する。)

注8

表現論(群の線型表現とか)で、忠実表現という言葉が登場する。が、文脈 が随分と違うから、同じ用語を使っても大丈夫でしょう。

忠実表現を持つ型システムでは、型階層が、表現(字句やXML)の世界の包含 関係として実現されている。さまざまな複合型やオブジェクト型を含む型シス テムに対して、忠実表現を構成するのはやさしいことではない。そもそも、デー タを再現可能な形にシリアライズ(エンコード)するのさえ楽ではない(*注9)

注9

複合型やオブジェクト型を含んでいても、そのなかでタチが良いサブシステ ムを選べば、忠実表現を持つ型システムを作れるのではないか、と僕は期待し ている。実際にやってみたわけではないので、それがどんな型システムか、詳 しくはわからない。だが、忠実なXMLシリアライズを持つ型システム(の型) に属するオブジェクトを"xmlizable object"と呼ぼうと予定している。ところ が、"xmlizable"をどう発音するか見当が付かないので、XOと略称するしかな いかとも思っている。XOってのはとても高いお酒の名前だから、高級そうでい いでしょ。 -- って、まだ正体不明のものを「高級そう」とか言ってみてもしょ うがないのだけどね。

6. 忠実表現を持つ型システムを整理する

ここらで、少し整理しておこう。"types as sets"解釈における型システムは、 「型の名前、型の領域、型階層」から成り立つ。型の名前(ソート)の集合を Sとしよう。Sのメンバーは単なる記号である。我々の事例では、 S = {'decimal', 'integer', 'point', 'latticePoint', 'polyline'}である。 ここで、名前を引用符で囲んだのは、単なる記号であることを強調したいから である。

型階層の概念を、Sのなかで定義しよう。つまり、単なる記号 のあいだの関係として型階層を定義したい。is-subtype-of は長たらしいので、 不等号「<」をis-subtype-ofの代わりに使おう(*注10)。記号「≦」は、「サ ブタイプであるか、または等しい」という意味である。

注10

別な記事「Janusのなかの計算系」の第6節で は、s is-subtype-of t を、この記事とは逆に s>t と書いている。 注釈で、不等号の向きなんてのはどっちにで もコジツケられる、と言い訳はしているけど。

集合{'decimal', 'integer', 'point', 'latticePoint', 'polyline'}のなか に、「'integer'<'decimal'」、「'latticePoint'<'point'」の関係がある。 順序関係≦を完全に示せば、次の表にようになる。表の各欄には、「行見出し (左)≦列見出し(上)」が成立しているかどうかが書き込んである。

TABLE: ソート(型の名前)集合上で定義された順序
'decimal' 'integer' 'point' 'latticePoint' 'polyline'
'decimal' Yes No No No No
'integer'Yes Yes No No No
'point' No No Yes No No
'latticePoint'No No Yes Yes No
'polyline' No No No No Yes

Dは、Sのメンバー(ソート)に領域と呼ばれる集合を対応させる(一種の) 写像である。ただし、s≦tならばD(s)⊆D(t)でなくてはならない。我々の事例 におけるDは既に定義済みである。つまり、D('decimal'), D('integer'), D('point'), D('latticePoint'), D('polyline')について説明をしたので、そ の説明をもって(厳密性には欠けるが)定義としよう。

以上、“ソート(型の名前)集合S”、“S上に定義された順序≦”、“Sのメ ンバーに集合を対応させる写像D”からなる3つ組(S, ≦, D)によって、型シ ステムが定義されるといってよいだろう。

NOTE: 型階層はどこに定義すべきか

集合Sは、単なる記号の集合である。型階層は、この記号の集合S上の 順序構造として実現されている。この定式化に違和感を感じるかたもいるだろ う。 Sは、“ホンモノの型の集合”ではなくて、記号の集合である。本来、順序 (階層)が定義されるべき場所は、型自体の集合ではないか? と。

だが、型自体の集合とは何だろうか。型の名前は型自体ではない。型の領域 も型自体ではない。では、型はどこのあるのだろう。型自体は観念だといって しまうと、それ以上定式化はできなくなる。実際に取り扱い可能なナニカを型 (型の代理と考えてもいいけど)だと定めないと先に進めない。だから、型の 名前である単なる記号をとりあえず型だと認めて、そこに順序を導入したので ある。

型システムが表現を持つ場合は、Sのメンバーに表現と呼ばれる集合を対応さ せる写像Rを付け加えて、(S, ≦, D, R)が型システムとなる。DとRが無関係 では困るので、 t∈Sごとに、表現に値を対応させる valt:R(t)→D(t) という写像が必要で ある。だから、(S, ≦, D, R, {valt | t∈S})とでも書いたほうがいいか もしれない(が、面倒だから、この記法は使わないけど)。

さて、表現を持つ型システム(S, ≦, D, R)が忠実な表現を持つとは、 次が成立することである。

さらに、x∈R(s)の値を、valsとvaltで求めて食い違いがあると具合が悪 いので、次の条件も必要である。

例えば、integerのサブタイプとしてnaturalNumberを設けたとき、 naturalNumberに対する表現'10'が整数16を意味するようなこと (valnaturalNumber('10') = valinteger('16'))があってはならな い。別な言い方をすると、s≦tのとき、R(t)上で定義されたvalt:R(t)→ D(t)を、R(s)の上に制限した写像がvalsになっている必要がある。

NOTE: 圏論的な整理

順序集合(S, ≦)は、Sを対象類(class of objects)とする圏とみなせる。 圏としてのSも同じ記号Sで表せば、

表現Rが忠実なら、RとDは、圏Sから集合圏への関手となる。R、Dどちらの関手 でも、Sの射には集合のあいだの包含写像が対応する。そして、valt:R(t) →D(t) は自然変換となる。

つまり、忠実な表現を持つ型システムは、 2つの関手R、Dと自然変換val:R⇒Dから成り立つ構造である。valが自然変換で ある条件が、vals(x) = valt(x) である。

7. 構文的型システム

この節は、ちょっと脇道にそれるので、スキップして次に節に進んでもよい。

値とか指示対象(denotation)の概念がなく、表現だけから組み立てられる 型システムを‘構文的型システム’と呼ぶ。構文的型システムは、値/指示対 象を持つ型システムと極端に変わるわけではない。上に述べた忠実表現を持つ 型システムからDを取り除いたものだと思えばよい。

(S, ≦)がソート(型の名前)集合とその上の順序だとする。s∈Sに対して、 表現と呼ばれる集合R(s)が対応している。ただし、D(s)やvalsは存在しない。 代わりに、sごとにNs:R(s)→R(s)という写像が付属している。このNsは、 正規化である。

正規化とは、たとえば、"+3.0"を"3"に直すような、標準的な表現に直す写像 である。標準的な表現を‘正規形’と呼ぶ。つまり、Nsは、ソートsに対す る‘正規化写像’である。正規形をもう一度正規化しても何も変わらないから、 Ns(Ns(x)) = x が成立している。逆に、NN = N となる写像Nなら、その内 容に関わらず正規化として採用してよい。

実は、R(s)の正規形の全体が値の集合D(s)の代わりをつとめる。正規形の全 体をD(s)とすれば、事実上、値/指示対象を持つ型システムと同じ取り扱いが できる。

つまり、こういうことになる: 値や指示対象という概念は、観念的/プラト ニックであり、実在するかどうかあやしい。一方で、表現 (字句表現、XML表現、その他なんでも)を構文的に定義することは、かなり 具体的である(*注11)。また、正規化を実行可能なアルゴリズムとして与えれ ば、これも具体的といっていいだろう。よって、構文的に定義された表現と正 規化手続きだけに基づく型システムは、(構文を信用する人間には)より確実 で“手でさわれるシステム”といえる。しかも、その型システムは、正規形を値 と考えることにより、値概念を(後から)導入することもできる。

注11

「ほんとに具体的か」と問われると、僕は確信を持ってYesとは答えられない のだけどね。

僕は、観念的/プラトニックな値/指示対象を嫌ってはいない。が、いつで も値/指示対象を要求されるととても困るのである(*注12)。一方、表現と正規 化手続きを与えることならできるケースは多い。この理由からChimairaでは、 構文的型システムをより基本的なものと位置付けたい。だがこれは、値/指示 対象をまったく認めないような極端な立場ではない。天上の世界(イデア界) に棲むと思われる“純粋な整数”とかもおおいに利用するつもりだ。

注12

例えば、日記エントリーや週報に対して、その値/指示対象は何だ?と詰め 寄られると困る。あるいは、文書中の見出しや段落の値/指示対象は何だ?と 聞かれても答えようがない。構文と正規化しかなければ、こういう意味強迫症 から逃れられる。

8. 折れ線の例で考える

ここで、我々の原点、つまり「折れ線の例」に戻って考えよう。既に述 べたように、型の名前/記号であるソートの集合として、 とりあえず{'decimal', ' integer', 'point', 'latticePoint', 'polyline'} があり、'integer'<'decimal'、'latticePoint'<'point'から誘導される (induced)順序構造がソート集合上にある。

ソートの順序構想が、すなわち型階層になる。この点に違和感があれば、ノー ト「型階層はどこに定義すべきか」を参照のこと。長年培った 常識から、次のことは納得できるだろう。

次はどうだろうか。

整数、有限小数の字句表現を普通に定義すれば、R('integer')⊆R('decimal) は成立する。格子点と点を、以下のパターンのXML要素で表現すれば、 R('latticePoint')⊆R('point')も大丈夫だ。

LatticePoint ::= <point x=integer y=integer />
Point ::= <point x=decimal y=decimal />

表現に値を対応させる写像は次の5つがある。厳密詳細に定義するのは面倒だ が、その存在をイメージすることは容易だろう。

  1. valdecimal : R('decimal') → D('decimal')
  2. valinteger : R('integer') → D('integer')
  3. valpoint : R('point') → D('point')
  4. vallatticePoint : R('latticePoint') → D('latticePoint')
  5. valpolyline : R('polyline') → D('polyline')

表現は字句(文字列)またはXMLインスタンスである。値/対象の領域には数 値や幾何学的対象が含まれる。valはそれらのあいだの対応を与える。また、 valintegerとvaldecimalは互換性を持つ(同じ規則である)し、 vallatticePointもvalpointと互換性を持つ。

折れ線の例では、R('point')など表現の集合を、最初を大文字にしたPointな どで示していた。そして、表現と値/対象をあまり区別しない形で説明をして いた。が、今までの分析で、折れ線の例には、“忠実表現を持つ型システム” が登場していたことが分かるだろう。

9. 折れ線の例でもっと考える

ところで、折れ線の例では、Polyline3、LatticePolylineなど (これらは表現の集合)も登場し、次のような階層があることも言及されて いる。

       Point
        |
    LatticePoint

       Polyline
        / \
      /     \
Polyline3  LatticePolyline
     \       /
       \   /
   LatticePolyline3

この階層は、表現の集合における包含関係である。対応する型を小文字では じまる名前にするなら、型(正確にはソート)のあいだにも、これとまったく 同じ順序があると考えてよいだろう。まったくの繰り返しとなるが、念のためにソート 集合の順序構造(型階層)を描けば次のとおり。

     'point'
        |
    'latticePoint'

       'polyline'
        /   \
      /       \
'polyline3'   'latticePolyline'
      \       /
        \   /
   'latticePolyline3'

ここで注目すべきことがいくつかある。まず、下の図を眺めて欲しい。

  'point'            'polyline'
     |                   |
 'latticePoint'    'latticePolyline'

'latticePoint'<'point'と'latticePolyline'<'polyline'が無関係とは思 えない。別な言い方をすると、'latticePolyline'<'polyline'である根拠は、 'latticePoint'<'point'にあると思える。さらに言い換えれば、 'latticePoint'<'point'が成立しているという事実から、 'latticePolyline'<'polyline'が推論できてもいいだろう。

同様な事情は、'integer'<'decimal'と'latticePoint'<'point'のあいだに も存在する。つまり、'integer'<'decimal'から'latticePoint'<'point'が 推論できてもいい、いや、できたほうがいい。

フーッ、引用符をつけるのがそろそろ鬱陶しくなってきたので、 ソートを表す場合でも、integerやpointと書くことにする。

「推論できたらいい」という希望を、もう少しハッキリと言っておこう。 integer<decimalは、基本的な関係だから、これは無条件に認めよう。point は、decimalから作られるし、latticePointはintegerから作られる。作り方は、 スカラー(と思う型)からレコード複合型を作る操作である。また、polyline はpointから作られるし、latticePolylineはlatticePointから作られる。作り 方は、正規表現による制限付きのリスト複合型を作る操作である。polylineか らpolyline3を作る操作は、正規表現による制限である。

おおざっぱにいえば、レコード複合型を作る操作、リスト複合型を作る操作、 自由リスト(シーケンス)型を正規表現により制限する操作などを含む型推論 体系があると、折れ線の例のような状況で便利に使えそうである。今回の話で は出てこなかったが、リスト(シーケンス)型からツリー型を作る操作(ツリー 化とでも呼べばよいのか?)もある。

10. 新たな宿題

XMLと相性がよくて、型推論を備えた型システムがあると便利そうだ。それは、 次のような構成素から成り立つだろう。

  1. 基本型システム
  2. いくつかの型構成操作。例えば、レコード構成、自由リスト(シーケンス) 構成、正規表現による制限、ジョイン(ユニオン)、ミート、ツリー化な ど。
  3. いくつかの型から新しい型を構成するときに、型の順序(型階層)を推論 するための推論規則。
  4. 推論以外の、型階層を判断する実効的手段。

4番目の実効的手段を除いた型システムは、形式的体系として定義できる。こ のとき、基本型システムはパラメータになる。形式的体系とみなした型システ ムは、ある種の文法と思えるし、再帰代入系による定式化が可能だと思う(確 証はまだない、多少の拡張が必要かもしれない)。パラメータとなる基本型シ ステムは、結局は順序付きアルファベットとみなせるから、再帰代入系は順序 言語を定義する文法となるだろう。

以上、漠然と述べたことを精密化するのはこれからの宿題だが、形式的体系、 再帰代入系、順序付きアルファベットと順序言語などの素材は、キマイラ・サ イト内に蓄積されつつある。

11. おわりに

この記事は、折れ線の例を、型システムの観点から解説したものであると同 時に、構文的型システムへの第一歩でもある。構文的型システムは(それがで きれば)、XMLとの相性はいいはずである。一方で構文的型システムは、プロ グラミング言語の型システムとは相性が悪い。記事「XML はどこに?」で触れた、2つの地域を隔てる「山」の一部は、この相性の悪 さに起因する。

構文的型システムを構成することが当面の宿題になるが、そのXMLフレンドリー な型システムを、通常の型システムとすりあわせることが、その後にひかえる 大きな課題となる。たぶん、なんとかなるだろう。