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

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

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

参照用 記事

モナドのたぐいとフレイド圏

いつぞや白石さんと会ってお話をしたあたりから、僕はフレイド圏(Freyd category)*1に興味を失ったのですが、最近また「フレイド圏て便利だな」と思い直しました。

というのも、モナドと余モナドと双モナドと、その他なんかモナド類似のナニカとかを使い分けるのにウンザリしてしまったからです。「モナド的代数系と一般化クライスリ圏」において、モナド、余モナド、双モナド、その他モナド類似の諸々をモナド代数系と呼ぼうとか言っているのですが、そもそも、そういうモナド類似物を引き合いに出すのがめんどくさいのです。

フレイド圏を使えば、こういうゴタゴタには言及せずに本質だけを語れます。ここで本質とは、データ型と計算機構の拡張のことです。フレイド圏の構造は、関手 J:CK で与えられます。この関手Jが、もとの圏Cのデータ型と計算機構をKまで拡張することを示しています。拡張方法が具体的にどんなであるかまでは気にしません。

モナドから作るフレイド圏

フレイド圏の典型例はモナドから作るクライスリ圏です。デカルト構造やプレモノイド構造を考慮すべきなんですが、ここでは単に圏の拡張だけに注目します。

F = (F, η, μ) が圏C上のモナドとします。K = Kl(C, F) を、C上のモナドFのクライスリ圏だとします。クライスリ圏を作るとき、対象は特に変えませんから、|C| = |K| です。

クライスリ圏の定義から (k:A→F(B) in C) ⇔ (k:A→B in K) です。C の射 f:A→B に、モナドの単位 ηB:B→F(B) を後結合(post compose)してみると、f;ηB:A→F(B) in C なので、K 内で A→B という射が定義できます。こうして定義されたK内の射をJ(f)と書くことにすると、J:CK という関手になります。Jの対象部分は、J(A) = A という自明な定義をしておきます。

今定義した関手Jの特徴は、対象の上では J(A) = A という自明な全単射となっていることです。他にプレモノイド構造に関する条件を仮定しますが、気にしないことにします。Jが埋め込みであることは要求しませんが、多くの例では埋め込みになっているので、そのときは「CK広い部分圏」だと思ってかまいません。

フレイド圏の別な例

フレイド圏の定義では、関手 J:CK にしか注目しないので、Jがどのような経緯で作られたかはどうでもよくなります。例えば、Kデカルト圏で、Cが広い部分デカルト圏のとき、包含 CK をJとすると、これはフレイド圏となります。極端なケースとして、KK はフレイド圏です。

別な例として、Cデカルト圏、S∈|C| を特定の対象とします。圏Kを次のように定義します。

  • (k:S×A→B in C) ⇔ (k:A→B in K)

(k:A→B K), (h:B→C in K) の結合は、C内で次のような結合 k#h を作り、それをKに持ちあげて解釈して作ります。(ΔSは、Sの対角 S→S×S です。)

  • k#h := (ΔS×idA);(idS×k);h :S×A→C

任意の対象 X∈|C| に対して、!X:X→1 は、終対象(兼デカルト積の単位)である1への唯一の射; λX:1×X→X はデカルト積の左単位律を与える射(自然変換の成分)としましょう。C内の射 f:A→B に対して、J(f) := (!S×f);λS と定義します。

対象に対しては J(A) = A と定義すれば、関手 J:CK を作れます。この J:CK はフレイド圏の例となります。

フレイド圏の使い途

フレイド圏は、圏の拡張、特にデータ型と計算機構の拡張を記述するには便利です。しかし、1つのフレイド圏は1つの拡張方法を表すに過ぎません。たくさんの拡張方法を一度に扱いたいときが多いので、フレイド圏をタバにして使うほうが便利でしょう。

タバにするには、インデックス付き圏を使います。パラメータ化フレイド圏(parameterized Freyd category)という言葉もあるようですが、インデックス付きフレイド圏(indexed Freyd category)でも同じことです。もっとも、フレイド圏をインデックスで束ねたものか、インデックス付き圏がフレイド構造を持つのかで扱いが違ってきます。僕が考えているのは、インデックス圏にフレイド構造が入ったものなので、フレイド・インデックス付き圏(Freyd indexed category)が適切かも知れません。

言葉使いはともかくとして、フレイド圏のタバを使えば、「モナドまたは余モナドまたは双モナド、あるいはその他なんかモナド類似の代数系により…」のようなゴタゴタに言及せずに済むので、だいぶスッキリしそうです。

*1:ここで言うフレイド圏とはまったく別な意味のFreyd categoryもありますのでご注意ください。