リストの累積コモナド、TypeScriptで - 檜山正幸のキマイラ飼育記 (はてなBlog)

「TypeScriptと関手やモナドなど」において、TypeScriptでリストモナドを書いてみたのですが、コモナド（モナドの双対概念）も扱ってみます。

通常、リストモナドと呼ばれているものは、リスト関手の上の載っている自然変換による代数構造です。同じリスト関手の上に別な代数構造が載ることもあります。そのひとつ、リストの累積コモナドを紹介します。記述にTypeScript（JavaScriptの拡張言語）を使うので、「リスト」の代わりに「配列」という言葉を使います。

内容：

累積配列
コモナド（余モナド）
コモナド法則
余クライスリ圏

累積配列

配列 [a0, a1, ..., aN] に対して、[[a0], [a0, a1], ...., [a0, a1, ..., aN]] を（もとの配列の）累積配列と呼びましょう。もとの配列の項目が a_i （0 ≦ i ≦ N）ならば、累積配列のk番目の項目は [a₀, ..., a_k] （0 ≦ k ≦ N）です。

累積配列を求めるJavaScript関数は：

function Array_accum(ax) {
    if (ax.length === 0) throw "Empty Array"
    var result = [];
    var item = [];
    for (var k = 0; k < ax.length; k++) {
	item.push(ax[k]);
	result.push([].concat(item)/*コピー*/);
    }
    return result;
}

関数の入り口で空配列を除外しています。空配列の累積配列は考えないことにします。

ここからTypeScriptを使うとして、Array_accumに無駄に丁寧な型宣言を付けてあげると*1：

function Array_accum<X> (ax:Array<X>) : Array<Array<X>> {
    if (ax.length === 0) throw "Empty Array"
    var result:Array<Array<X>> = [];
    var item:Array<X> = [];
    for (var k:number = 0; k < ax.length; k++) {
	item.push(ax[k]);
	result.push([].concat(item)/*コピー*/);
    }
    return result;
}

配列の最後の項目を取り出す関数もゴージャスな型宣言付きで書いておきます。

function Array_last<X> (ax:Array<X>) : X {
    if (ax.length === 0) throw "Empty Array"
    return ax[ax.length -1]
}

もし、非空配列（non-empty array）の型 NEArray<X> が定義できるなら、実行時チェック if (ax.length === 0) throw "Empty Array" の代わりに型システムの静的チェックが使えます。累積配列と最後の項目の意図から言えば、次の宣言が正確です。

function NEArray_accum<X> (ax:NEArray<X>) : NEArray<NEArray<X>> ;

function NEArray_last<X> (ax:NEArray<X>) : X ;

現実にはNEArray型は使えませんが、以下の説明ではNEArray型が存在するかのごとくに書きます。

コモナド（余モナド）

型パラメータ付きのNEArray型、そのマップ関数であるNEArray_fmap、累積配列の作成NEArray_accum、最後の項目の取り出しNEArray_last、これらはコモナド（余モナド）を構成します。（NEArray_fmapは、「TypeScriptと関手やモナドなど」で定義したArray_fmapを流用できます。）

モナドは知っていても、コモナドは聞いたことない方もいるでしょう。コモナドはモナドの双対です。モナドが関手に載ったモノイド構造であるのに対して、コモナドは関手に載ったコモノイド構造です。コモノイド（余モノイド）は余乗法と余単位からなり、余単位律と余結合律を満たします。

圏Cの自己関手F上のコモナドを (F, δ, ε) とします。δとεは自然変換で：

余乗法自然変換 δ::F⇒FF:C→C
余単位自然変換 ε::F⇒I:C→C （Iは恒等関手）

並置を自然変換の横結合、「;」を自然変換の縦結合として、コモナド法則は：

左余単位律 δ;εF = F
右余単位律 δ;Fε = F
余結合律 δ;δF = δ;Fδ

一般的なコモナド概念と今回の具体例には、次の対応があります。

一般的なコモナド	累積配列コモナド
圏の対象	型X
圏の射	関数 f: (x:X) => Y
関手Fの対象部分	NEArray<X> 型構成子
関手Fの射部分	NEArray_fmap<X, Y> 総称関数
余乗法δ	NEArray_accum<X> 総称関数
余単位ε	NEArray_last<X> 総称関数

コモナド法則

コモナド法則を総称関数のあいだの等式で書いてみると次のようになります。

左余単位律 NEArray_last(NEArray_accum(ax)) = ax
右余単位律 NEArray_fmap(NEArray_last)(NEArray_accum(ax)) = ax
余結合律 NEArray_accum(NEArray_accum(ax)) = NEArray_fmap(NEArray_accum)(NEArray_accum(ax))

TypeScriptで書いた Array_fmap, Array_accum, Array_last でも、空配列を渡さないように注意すれば、等式は成立します。例えば、次のようなテスターで確認できます。テスター内の型宣言はそれほど厳密ではありません、面倒なのでテキトーに実行時型チェックを併用しています。

function testArrayEq(
    lhs: (arr:Array<any>)=>Array<any>, 
    rhs: (arr:Array<any>)=>Array<any>, 
    from: number, 
    to: number
) : boolean
{
    function makeArray(n:number) : Array<number> {
	var arr:Array<number> = [];
	for (var i:number = 0; i < n; i++) {
	    arr.push(i);
	}
	return arr;
    }
    function arrayEq(a1:Array<any>, a2:Array<any>) : boolean {
	if (a1.length !== a2.length) return false;
	for (var i:number = 1; i < a1.length; i++) {
	    var eq:boolean;
	    if (typeof a1[i] === 'object') {
		// 面倒なので、配列以外のオブジェクトは除外する
		// nullも除外される、undefinedは残るがまーいいでしょう。
		if (! (a1[i] instanceof Array)) throw "Cannot accept non-array object"
		// a1[i] は配列
		eq = arrayEq(a1[i], a2[i]);
	    } else {
		eq = (a1[i] === a2[i])
	    }
	    if (!eq) return false;
	}
	return true;
    }

    for (var k:number = from; k <= to; k++) {
	var arr:Array<number> = makeArray(k);
	if (! arrayEq(lhs(arr), rhs(arr))) {
	    return false;
	}
    }
    return true;
}


var result:boolean;
// 左余単位律
result = testArrayEq(
    (ax)=>{return Array_last(Array_accum(ax));},
    (ax)=>{return ax;},
    1,
    10);
console.log(result)

// 右余単位律
result = testArrayEq(
    (ax)=>{return Array_fmap(Array_last)(Array_accum(ax));},
    (ax)=>{return ax;},
    1,
    10);
console.log(result)

// 余結合律
result = testArrayEq(
    (ax)=>{return Array_accum(Array_accum(ax));},
    (ax)=>{return Array_fmap(Array_accum)(Array_accum(ax))},
    1,
    10);
console.log(result)

有限個の特殊例のチェックなんて信用できん、て方は、やっぱり証明支援系かしら :-)

余クライスリ圏

(F, δ, ε) が圏C上のコモナドのとき、モナドのクライスリ圏とまったく同様に（ただし双対的に）余クライスリ圏を構成できます。

f:F(X)→Y in C の形の射を、（コモナドに関する）余クライスリ射と呼びます。2つの余クライスリ射 f:F(X)→Y と g:F(Y)→Z に対して、それらの余クライスリ結合 f#g を δ_X:F(X)→FF(X), F(f):FF(X)→F(Y), g:F(Y)→Z の結合 δ_X;F(f);g で定義します。そして、cid_X := ε_X :X→F(X) とします。これは余クライスリ恒等。このとき：

(f#g)#h = f#(g#h)
cid_X#f = f
f#cid_Y = f

が成立します。なので、次のようにして圏Dを定義できます。

|D| := |C|
D(X, Y) := C(F(X), Y)
結合は#
単位はcid

この圏Dが、C上のコモナド (F, δ, ε) の余クライスリ圏です。

モナドのクライスリ圏が、ベースの圏Cの計算概念を拡張した圏であるのと同様に、コモナドの余クライスリ圏も計算概念の拡張を与えます。典型的な例は、大域的な環境がEで表されるとき、関手 F(X) = E×X 上に、δ_X:E×X→E×(E×X) をEの対角 Δ_X:E→E×E を使い定義して、ε_X:E×X→X を直積の射影（環境を無視する）とするものです。このコモナド *2の余クライスリ圏は、「大域環境を参照する計算」の圏となります。

「大域環境を参照する計算」の場合、計算の入力の情報がXから F(X) = E×X に増えているのですが、配列（リスト）関手の場合も、入力情報がXからXの有限順序列に増えます。どちらも、入力情報がより豊かになった場合の計算を扱うことになります。

配列のインデックスを離散時刻と考えると、配列関手や累積コモナドが、時間の扱いに使えないかな？とか思ったり思わなかったり。

*1:var k:number = 0 なんてのは、容易に型推論できるので、実際に無駄です。しかし、初期値が空配列 [] の型はその時点での型推論は無理です。後々の使い方から推論できるかも知れませんが、人の意図なのでこれは手で書くものだと思います。

*2:任意の集合の対角と終対象への射が、集合圏のコモノイドになります。当該のコモナドは、対角コモノイドのスタンピング・コモナドです。「スタンピング」は「集合の直積で掛け算する」という程度の意味です。