このブログの更新は Twitterアカウント @m_hiyama で通知されます。
Follow @m_hiyama

メールでのご連絡は hiyama{at}chimaira{dot}org まで。

はじめてのメールはスパムと判定されることがあります。最初は、信頼されているドメインから差し障りのない文面を送っていただけると、スパムと判定されにくいと思います。

参照用 記事

インデックス付き圏を使ってオブジェクト指向風計算を定式化してみる

不純な計算のモデルとしてモナドは強力ですけど、万能ってわけではないですね。例えば、オブジェクト指向風の計算は状態概念を伴います。状態付き計算にモナドを使えますが、あんまり適切じゃない気がするのです。もっと直接的に状態を更新する計算を定式化してもいいのじゃないだろうか、と。

それで、モナドとは別な方法により状態付き計算を考えてみます。状態空間Sに対して、S上のメソッドの全体をMethodSとします。MethodSは圏であり、その部分圏がクラスに相当します。複数のクラスとそのあいだの継承関係はインデックス付き圏(indexed category)により表現します。

内容:

  1. 状態を含む計算
  2. 射影の圏
  3. インデックス付き圏と継承
  4. それから

状態を含む計算

Cデカルト圏だとします。つまり、Cには終対象と直積があり、それによりモノイド圏の構造 (C, ×, 1) を持つということです。Cデカルト圏なら何でもいいのですが、集合圏Setの部分圏と考えると分かりやすいでしょう。例えば、有限集合の圏とか高々加算な集合の圏とかです。

Cの対象Sを一つ固定して、C[S] という圏を作ります。記号を簡単にするため、D = C[S] としましょう。

  1. Dの対象類は、Cの対象類と同じである。つまり、|D| = |C| 。
  2. A, B∈|D| に対して、D(A, B) = C(S×A, S×B)
  3. A∈|D| に対して、idA:A→A in D は、idS×A in C とする。
  4. f:A→B, g:B→C in D の結合 f;g:A→C in D は、対応する f:S×A→S×B, g:S×B→S×C in C の結合とする。

こうして作った D = C[S] は圏となります。通常のプログラミングとの関係を示唆するために、C[S] を MethodS とも書きます。また、もとの圏 C を Function とも書きます。

C[S]の作り方から、次は明らかです。

  1. C[S](A, B) = C(S×A, S×B) というホムセットの同型(実際はイコール)がある。
  2. C[1] は C と圏として同型。

記法を変えて言えば:

  1. MethodS(A, B) = Function(S×A, S×B)
  2. Method1 は Function と圏として同型。

これらの事実は、純粋関数を使ってメソッドを表現でき、純粋関数はメソッドの特別なものとみなせることを意味します。

射影の圏

Cから、もうひとつ別な圏を作っておきます。デカルトCのなかで「射影」(projection)とみなせる射だけからなる部分圏を Proj(C) とします。p:A→B in C が射影であるとは次のことです。

  • Cの対象Dと、同型 i:A→D×B があり、p = i;π と書ける。ここで、πは、D×BからBへの標準的第二射影。

要するに、pは π:D×B→B と同等な射だってことです。以下では、記号の乱用で、A = D×B という同一視をして、pを標準第二射影πと同一視することがあります。

定義から、C内の射影の全体は圏となるので、これを P = Proj(C) と置きます。圏Pの対象類|P|は、|C|です。また、恒等と結合もCのモノをそのまま使います。

インデックス付き圏と継承

p:T→S を射影とします。前節で注意した記号の乱用を使えば、T = D×S, p:D×S→S と書けます。MethodS = C[S], MethodT = C[T] などは既に述べたメソッド(=状態空間付きの関数)の圏です。この状況で、p*:C[S]→C[T] という関手を作れることを見ます。

C[S]、C[T] の対象類は|C|でした。これから考える関手の対象部分(object part)は、|C|の恒等写像だとします。これにより関手の対象部分は特に考えなくていいことになります。

関手 p*:C[S]→C[T] をホムセットごとに分割すると、p*:C[S](A, B)→C[T](A, B) という写像の族になります(正確に書けば、p* は p*A,B です)。f∈C[S](A, B) ごとに p*(f)∈C[T](A, B) を決めていけばいいのです。

f∈C[S](A, B) とは、f:S×A→S×B in C でした(定義より)。また、T = D×S でした。このDを f に直積で掛け算します。すると、D×f:D×(S×A)→D×(S×B) in C となります。掛け算の結合律から、D×f:(D×S)×A→(D×S)×B in C とみなしてもかまいません。D×f:(D×S)×A→(D×S)×B in C は、D×f:T×A→T×B in C なので、結局、D×f:A→B in C[T] です。

以上の f |→ D×f という対応は、射影 p:T→S に基づいて定義された関手 p*:C[S]→C[T] となっています。もう少し調べると次の事実もわかります。

  • S∈P ごとに C[S] という圏が対応している。
  • p:T→S in P ごとに関手 p*:C[S]→C[T]が対応している。
  • C[-], (-)* は、PCat という関手になっている。

これはつまり、C[-] が((-)*と共に)インデックス付き圏となっていることです。

このインデックス付き圏のファイバー C[S] は、状態空間Sを持つメソッドの圏 MethodS です。ベース圏Pの射 p:T→S は、T = D×S という直積分解を与えるものですが、これは、SからTへの継承階層を定義し、Dがその差分となっています。pから定義される関手 C[S]→C[T] がメソッドの自然な(オーバーライドなしの)継承 MethodS→MethodT となっています。

それから

以上の定式化は、状態空間とメソッドのモデルとしては直接的・直感的なものだと思います。多くの現実の実装が採用している方式と同じで、メソッドはthisとかselfとかの暗黙の引数を持つことにより実現されます。大域関数はthisの値がvoidであるメソッドとみなされます。

この定式化と、インスティチューション、ホーアトリプル、余代数などの関係を考えてみると面白いかも(あるいは面白くないかも)しれません。