Catyにおけるメイヤー指標 - 檜山正幸のキマイラ飼育記 (はてなBlog)

「メイヤー指標」のコメント欄において：

Juppaさん：
> むしろいつも，何の問題を解こうとしているのかが先に示されないまま代数的方法が始まるという印象です．

shiroさん：
> このへんの議論がcatyにどうやって落とし込まれるのか興味を持って見ています。

なんて話もあるので、Caty（動画）におけるメイヤー指標の実装状況／未実装状況を紹介しておきます。

内容：

「コマンド」という言葉に要注意
Catyの指標とモジュール
メイヤー指標の実装
ほんとの目的はトランザクション付き副作用モナド

「コマンド」という言葉に要注意

Catyにおける「コマンド」に特に変わった意味はなくて、「コマンドライン」、「コマンドシェル」、「コマンド言語」といった用法で使う常識的なコマンドのことです。一方、メイヤー先生の「Command-Query分離の原則」のCommandは、副作用として状態遷移を引き起こすメソッドのことです。どちらも command なので混乱しそうです。

ここから先では、カタカナ書きの「コマンド」はCatyのコマンドを含む常識的な意味、英字で「Command」と書いたらメイヤーの意味だとします。

Catyでは、メイヤーの意味のCommandを更新コマンド（updater command）、メイヤーの意味のQueryを読み出しコマンド（reader command）と呼んでいます。対応をまとめておくと：

メイヤー指標	Caty
Operation	コマンド（command）
Command	更新コマンド（updater command）
Query	読み出しコマンド（reader command）
Creator	創生コマンド（creator command）

Catyの指標とモジュール

次は、「コンストラクタやクローニングの表示的意味論：多オブジェクト系とフォック構成 (1)」で例に出した、スタックとカウンターの指標を含む指標モジュールです。

hidden sorts : Stack, Counter;
visible sorts : Integer, Boolean, Error, OK;

signature global() {
  creator newStack :: void -> Stack as stack;
  creator newCounter :: void -> Counter as counter;
}

signature stack(Stack) {
  command push :: Integer -> Stack;
  command pop :: void -> [Stack, (OK | Error)];
  query top :: void -> (Integer | Error);
  query isEmpty :: void -> Boolean;

  creator clone :: void -> Stack as stack;
}

signature counter(Counter) {
  command inc :: void -> Counter;
  command dec :: void -> Counter;
  command reset :: void -> Counter;
  query value :: void -> Integer;
}

これは擬似言語ですが、これと同じことをCatyのスキーマ言語で書くことができます。擬似言語とCatyスキーマ言語は少し違いがありますが、その違いは後で説明することにして、実際のCatyスキーマ定義を以下に。

module sample;

/* visible sorts : 
   Integer => integer
   Boolean => boolean
   OK      => void
*/

exception StackError = deferred object; // 詳細は決めてない

type Stack = foreign;
type Counter = foreign;


@[creator]
command newStack :: void -> Stack /* as stack*/;
@[creator]
command newCounter :: void -> Counter /*as counter*/;


@[signature]
class stack(Stack) {
  @[updater]
  command push :: integer -> void;
  @[updater]
  command pop :: void -> void throws StackError;
  @[reader]
  command top :: void -> integer throws StackError;
  @[reader]
  command isEmpty :: void -> boolean;
  @[creator]
  command clone :: void -> Stack /*as stack*/;
};

@[signature]
class counter(Counter) {
  @[updater]
  command inc :: void -> void;
  @[updater]
  command dec :: void -> void;
  @[updater]
  command reset :: void -> void;
  @[reader]
  command value :: void -> integer;
};

記述している内容は同じだし、ほぼ対応が取れていますが、次の点に注意してください。

主要ソートを持たない指標（のオペレーション宣言）はモジュールのトップレベルに書く*1。
Command, Query, Creatorの違いは、コマンド宣言のアノテーションで示す。対応するアノテーションはそれぞれ、@[updater], @[reader], @[creator]。
指標であることを示すにも、@[signature]アノテーションを使う*2。
現状、as Stack のような書き方はサポートしてない（コメントにしている）。
擬似言語の command push :: Integer -> Stack; では、Commandの戻り値の隠蔽ソートを明示的に書いているが、Catyの更新コマンドでは主要ソートを完全に省略する。
Catyスキーマには、例外型の宣言（exception宣言）とコマンド宣言のthrows節がある。エラーは例外機構で扱える。
可視ソートは、Caty型システムの通常の型に対応する。
隠蔽ソートは、foreign型という特殊な型で表す。foreign型は、Caty型システムからは正体が分からない謎のデータオブジェクトに対して付ける型である。

classというキーワードを使ってますが、オブジェクト指向のクラスのような機能性は持ってません。Catyのclassは、コマンド宣言にまとまりを付ける程度のものだと理解してください。

メイヤー指標の実装

Catyのコマンド実装は、たいていはCatyScriptで書くことができますが、隠蔽ソート（foreign型）を扱うコマンドはPythonで書く必要があります。counterというメイヤー指標に対するPython実装は例えば次のようになります。簡単ですね。

class Counter(object):
    def __init__(self):
        self._value = 0

    def inc(self):
        self._value += 1

    def dec(self):
        self._value -= 1

    def reset(self):
        self._value = 0

    def value(self):
        return self._value

上記のCounterはPythonのクラスなので、CatyScriptからは、そのままでは見えません -- なにしろ隠蔽ソートの実体ですから。PythonとCatyScriptの橋渡しをするために、次のようなグルーイングコードが必要です。グルーイングコードは定型パターンなので、いずれは処理系が勝手に作れるようになると思います。

from caty.command import Command

class NewCounter(Command):
    def execute(self):
        return Counter()

class CounterInc(Command):
    def execute(self):
        self.arg0.inc()

class CounterDec(Command):
    def execute(self):
        self.arg0.dec()


class CounterReset(Command):
    def execute(self):
        self.arg0.reset()

class CounterValue(Command):
    def execute(self):
        return self.arg0.value()

CatyScriptからPythonのクラス／オブジェクトにアクセスするためには、CatyScriptのコマンドをPythonのメソッドにバインドする必要があります。現状では、指標の記述とバインディング記述が分離してなくて、指標そのものを書き換えることになります（良くない！）。以下の、refers宣言節がコマンドとPython実装を結びつけています。

@[creator]
command newCounter :: void -> Counter /*as counter*/ 
  refers python:sample.NewCounter;

class counter(Counter) {
  @[updater]
  command inc :: void -> void 
    refers python:sample.CounterInc;
  @[updater]
  command dec :: void -> void
    refers python:sample.CounterDec;
  @[updater]
  command reset :: void -> void
    refers python:sample.CounterReset;
  @[reader]
  command value :: void -> integer
    refers python:sample.CounterValue;
};

これで、次のような対応関係が確立します。

CatyScriptコマンド	Pythonメソッド
sample:newCounter	Counterのコンストラクタ
sample:counter.inc	Counterのinc()
sample:counter.dec	Counterのdec()
sample:counter.reset	Counterのreset()
sample:counter.value	Counterのvalue()

ほんとの目的はトランザクション付き副作用モナド

今まで述べたような方法で、Pythonのクラス／オブジェクト／メソッドをCatyScriptからアクセスできるようになります。しかし、これだけではたいして面白い話ではありません。CatyScriptのコマンドに対して、系統的に副作用（むしろ主作用ですが）を与えるメカニズムが欲しいのです。実用上の要求から、入れ子トランザクションをサポートする必要があります。圏論的な表示的意味論で言えば、型とコマンド達が形成するベースの圏に対して、副作用モナドによりクライスリ拡張圏を作ることになります。

副作用が働く相手である状態空間はPythonクラスとして定義されます。ある時点での状態点はPythonオブジェクトが保持します。CatyScriptから見ると、Pythonのクラス／オブジェクトは隠れた世界（hidden world）の存在物で、直接的には観測も操作もできません。隠れた世界との通信に利用するワームホールの目印が隠蔽ソート、Catyではforeign型です。

foreign型データ（実は、Pythonネイティブオブジェクトへの参照）を、隠れた実体へのアクセスが許されたCatyコマンド（Pythonメソッドの代理）に渡すと、隠れた実体の観測と操作が可能となります。隠れた実体の受け渡しには、コマンドの第0引数（arg0）を使うことにしています。通常のオブジェクト指向言語のthisやselfにあたるのがarg0です。arg0の使い方はちょっとカッコ悪いので今日は説明しません。シンタックスシュガーが必要だと思っています。

このようなことがだいたい出来ているし、トランザクションも含めて動いてはいるのですが、Creatorをどう扱うか（例えば、トランザクション内で作ってしまったエンティティをどうやって巻き戻しましょうか？）とか、その他細かい（いや、細かくもない）問題がまだ残っています。実際に作ってみてダメならやり直す方法は、開発資源が極小だと採用できないので、机上の思考実験で目星が付いたら実装する手順になります。

いま、思考実験しなくちゃならない課題は、Creator付きメイヤー指標とか、指標のあいだの演算とか、指標と実装の結び付け方とかです。

[追記]ここに書いてあるようなことを試すににも、例えば hg clone https://m_hiyama@bitbucket.org/project_caty/dev としても、たくさんのファイルがあり過ぎて何だかワケ分かんない状況だと思います。今、簡単なパッケージングシステムとインストーラー／アンイストーラーを作っています。これが出来ると、「シェルが動くだけの最小限のシステム」とかを配布パッケージにまとめることができるので、目的ごとの配布が可能になると思います。[/追記]

*1:実際には、globalと同様な書き方も出来ます。あまり使わないだけです。

*2:現状、処理系は@[signature]アノテーションを認識してなくて、コメントの役割りしか果たしてません。