このブログは、旧・はてなダイアリー「檜山正幸のキマイラ飼育記 メモ編」（http://d.hatena.ne.jp/m-hiyama-memo/）のデータを移行・保存したものであり、今後（2019年1月以降）更新の予定はありません。

今後の更新は、新しいブログ http://m-hiyama-memo.hatenablog.com/ で行います。

総称コマンドと関手とモナドとか、あとアイレンベルグ／ムーア構成とか、色々

Caty モナド

記法としては、通常の集合論／圏論の記法よりは、CatyScriptの構文に近い書き方をする。が、最初は一般的かつ抽象的な状況設定、すぐ後で具体的なスクリプトで書く。

Cは、なんか具体的な対称モノイド圏だとする。Cは集合圏の部分圏と仮定してもいい（別になんだっていいけど）。Monoid(C) は、C内のモノイドを対象として、モノイド準同型を射とする圏。もとの圏Cが対称モノイダルなら、そのなかでモノイド概念は意味を持つ。

L:C→C をリスト関手とする。Cが抽象的な圏だと、リスト関手つっても意味がないので、リスト関手が意味を持つ程度には具体的セッティングだとする。Catyの計算モデル圏ではリスト関手は意味を持つ（list<T> と each<T> :: list<T> -> T）。

自己関手Lに、リスト平坦化μとシングルトンリストηを加えてモナドにする。Caty内では、flatten<T> :: list<list<T>> -> list<T> と sing<T> :: T -> list<T> で与えられる。記号の乱用で L = (L, μ, η) と書く。CatyScriptなら次のように書ける。

// Listモナド

type List<T> = [T*];

class List {
 command flatten<T> :: List<List<T>> -> List<T>;
 command sing<T> :: T -> List<T>;
};

classに型パラメータTを付けて、それがメソッド（クラス内コマンド）に行き渡るほうが使いやすいかもしれない。

// Listモナド

type List<T> = [T*];

class List<T> {
 command flatten :: List<List<T>> -> List<T>;
 command sing :: T -> List<T>;
};

型パラメータの具体化が、List.sing<integer> か List<integer>.sing かの違いが出てくる。-- これは横道だった。

Alg(C, L) を、リストモナドLの代数の圏だとする。Alg(C, L) はLのアイレンベルグ／ムーア圏（http://d.hatena.ne.jp/m-hiyama/20110930/1317376793）だ。

モノイドの表現

Monoid(C) の対象はC内のモノイドだが、これは次のものから構成される。（最初に注意したように、記法はCatyScript風。）

  1. 台集合 T （TはCの対象）
  2. 二項演算 op :: [T, T] -> T ;
  3. 単位元 unit :: void -> T ;

演算が単位的かつ結合的なら、3つ組 (T, op, unit) がモノイドとなる。

例えば、num:add :: [number, number] -> number はモノイドを定義するが、次のように書くとハッキリするかも。

// NumAddモノイド

class NumAdd {
 command op :: [number, number] -> number {
   num:add
 };
 command unit :: void -> number {
   0
 };
};

モノイド概念の抽象的定義である指標（インターフェイス）は次のよう。

// モノイドの指標

@[signature]
class Monoid {
 command op<T> ::  [T, T] -> T;
 command unit<T> :: void -> T;
};

型パラメータTがclassに付けられるなら：

// モノイドの指標

@[signature]
class Monoid<T> {
 command op ::  [T, T] -> T;
 command unit :: void -> T;
};

NumAddは、指標Monoid<T> の型パラメータTを具体型numberで具体化しているから、

  • NumAdd conforms Monoid<number>

となる。conforms は適合性（conformance）を表しているが、リスコフ置換可能性のこと。実装を持つクラスも指標クラス（実装なしのインターフェイス）も、振る舞い制約（CatyFITによる表明セット）とともにリスコフ置換可能性による順序構造を持つ。って、これも横道だった。

ともかくも、台集合がTであるモノイドは、二項演算 op :: [T, T] -> T; と単位元 unit :: void -> T; で表現される、ってこと。

アイレンベルグ／ムーア代数

リストモナドLに限定して言うと、a:L(T)→T というCの射がある条件を満たすとき、(T, a) を、Lのアイレンベルグ／ムーア代数（あるいは単に代数）と呼ぶ。CatyScriptで書けば：

// アイレンベルグ／ムーア代数

@[signature]
class EMAlg {
  command em-op<T> :: List<T> -> T;
};

あるいは、

// アイレンベルグ／ムーア代数

@[signature]
class EMAlg<T> {
  command em-op :: List<T> -> T;
};

モノイドとアイレンベルグ／ムーア代数の相互変換

圏Cに対して、Monoid(C) と Alg(C, L) は圏同値であることが知られている。つまり、Monoid(C) と Alg(C, L) は事実上同じものだ。これは、up-to-isoで互いに逆になる関手 U:Monoid(C)→Alg(C, L)、B:Alg(C, L)→Monoid(C) がある。このUとBをCatyScriptで書き下してみる。

まず、B:Alg(C, L)→Monoid(C) のほうが簡単だから先にやる。アイレンベルグ／ムーア代数にモノイドを対応させる関手がBだが、関手Bの対象対応の部分 |Alg(C, L)|→|Monoid(C)| だけを考えると、二項演算opと単位元unitからアイレンベルグ／ムーア演算em-opを作ればよい。

CatyScriptは本物の高階引数は取れないから、代わりに演算の名前（文字列）を引数にする。

// アイレンベルグ／ムーア代数の演算から二項部分だけを取り出す
  
type operator = string(remark="高階引数の代わりに使う演算名の文字列");

command binary-part<T> [operator em-op /* em-op :: List<T> -> T */] :: [T, T] -> T {
  pass > in;
  %1   > em-op;
  
  %in | call %em-op
};

pass > in; %1 > em-op; が、CatySriptの鬱陶しい部分が出てしまっているが、まー定義は簡単だ。

逆向きの関手は、二項演算opと単位元unitから、em-op :: List -> T を作ればいいが、List -> T の形の演算をunbiased演算と言うので、「二項演算 → unbiased演算」の高階コマンド（もどき）を定義する。

type operator = string(remark="高階引数の代わりに使う演算名の文字列");

command unbiased<T> [operator op /* op:: [T, T] -> T*/, T unit] :: [T*] -> T {
 pass > in;
 %1   > op;
 %2   > unit;

 %in |
 cond {
   [] => %unit,
   [T] => nth 1, /* (A) */
   [T, T] => call %op, /* (B) */
   * =>
     pass > in2 | [nth 1, nth 2] | call %op > bin-result;
     [[%bin-result],  (%in2 | list:slice 2)] | list:concat > rest;
     %rest | unbiased<T> %op %unit /* (C) */
   ,
 }
};

実は、これは現状では動かない。(A), (B), (C) と書いてあるところが動かない原因。動くように手直しすると：

kind LowerAny = lower any;

command unbiased<T in LowerAny default any> [operator op /* op:: [T, T] -> T*/, any unit] :: [T*] -> T {
 pass > in;
 %1   > op;
 %2   > unit;

 %in |
 cond {
   [] => %unit,
   [any] => nth 1, /* (A) */
   [any, any] => call %op, /* (B) */
   * =>
     pass > in2 | [nth 1, nth 2] | call %op > bin-result;
     [[%bin-result],  (%in2 | list:slice 2)] | list:concat > rest;
     %rest | call u:unbiased %op %unit /* (C) */
   ,
 }
};

これはちゃんと動く（結果オーライだ）が、型パラメータの処理は不十分。コマンドの定義体であるスクリプトコード内に出現する型パラメータ参照が処理できてない。しょうがないので、定義体で型パラメータを使うのはやめて、anyで代用している。(C) が call u:unbiased %op %unit となっているのは現在の制限回避の書き方で、そのうち、unbased %opt %unit と書けるだろう。

型スキーム、コードスキームと総称コマンド

List<List> とか List<T> -> T のように、型パラメータを含む型表現を型スキームと呼ぶことがある（http://d.hatena.ne.jp/m-hiyama/20120405/1333608868）。構文上、型パラメータと定義済み型名の区別はできないので、どれが型パラメータかを明示する必要がある。式のなかのパラメータを特定することはラムダ抽象と似ているので、大文字ラムダを使うことにすると：

  • Λ<T>.List<List>
  • Λ<T>.(List<T> -> T)

(List<T> -> T) は指数型だが、Catyではプロファイルと呼んで通常の型とは別な扱いにしている（指数型を正式には認めてない）。よって、二番目はプロファイル・スキームとでも呼ぶべきだが、型スキームでもいいや。

型スキームは、型パラメータを持った型表現（またはプロファイル）だが、型パラメータを持ったスクリプトコードという概念がある。これはコードスキームと呼ぶことにしよう。コードスキームは、型名を変数（プレースホルダー）に持つテンプレートとかマクロとか言ってもいいが、いわゆる「テンプレート」以外の実現方法もある。

「プロファイルにも定義体のコードにも型パラメータを含んだコマンド」が、総称コマンド。現在、プロファイルに出現する型スキームの具体化には対応してるが、定義体がコードスキームになる場合がサポートされてない。

総称コマンドでは、プロファイル（例外やシグナルの宣言も含む）が型スキームになっていて、定義体はコードスキームになっている。実行の前に、型スキームを具体化して具体型に、コードスキームを具体化して具体コードにする必要がある。コンパイル時に具体化するのが望ましいが、実行時型引数があると、実行時まで具体化できないこともある。

コードスキームに登場する型パラメータ参照を発見・特定しなくちゃならんが、cmd<Type> の形以外に、case と cond の分岐条件部分に型パラメータが出現する可能性がある。とはいえ、出現位置は決まっているので、発見・特定が困難ということはない。

圏論とCatyScript

CをCatyの計算モデル圏とすると：

  • CatyScriptの型 ＝ Cの対象
  • CatyScriptのコマンド ＝ Cの射

となる。コマンドとスクリプトはあまり区別する必要はない（名前のあるなし程度）。

型パラメータTを含む型関数、例えば Λ<S, T>.[S, T]、Λ<T>.[T*] とかは、Cの対象に対象を対応させるので、通常は自己関手の対象部分として使う。

コマンドにコマンドを対応させる高階コマンドは、CatyScriptに正式にはないが、コマンド名文字列を引数にするコマンドで代用できる。これで、関手の射部分を書ける。例えば：

class List {
 // ...
 command map<T> [string cmd] :: List<T> -> List<T> {
  each {call %1}
 };
};

このList.mapは、型パラメータTを持っているので、cmd :: A -> A を (map<A> cmd) :: List<A> -> List<A> に移している。つまり、自然変換。通常、自然変換の下付き添字として書く対象が、総称コマンドの型パラメータとして現れる。

まとめると：

  1. 型関数 ： 関手の対象部分
  2. 高階コマンド ： 関手の射部分
  3. 総称高階コマンド ： 自然変換

となる。もちろん、関手と自然変換以外の定義に総称や高階モドキを使ってもいい。

かなりのところ総称をサポートしているのに、指数型や高階コマンドを正式サポートしないのは中途半端だが、切実な必要性がないならやらない。