フリー・モナド変換子のために - 檜山正幸のキマイラ飼育記 (はてなBlog)

過去記事「フリーモナド 1：自由で無料な木」において、フリーモナドの説明をしました。その過去記事の冒頭は次のようでした：

説明には、多くの場合、HaskellコードまたはHaskell風擬似コードが使われています。プログラミング言語としてのHaskellの利便性が、当該メカニズムの圏論的内実を抽出するときにはむしろ仇になります。それで苦労している人へのアドバイス／解説がこの記事の内容です。

フリーモナドの先に、フリー・モナド変換子〈free monad transformer〉*1というものが出てきます。フリー・モナド変換子は、概念的にもだいぶ難しいですが、その定義と説明がHaskellコードまたはHaskell風擬似コードで行われると、その解釈（あるいは翻訳）で消耗します。今回も「苦労している人へのアドバイス／解説」ですが、幾つかのヒントだけで系統的な説明にはなっていません。$`\newcommand{\cat}[1]{\mathcal{#1} }
\newcommand{\mrm}[1]{\mathrm{#1} }
\newcommand{\In}{\text{ in }}
\newcommand{\id}{\mrm{id}}
\newcommand{\K}{\mathrm{K} }
\newcommand{\Iff}{\Leftrightarrow}
\newcommand{\u}[1]{\underline{#1}}
\require{color} % 緑色
\newcommand{\Keyword}[1]{ \textcolor{green}{\text{#1}} }%
\newcommand{\For}{\Keyword{For } }%
\newcommand{\Where}{\Keyword{Where } }%
`$

内容：

関数／関手のアフィン化
関手の記述方法：次元ワイルドカード
アフィン化のHaskell風記述 FreeF
モッジの再開モナド
フリー・モナド変換子と再開モナド構成子
不動点方程式とFreeT

関数／関手のアフィン化

フリーモナドもフリー・モナド変換子も、不動点理論の圏論バージョンに依拠しています。頻繁に現れる不動点方程式はアフィン型不動点方程式〈affine-type fixed point equation〉です（「不動点方程式／不動点不等式と不動点オペレーター // アフィン型不動点方程式」参照）。

ここでの「アフィン」は、アフィン線形写像にちなんだものです。アフィン線形写像は、線形写像に定数項を足した形のものです。一番簡単な例は：

$`\quad g:{\bf R}\to{\bf R}\\
\quad g(x) := a + cx
`$

これを一般化すると、任意の関数 $`f`$ に定数項を足した関数を考えることができます。

$`\quad g:{\bf R}\to{\bf R}\\
\quad g(x) := a + f(x)
`$

ここで、定数項 $`a`$ も変数〈パラメータ〉だと思えば：

$`\quad g:{\bf R}\times {\bf R}\to{\bf R}\\
\quad g(a, x) := a + f(x)
`$

あるいはカリー化して：

$`\quad g:{\bf R} \to \mrm{Map}({\bf R}, {\bf R})\\
\quad g(a) := \lambda\, x.(\,a + f(x)\,)
`$

$`g`$ は $`f`$ と $`a`$ から決まるので、$`(f, a)\mapsto g`$ という高階関数に $`\mrm{aff}`$ という名前を付けると：

$`\For f\in \mrm{Map}({\bf R}, {\bf R})\\
\For a\in {\bf R} \\
\quad \mrm{aff}(f, a) := \lambda\, x\in {\bf R}.(\,a + f(x) \;\in {\bf R}\,)
`$

この定義から、$`\mrm{aff}`$ のプロファイルは次のようだと分かります。

$`\quad \mrm{aff} : \mrm{Map}({\bf R}, {\bf R})\times {\bf R} \to \mrm{Map}({\bf R}, {\bf R}) \In {\bf Set}`$

集合圏の指数〈内部ホム〉をブラケットで表すなら：

$`\quad \mrm{aff} : [{\bf R}, {\bf R}]\times {\bf R} \to [{\bf R}, {\bf R}] \In {\bf Set}`$

これは、与えられた自己関数に定数項を付け足した関数を作る操作ですが、関数のアフィン化〈affinization〉と呼んでおきます。アフィン化には、足し算が必要なことに注意してください。

関手のアフィン化も同様です。“圏の圏”の指数〈内部ホム〉である関手圏もブラケットで表すとして、次のように書けます。以下、$`\cat{C}`$ は直和（足し算）を持つ圏とします。

$`\For F\in |[\cat{C}, \cat{C}]|\\
\For A\in |\cat{C}|\\
\quad \mrm{Aff}(F, A) := \lambda\, X\in |\cat{C}|.(\,A + F(X) \;\in |\cat{C}|\,)
`$

上の定義だけだと、$`\mrm{Aff}`$ のプロファイルは次のようです。

$`\quad \mrm{Aff} : |[\cat{C}, \cat{C}]|\times |\cat{C}| \to \mrm{MAP}(|\cat{C}|, |\cat{C}|) \In {\bf SET}`$

しかし、容易な拡張により次のように解釈できます。

$`\quad \mrm{Aff} : [\cat{C}, \cat{C}]\times \cat{C} \to [\cat{C}, \cat{C}] \In {\bf CAT}`$

「容易な拡張」と書きましたが、「容易だから明示的に書かない」ことになり、暗黙の前提になります。しかし、人によっては必ずしも容易ではないし、暗黙の前提は理解を妨げる元凶です。

関手の記述方法：次元ワイルドカード

この節では、型構成子〈コンストラクタ〉が関手にまで容易に（あるいは自動的に）拡張できる状況を説明します。圏 $`\cat{C}`$ と自己関手 $`F:\cat{C} \to \cat{C}`$ 、それと対象 $`A\in |\cat{C}|`$ は一旦固定しておきます。

$`\mrm{Aff}(F, A)`$ が関手であるためには、対象パートと射パートが必要です。前節の定義は対象パートだけでした。射パートも書くと次のようになるでしょう。

$`\quad\mrm{Aff}(F, A) :=
\left\{
\begin{array}{l}
\lambda\, X\in |\cat{C}|.(\, A + F(X) \;\in |\cat{C}|\,)\\
\lambda\, f\in \mrm{Mor}(\cat{C}).(\, \id_A + F(f) \;\in \mrm{Mor}(\cat{C})\,)
\end{array}
\right.
%`$

対象パートも射パートもちゃんと書けば正確になりますが、記述は面倒になります。面倒だから対象パートだけ書いて「後は各自補ってね」となるわけです。

対象パートと射パートを同時に書く方法を考えてみましょう。まず、n-圏 $`\cat{C}`$ のk-射全体の集合を
$`\quad |\cat{C}|_k`$
と書きます。特に：

$`\quad |\cat{C}|_0 = |\cat{C}| = \mrm{Obj}(\cat{C})\\
\quad |\cat{C}|_1 = \mrm{Mor}(\cat{C})
`$

「k-射として所属する」を意味する記号 '$`\in_k`$' を次のように定義します。

$`\quad x \in_k \cat{C} :\Iff x \in |\cat{C}|_k`$

特に：

$`\quad x \in_0 \cat{C} :\Iff x \in |\cat{C}|\\
\quad x \in_1 \cat{C} :\Iff x \in \mrm{Mor}(\cat{C})
%`$

「なんらかの次元の射として所属する」を意味する記号 '$`\in_*`$' は次のように定義します。

$`\quad x \in_* \cat{C} :\Iff \exists k \in\{0, 1, \cdots, n\}.x\in_k \cat{C}`$

次のように定義しても同じです。

$`\quad x \in_* \cat{C} :\Iff x \in \sum_{k = 0}^n |\cat{C}|_k`$

右下付きのアスタリスクは、任意の次元（ただし、n 以下）に具体化できるワイルドカードになっています。この記法を使って $`\mrm{Aff}(F, A)`$ を記述してみます。

$`\quad\mrm{Aff}(F, A) :=
\lambda\, x \in_* \cat{C}.(\, \K_A(x) + F(x) \;\in_* \cat{C}\,)
%`$

ここで、$`\K_A`$ は定数関手で次のように定義されます。

$`\quad \K_A :=
\left\{
\begin{array}{l}
\lambda\, X\in |\cat{C}|.(\,A \;\in |\cat{C}|\,)\\
\lambda\, f\in \mrm{Mor}(\cat{C}).(\, \id_A \;\in \mrm{Mor}(\cat{C})\,)
\end{array}
\right.
%`$

ラムダ束縛変数を使わずに、関手をポイントフリースタイルで書くこともできます（$`\Delta`$ は対角関手、$`*`$ は関手の図式順結合）。

$`\quad\mrm{Aff}(F, A) := \Delta_{\cat{C}} * (\K_A \times F)*(+) \;:\cat{C}\to\cat{C} \In {\bf CAT}
%`$

最初に出した「面倒だから対象パートだけ書く」方式も許容するために、次の便宜上の約束をしましょう。

関手を表す式〈expression〉のなかに対象 $`A`$ が出てきたときには、定数関手 $`\K_A`$ の適用だとみなす。

この約束のもとでは、次は射パートも定義しています。型構成子〈コンストラクタ〉だけではなく、関手を一挙に定義しているのです。

$`\quad\mrm{Aff}(F, A) :=
\lambda\, x \in_* \cat{C}.(\, A + F(x) \;\in_* \cat{C}\,)
%`$

アフィン化のHaskell風記述 FreeF

次のようなHaskell風（あるいはHaskellそのもの）の記述があります。

data FreeF f a x 
  = Pure a 
  | Free (f x)

これは関手のアフィン化を意味しています。ただし、「容易だから明示的に書かない」「面倒だから、後は各自補ってね」というスタイルで書かれています。

Haskell構文と言語処理系の型推論機能により、次のことは分かります。

a と x は、型変数
f は、型構成子を表す変数

型構成子 f は“気持ちの上では”関手なので、圏 $`\cat{C}`$ における解釈は次のようになります。

$`A`$ と $`X`$ は、圏 $`\cat{C}`$ の対象
$`F`$ は、圏 $`\cat{C}`$ 上の自己関手

$`\cat{C}`$ は集合圏の部分圏だと考えて、「フリーモナド 1：自由で無料な木」で述べたタグ付きユニオン記法を使うと、上記のHaskell風data定義は次のように解釈できます。

$`\quad \mrm{FreeF}(F, A, X) := (\text{@Pure } A) \cup (\text{@Free }F(X))\\
\qquad \cong A + F(X)
%`$

アフィン化として我々が使っていた名前 $`\mrm{Aff}`$ にリネームして、引数の渡し方も $`\mrm{Aff}`$ に合わせると：

$`\For F:\cat{C} \to \cat{C} \In {\bf CAT}\\
\For A, X \in |\cat{C}|\\
\quad \mrm{Aff}(F, A)(X) := A + F(X) \; \in |\cat{C}|
%`$

繰り返しになりますが念の為、前節で述べた方法（次元ワイルドカード）を使って射パートも一緒に定義するなら：

$`\For F:\cat{C} \to \cat{C} \In {\bf CAT}\\
\For A \in |\cat{C}|\\
\For x \in_* \cat{C}\\
\quad \mrm{Aff}(F, A)(x) := A + F(x) \; \in_* \cat{C}
%`$

あるいは：

$`\For F:\cat{C} \to \cat{C} \In {\bf CAT}\\
\For A \in |\cat{C}|\\
\quad \mrm{Aff}(F, A) := \lambda\,x \in_* \cat{C}.(\, A + F(x) \; \in_* \cat{C}\,) \; :\cat{C} \to \cat{C} \In {\bf CAT}
%`$

今述べたような“定義の関手への拡張”は、Haskellの deriving Functor を使うと、ある程度は出来るようです。

さらに、「容易だから明示的に書かない」「面倒だから、後は各自補ってね」のなかには、対象を表す $`F\in |[\cat{C}, \cat{C}]|`$ と $`A\in |\cat{C}|`$ を射にまで広げて、$`\mrm{Aff}`$（a.k.a. FreeF）を次の関手にまで拡張する作業まで入っているかも知れません。

$`\quad \mrm{Aff} : [\cat{C}, \cat{C}]\times \cat{C} \to [\cat{C}, \cat{C}]\In {\bf CAT}`$

暗黙の前提、恐るべし。

モッジの再開モナド

ザッと探した感じでは、フリー・モナド変換子に対する圏論的にハッキリした説明は見つからなかったのですが、どうやら起源はモッジ*2〈Eugenio Moggi〉の再開モナド〈resumption monad〉というものらしいです。次のテキストが初出らしいのですが、"resumption monad" と文字列検索してもありません。なんか別な名前で初登場したのでしょうか。

Title: An Abstract View of Programming Languages
Author: Eugenio Moggi
Date: 1989
Pages: 51p
URL: https://www.ics.uci.edu/~jajones/INF102-S18/readings/09_Moggi.pdf

再開モナドは、単一のモナドのことではなくて、与えられたモナドを与えられた自己関手で変形して別なモナドを作る構成手続き〈construction procedure〉のことです。

圏 $`\cat{C}`$ 上のモナドの圏を $`\mrm{Mnd}(\cat{C})`$ とします。

$`\quad \mrm{Mnd}(\cat{C}) := \mrm{Monoid}( ([\cat{C}, \cat{C}], *, \mrm{Id}_{\cat{C}}) )`$

つまり、モナドの圏は、自己関手圏を“結合をモノイド積とするモノイド圏”と考えて、そのなかのモノイド対象の圏です。$`\mrm{Mnd}(\cat{C})`$ の射は、モノイド構造を保つ自然変換です。この圏は、色々な“モナドの圏”のなかで一番単純なものです。

再開モナドの中身は一旦棚上げにして、モナド $`M\in |\mrm{Mnd}(\cat{C})|`$ と自己関手 $`F\in |[\cat{C}, \cat{C}]|`$ に対する再開モナドを $`\mrm{Resump}(M, F)`$ としましょう。つまり：

$`\For M\in |\mrm{Mnd}(\cat{C})|\\
\For F\in |[\cat{C}, \cat{C}]|\\
\quad \mrm{Resump}(M, F) \in |\mrm{Mnd}(\cat{C})|
`$

これは、対象に対象を対応させているだけなので、型構成子（次元0の圏論的コンストラクタ）であり、次のように書けます。

$`\quad \mrm{Resump} : |\mrm{Mnd}(\cat{C})| \times |[\cat{C}, \cat{C}]| \to |\mrm{Mnd}(\cat{C})| \In {\bf SET}`$

$`\mrm{Resump}`$ を $`{\bf SET}`$ 内で左カリー化したものを $`\mrm{ResumpT}`$ と名付けると、次のようになります。

$`\quad \mrm{ResumpT} = {^\cap \mrm{Resump} } : |[\cat{C}, \cat{C}]| \to [|\mrm{Mnd}(\cat{C})| , |\mrm{Mnd}(\cat{C})| ] \In {\bf SET}`$

$`\mrm{ResumpT}`$ に自己関手を渡すと、モナドからモナドを作るようなコンストラクタが出てきます。

$`\For F \in |[\cat{C},\cat{C}]|\\
\quad \mrm{ResumpT}(F) : |\mrm{Mnd}(\cat{C})| \to |\mrm{Mnd}(\cat{C})| \In {\bf SET}
`$

Haskell風記述では、自己関手もモナドも型構成子（次元0の圏論的コンストラクタ）であり、「フリーモナド 1：自由で無料な木 // 忘却と増強」で述べた忘却・増強のメカニズムを前提して、「自己関手に増強可能な型構成子」「モナドに増強可能な型構成子」という扱いになります。増強は、言語処理系または人間によって行われます。

増強は後回しにして、$`\mrm{ResumpT}`$ の型構成子の部分だけを取り出してそれを $`\mrm{FreeT}`$ と名付けると：

$`\For F \in [|\cat{C}|,|\cat{C}|]_0\\
\quad \mrm{FreeT}(F) : [|\cat{C}|,|\cat{C}|]_0 \to [|\cat{C}|,|\cat{C}|]_0 \In {\bf SET}
`$

ブラケットに付いた下付きの 0 は、関手圏ではなくて関数集合であることを強調しています。$`\mrm{FreeT}`$ に引数を順次渡していったときの“型”を追跡してみます。

$`\quad \mrm{FreeT} : [|\cat{C}|,|\cat{C}|]_0 \to \big[ [|\cat{C}|,|\cat{C}|]_0,\; [|\cat{C}|,|\cat{C}|]_0 \big]_0\In {\bf SET}\\
\For F \in [|\cat{C}|,|\cat{C}|]_0\\
\quad \mrm{FreeT}(F) \in \big[|\cat{C}|,|\cat{C}|]_0,\; [|\cat{C}|,|\cat{C}|]_0 \big]_0\\
\text{i.e.}\\
\quad \mrm{FreeT}(F) : [|\cat{C}|,|\cat{C}|]_0 \to [|\cat{C}|,|\cat{C}|]_0 \In {\bf SET}\\
\For M \in [|\cat{C}|,|\cat{C}|]_0\\
\quad \mrm{FreeT}(F)(M) \in [|\cat{C}|,|\cat{C}|]_0\\
\text{i.e.}\\
\quad \mrm{FreeT}(F)(M) : |\cat{C}| \to |\cat{C}| \In {\bf SET}\\
\For A \in |\cat{C}|\\
\quad \mrm{FreeT}(F)(M)(A) \in |\cat{C}|
%`$

$`\mrm{FreeT}(F)(M)(A)`$ に対するHaskell風の定義が以下です（後で再度触れます）。

newtype FreeT f m a = 
  FreeT {
    runFreeT :: m (FreeF f a (FreeT f m a)) 
  }

フリー・モナド変換子と再開モナド構成子

Haskell風の定義で明示的に書かれる部分は、意図している構造の一部です。明示的な記述から増強に増強を重ねて、意図している構造に到達できます。

FreeT が意図している構造はフリー・モナド変換子です。フリー・モナド変換子は、自己関手からモナド変換子を作る関手的構成手続き〈functorial construction procedure〉なので、モナド変換子の圏を $`\mrm{MndTrans}(\cat{C})`$ として以下のようなプロファイルを持ちます。

$`\quad \mrm{IntendedFreeT} : [\cat{C}, \cat{C}] \to \mrm{MndTrans}(\cat{C}) \In {\bf CAT}`$

明示的に定義される $`\mrm{FreeT}`$ は、忘却関手／忘却写像で $`\mrm{IntendedFreeT}`$ の諸々の構造・性質が削り落とされた影（残骸？）のようなものです。忘却関手／忘却写像を一律に $`U`$ と書くことにして次のような可換図式があります。

$`\require{AMScd}
\begin{CD}
[\cat{C}, \cat{C}] @>{\mrm{IntendedFreeT}}>> \mrm{MndTrans}(\cat{C}) \\
@V{U}VV @VV{U}V \\
[|\cat{C}|, |\cat{C}|]_0 @. \mrm{MndCtor}(\cat{C}) \\
@| @| \\
[|\cat{C}|, |\cat{C}|]_0 @. [|\mrm{Mnd}(\cat{C})|, |\mrm{Mnd}(\cat{C})| ]_0 \\
@| @VV{U}V \\
[|\cat{C}|, |\cat{C}|]_0 @. \big[ |\mrm{Mnd}(\cat{C})|,\;[\cat{C}, \cat{C}] \big]_0 \\
@| @VV{U}V \\
[|\cat{C}|, |\cat{C}|]_0 @. \big[ [\cat{C},\cat{C}],\;[\cat{C}, \cat{C}] \big]_0 \\
@| @VV{U}V \\
[|\cat{C}|, |\cat{C}|]_0 @>{\mrm{FreeT}}>> \big[ [|\cat{C}|, |\cat{C}|]_0,\; [|\cat{C}|, |\cat{C}|]_0 \big]_0
\end{CD}\\
\:\\
\text{commutative in }\widehat{\bf CAT}
`$

ここで、$`\widehat{\bf CAT}`$ は、「コンストラクタ系と変換手性」で出てきた何でもかんでも入っているごった煮な世界です。忘却・増強は、$`\widehat{\bf CAT}`$ のなかでないとうまく記述できません。

上記の忘却・増強構造をたどって、増強のハシゴを何段階も昇るのは面倒なので、再開モナド構成子〈resumption monad constructor〉を次の形の構成手続きだとして*3、それを眺めてみましょう。

$`\quad \mrm{ResumpT'} : |[\cat{C}, \cat{C}]| \to \big[ |\mrm{Mnd}(\cat{C})|,\, [\cat{C},\cat{C}] \big]_0 \In \widehat{\bf CAT}
%`$

$`\mrm{ResumpT'}`$ は、$`\mrm{IntendedFreeT}`$ から何段回か忘却されたコンストラクタです。ポイントとなる表式は次です。

$`\For F \in |[\cat{C}, \cat{C}]|\\
\For M = (\u{M}, \mu, \eta) \in |\mrm{Mnd}(\cat{C})|\\
\quad \mrm{ini}\,y.\u{M}(A + F(y))
`$

ここで、$`\mrm{ini}\,y.G(y)`$ は自己関手から決まる（それがあれば）始代数の台対象です。もう少し丁寧に書くと、まず、自己関手の始代数を次だとします。

$`\quad \mrm{iniAlg}\,y\in_* \cat{C}.G(y) \\
= \mrm{iniAlg}\big( \lambda\, y\in_* \cat{C}.G(y) \big)\\
= \mrm{iniAlg}(G)\;\in |\mrm{LamAlg}(G / \cat{C})|
%`$

ここで、$`\mrm{LamAlg}(G / \cat{C})`$ は、圏 $`\cat{C}`$ 上の自己関手 $`G`$ のランベック代数〈無法則代数〉の圏です。始代数の台対象は $`\mrm{ini}`$ で取り出すことにします。

$`\quad \mrm{ini}\,y\in_* \cat{C}.G(y) \\
= \mrm{ini}\big( \lambda\, y\in_* \cat{C}.G(y) \big) \\
= \mrm{ini}(G) \;\in |\cat{C}|
%`$

$`\lambda y.(A + F(y)) = \mrm{Aff}(F, A)`$ であることに注意してください。ですが、$`\mrm{Aff}`$ は使わないで、次のように書いたほうがむしろ分かりやすでしょう。

$`\quad \mrm{ini}\,y.\u{M}(A + F(y)) \;\in |\cat{C}|`$

ここで、$`A`$ を動かすと次のような関数ができます。

$`\quad \lambda\, A\in |\cat{C}|.(\, \mrm{ini}\,y.\u{M}(A + F(y)) \;\in |\cat{C}|\,)
\;: |\cat{C}| \to |\cat{C}| \In {\bf SET}`$

対象だけではなくて、射も動く変数 $`x`$ （と次元ワイルドカード）を使うと*4、次のように書けます。

$`\quad \lambda\, x \in_* \cat{C}.(\, \mrm{ini}\,y.\u{M}(x + F(y)) \;\in_* \cat{C}\,)
\;: \cat{C} \to \cat{C} \In {\bf CAT}`$

つまり（ラムダ式を短めに書いて）、

$`\quad \lambda\, x .\, \mrm{ini}\,y.\u{M}(x + F(y)) \in [\cat{C}, \cat{C}]`$

いままで自己関手 $`F`$ とモナド $`M`$ は固定してきましたが、これも動かすと次のようになります。

$`|[\cat{C}, \cat{C}]| \ni F \mapsto \big(\\
\quad |\mrm{Mnd}(\cat{C})| \ni M \mapsto \big(\\
\qquad \lambda\, x .\, \mrm{ini}\,y.\u{M}(x + F(y)) \in [\cat{C}, \cat{C}]\\
\quad \big)\\
\big)
%`$

これが、$`\mrm{ResumpT'}`$ の表示になります。清書すれば：

$`\quad \mrm{ResumpT'} : |[\cat{C}, \cat{C}]|
\to \big[ |\mrm{Mnd}(\cat{C})|,\; [\cat{C}, \cat{C}] \big] \In {\bf SET}\\
\For F \in |[\cat{C}, \cat{C}]|\\
\For M \in |\mrm{Mnd}(\cat{C})|\\
\quad \mrm{ResumpT'}(F)(M) := \lambda\, x \in_* \cat{C}.(\, \mrm{ini}\,y\in_* \cat{C}.\u{M}(x + F(y)) \;\in [\cat{C}, \cat{C}]\,)
`$

この再開モナド構成子 $`\mrm{ResumpT'}`$ を何段階か増強すると、ホントのフリー・モナド変換子である $`\mrm{IntendedFreeT}`$ が得られます。

不動点方程式とFreeT

前節の $`\mrm{ResumpT'}`$ の表示の中核的な部分は次の式です。

$`\quad \lambda\, x \in_* \cat{C}.(\, \mrm{ini}\,y\in_* \cat{C}.\u{M}(x + F(y)) \;\in [\cat{C}, \cat{C}]\,)`$

これは不動点方程式の記述で、対象に注目すれば、$`X\in |\cat{C}|`$ ごとに次の不動点方程式を解くことになります。

$`\quad Y \cong \u{M}(X + F(Y)) \In \cat{C}`$

$`\mrm{Aff}`$ を使えば：

$`\quad Y \cong \u{M}( \mrm{Aff}(F, X)(Y) ) \In \cat{C}`$

名前を揃えるために、$`X`$ を $`A`$ に置き換えます。$`A`$ をパラメータとする不動点方程式は：

$`\quad Y \cong \u{M}( \mrm{Aff}(F, A)(Y) ) \In \cat{C}\\
\Where\\
\quad Y = \mrm{ResumpT'}(F)(M)(A)
`$

この不動点方程式に対応する帰納的データ型定義をHaskell風に書けば：

data ResumpT' f m a = m (Aff f a (ResumpT' f m a))

概念的にはこれでいいのですが、Haskellの言語仕様と言語処理系の都合から、次の形になります。

newtype ResumpT' f m a = 
  ResumpT' {
    runResumpT' :: m (Aff f a (ResumpT' f m a)) 
  }

これをリネームして、実際の FreeT の定義は次のとおり。

newtype FreeT f m a = 
  FreeT {
    runFreeT :: m (FreeF f a (FreeT f m a)) 
  }

*1:「自由モナド変換子」としなかったのは、区切りのナカグロを入れたかったからです。「自由・モナド変換子」は表記として不自然な気がします。もっとも、「フリー・モナド変換子」としても、「フリーモナドを変換するもの」と解釈されるかも知れませんが。意味は、自己関手からモナド変換子を自由生成するメカニズムです。

*2:発音： https://www.youtube.com/watch?v=BX3aT0_s4xA

*3:忘却・増強のハシゴの中間段階を選んだのですが、中途半端な所を選んでしまったな、とは思っています。

*4:変数名を変える必要はないのですが、$`A`$ のままだと対象のような“感じ”がするので。