Functor型クラスの型インスタンスは関手なのか？ - 檜山正幸のキマイラ飼育記 (はてなBlog)

ひとつ前の記事「フリーモナド 1：自由で無料な木」において次のように書きました（ブラケット内は要約です）。

[圏論的に考えた場合と、型クラスで考えた場合とでは] メンタルモデルがだいぶ違います。この食い違いがコミュニケーションの障害になることがあります。

同じ言葉を使っていても指しているモノが違うらしく話が噛み合わない感じは、長年、色々な場面で経験してきました。今は、どこが食い違っているのか？なんとなくは分かるようになりました。

ここでは、「関数」と「関手」という2つの言葉に関して、ありがちな食い違いを説明します。なお、地の文内の「関数」は集合のあいだの写像と同義です。$`\newcommand{\mrm}[1]{\mathrm{#1}}
\newcommand{\cat}[1]{\mathcal{#1}}
\newcommand{\In}{\text{ in } }
\newcommand{\Iff}{\Leftrightarrow }
\require{color}
\newcommand{\Keyword}[1]{ \textcolor{green}{\text{#1}} }%
\newcommand{\For}{\Keyword{For } }%
%`$

内容：

関数は値
デカルト閉圏における型、関数、値
自己関手と対象パート
自己関手と型構成子
すべての自己関手
型構成子から自己関手への増強
関手とは何か？
おわりに

関数は値

スタックを表す指標を書いてみます（指標については「指標と不完全インスタンス」参照）。

signature Stack {
  sort Stk
  sort Elm
  operation create : 1 → Stk
  operation push : Stk × Elm → Stk
  operation pop : Stk → Stk
  operation top : Stk → Elm
}

指標の解釈は集合圏で行うことにします。1 は単元集合 $`{\bf 1}`$ のことです。スタックがスタックとして振る舞うことを要求する法則は書いていません。スタックが空の状況も無視しています。まーいいとしましょう。

指標に使うキーワードは好みの問題なので、sort → type, operation → function とリネームしてみます。

signature Stack {
  type Stk
  type Elm
  function create : 1 → Stk
  function push : Stk × Elm → Stk
  function pop : Stk → Stk
  function top : Stk → Elm
}

StandardMLを使うと、上記の疑似コードを実際のコードにほとんどそのまま書き写せます（StanndardMLの名付け習慣には反しますが）。

signature Stack =
sig
  type Stk
  type Elm
  val create : unit -> Stk
  val push : Stk * Elm -> Stk
  val pop : Stk -> Stk
  val top : Stk -> Elm
end

キーワードが function じゃなくて val（valueの短縮）です。あれ？と思ったかも知れませんが val は適切です。プログラミング言語内の「関数」は値〈データ〉です。

デカルト閉圏における型、関数、値

プログラミング言語が背景として想定している圏を $`\cat{C}`$ とします。とりあえず、$`\cat{C} = {\bf Set}`$ と思ってもかまいません。が、コンピュータが大きな圏を直接扱えるわけもないので、$`\cat{C}`$ は小さな圏としましょう。$`\cat{C}`$ の対象〈データ領域〉は単なる集合ではなくて順序や位相が入っているかも知れません。ラムダ計算の意味論は欲しいので、$`\cat{C}`$ はデカルト閉圏だとします。

$`\cat{C}`$ はデカルト・モノイド積〈直積〉を持つので、記号の乱用で $`\cat{C} = (\cat{C}, \times, {\bf 1})`$ と書きます*1。$`\cat{C}`$ は閉圏なので、指数演算を持ちます。指数演算は通常 $`[-, -]`$ と書きます。多くのプログラミング言語では、指数演算の演算記号として矢印（-> や =>）を使います。ここでは中庸を取って記号 $`[- \to -]`$ を使うことにします。カンマの代わりに矢印を使いますが、必ずブラケットで囲みます。

$`\cat{C}`$ がデカルト閉圏であることを、記号の乱用で $`\cat{C} = (\cat{C}, \times, {\bf 1}, [- \to -])`$ と書きましょう。例えばカリー同型は次のようになります。

$`\For A, B, C \in |\cat{C}|\\
\quad \cat{C}(A \times B , C) \cong \cat{C}(B, [A \to C])\\
\quad \cat{C}(A \times B , C) \cong \cat{C}(A, [B \to C])
`$

プログラミング言語が背景として想定している圏 $`\cat{C}`$ の対象を型〈type〉、射を関数〈function〉、終対象からの射を値〈value〉と呼びます。

$`A`$ は型 ⇔ $`A \in |\cat{C}|`$
$`f`$ は関数 ⇔ $`f:A \to B \In \cat{C}`$
$`v`$ は値 ⇔ $`v:{\bf 1} \to A \In \cat{C}`$

指数対象 $`[A \to B] \in |\cat{C}|`$ は関数型〈function type〉とも呼びます。関数型〈指数対象〉を余域とする値を関数型値〈value of function type〉または関数データ〈function data〉と呼びます。

$`w`$ は関数型値 ⇔ $`w:{\bf 1} \to [A\to B] \In \cat{C}`$

カリー同型から、関数の集合と関数型値の集合は同型になります。

$`\For A, B \in \cat{C}\\
\quad \cat{C}(A , B) \cong \cat{C}({\bf 1} \times A , B) \cong \cat{C}({\bf 1}, [A \to B])
`$

カリー同型を与えるカリー化／反カリー化は次の演算子で書きます（僕の習慣です）。

$`\quad \cat{C}(A , B) \ni f \mapsto f^\cap \in \cat{C}({\bf 1}, [A \to B])\\
\quad \cat{C}({\bf 1}, [A \to B]) \ni w \mapsto w_\cup \in \cat{C}(A , B)\\
\quad (f^\cap)_\cup = f\\
\quad (w_\cup)^\cap = w
%`$

$`f \longleftrightarrow f^\cap`$ という1：1対応があるので、関数と関数型値は同一視していい場合が多いですが、区別しないと混乱することもあります。例えば、「Haskellの二重コロン「::」とバインド記号「>>=」の説明」では、関数と関数型値を区別して説明しています。

念のために、「関数」の多義性をまとめておくと：

地の文では、集合のあいだの写像を関数と呼んでいる。関数＝写像
デカルト閉圏 $`\cat{C}`$ 内の射を関数と呼ぶことがある。関数＝射
デカルト閉圏 $`\cat{C}`$ 内の関数型値（終対象から指数対象への射）を関数と呼ぶことがある。関数＝関数型値

StanndardMLの指標に出てきた val push : Stk * Elm -> Stk は次の意味だと解釈できます。

$`\quad \text{push} : {\bf 1} \to [\text{Stk} \times \text{Elm} \to \text{Stk}] \In \cat{C}`$

push は確かに値（終対象からの射）です。

ちなみに、圏の対象に要素という概念はないので、$`\text{push}\in [\text{Elm} \to \text{Stk}]`$ とは書けません。所属記号 $`\in`$ が使われているとしたら、たぶん次のような事情でしょう。

$`v : {\bf 1} \to A \In \cat{C}`$ を $`v\in A`$ と書くと記法の約束をしている。
対象 $`A \in |\cat{C}|`$ とホムセット $`{\bf Set}({\bf 1}, A)\in |{\bf Set}|`$ を意図的に同一視している。
$`\cat{C}`$ が集合圏の部分圏、または集合圏への埋め込みを持つ圏である。ポインティング写像と要素を標準的に同一視している。

自己関手と対象パート

圏 $`\cat{C}`$ 上の自己関手が何であるかは説明しません。記法の確認だけしましょう。$`\cat{C}`$ は小さい圏だと仮定して、自己関手は次のように書きます。

$`\quad F:\cat{C} \to \cat{C} \In {\bf Cat}\\
\quad F \in |[\cat{C}\to \cat{C}]_1|,\: [\cat{C}\to \cat{C}]_1 \in |{\bf Cat}|
`$

ここで、$`[\cat{C}\to \cat{C}]_1`$ は“圏の圏”の指数対象です。デカルト閉圏の指数対象と同じ記法にしました。下付きの 1 は、指数対象が1-圏（通常の圏）であることを示す目印です。

圏の対象に絶対値記号を使うと視認性が悪くなるときは、次の書き方も使います。

$`\quad F \in \mrm{Obj}([\cat{C}\to \cat{C}]_1),\: [\cat{C}\to \cat{C}]_1 \in \mrm{Obj}({\bf Cat})
`$

関手 $`F`$ の対象パート〈object part〉を $`F_\mrm{obj}`$ または $`\mrm{Obj}(F)`$ と書きます。これは、“圏の圏”から集合圏への関手になります。

$`\quad \mrm{Obj}: {\bf Cat}|_{\le 0} \to {\bf Set} \In {\bf CAT}`$

ここで、$`{\bf Cat}|_{\le 0}`$ は2-射〈自然変換〉を捨てて、1-圏とみなした“圏の圏”です*2。1-圏のあいだの関手 $`\mrm{Obj}`$ を $`\cat{C}`$ 上の自己関手に制限したものを $`U`$ とすれば：

$`\quad U : {\bf Cat}|_{\le 0}(\cat{C}, \cat{C}) \to {\bf Set}(|\cat{C}|, |\cat{C}|) \In {\bf Set}`$

関手をホムセットに制限したので、 $`U`$ はモノイド準同型写像（単一対象の圏のあいだの関手）です。今回モノイド構造には注目しないので、以下 $`U`$ は単なる写像として扱います。自己ホムセットのモノイド構造も忘れます。

上記の“自己関手の対象パート”をとる操作を忘却写像とみなしましょう。この忘却写像に対する増強 $`E`$ が後で重要になります。（以下で、$`\mrm{def}(-)`$ は部分写像の定義域です。）

$`\quad E : {\bf Set}(|\cat{C}|, |\cat{C}|) \supseteq\!\to {\bf Cat}|_{\le 0}(\cat{C}, \cat{C})\In {\bf Partial}\\
\For t \in \mrm{def}(E) \subseteq {\bf Set}(|\cat{C}|, |\cat{C}|)\\
\quad U(E(t)) = t
`$

自己関手と型構成子

記述を簡略化するために、次の記法を導入します。

$`\quad \mrm{EndFtor}(\cat{C}) := {\bf Cat}|_{\le 0}(\cat{C}, \cat{C}) = | {\bf Cat}(\cat{C}, \cat{C} ) | \;\in |{\bf Set}|\\
\quad \mrm{TyCtor}(\cat{C}) := {\bf Set}(|\cat{C}|, |\cat{C}| ) \;\in |{\bf Set}|
`$

それぞれ、endo-functor, type constructor の集合です。前節の忘却と増強は次のように書けます。

$`\quad U : \mrm{EndFtor}(\cat{C}) \to \mrm{TyCtor}(\cat{C}) \In {\bf Set}\\
\quad E : \mrm{TyCtor}(\cat{C}) \supseteq\!\to \mrm{EndFtor}(\cat{C}) \In {\bf Partial}`$

さて、当然ながら型構成子は自己関手ではありません。型構成子が与えられて、何を付け足せば関手になるか？ -- それを記述するのがHaskell風の型クラスです。

class Functor f where
  fmap :: (a -> b) -> f a -> f b

f は与えられた型構成子です。「f に fmap を付け足してやれば自己関手になる」と書かれています。fmap は総称関数、つまり、型でインデックス付け〈パラメータ付け〉された関数（$`\cat{C}`$ の関数型値）の族です。次のように書けます。

$`\quad \text{fmap}_{a, b} : {\bf 1} \to [[a \to b]\to [f\; a \to f\; b]] \In \cat{C}`$

あるいは：

$`\quad \text{fmap}_{a, b} \in \cat{C}({\bf 1}, [[a \to b]\to [f\; a \to f\; b]])`$

ここで、a, b は型変数なので、型の集合（圏 $`\cat{C}`$ の対象集合 $`|\cat{C}|`$）内で動きます。その旨を、論理の全称記号〈総称記号〉を流用して次のように書くのが習慣です（僕はこの習慣嫌いですけど）。

$`\quad \forall (a, b) \in |\cat{C}|\times|\cat{C}|.\, \text{fmap}_{a, b} : {\bf 1} \to [[a \to b]\to [f\; a \to f\; b]] \In \cat{C}`$

あるいは、

$`\quad \forall (a, b) \in |\cat{C}|\times|\cat{C}|.\, \text{fmap}_{a, b} \in \cat{C}({\bf 1}, [[a \to b]\to [f\; a \to f\; b]] )`$

こう書くと、$`\text{fmap}_{-, -}`$ は、型のペアに対して $`\cat{C}`$ の関数型値〈特殊な射〉を対応させる関数（集合のあいだの写像）であることがわかります。

$`\quad \text{fmap}_{-, -} : |\cat{C}|\times|\cat{C}| \to \mrm{Mor}(\cat{C}) \In {\bf Set}\\
\For (a, b) \in |\cat{C}|\times|\cat{C}|\\
\quad \text{fmap}_{a, b} \in \cat{C}({\bf 1}, [[a \to b]\to [f\; a \to f\; b]] )
`$

依存型のパイ型〈パイ構成〉を使うと、次のように書けます。

$`\quad \text{fmap} \in \prod_{(a, b) \in |\cat{C}|\times|\cat{C}|} \cat{C}({\bf 1}, [[a \to b]\to [f\; a \to f\; b]] )`$

依存型については次の過去記事を参照してください。

関手が満たすべき法則は今は無視することにして、型クラス Functor のインスタンスは次の2つの構成素の組になります。

$`f \in \mrm{TyCtor}(\cat{C}) = {\bf Set}(|\cat{C}|, |\cat{C}|)`$
$`\text{fmap} \in \prod_{(a, b) \in |\cat{C}|\times|\cat{C}|}\cat{C}({\bf 1}, [[a \to b]\to [f\; a \to f\; b]] )`$

2つの構成素を独立に選べるわけではなくて、型構成子 f を選んだ後でないと総称関数 fmap を決められません。fmap は f に依存しています。

すべての自己関手

すべての自己関手の集合は $`\mrm{EndFtor}(\cat{C})`$ と書くことにしました。Haskell型クラス Functor は、$`\mrm{EndFtor}(\cat{C})`$ をエンコードするためのデータ構造を定義しています。そのデータ構造を調べましょう。

前節で出てきた $`\cat{C}({\bf 1}, [[a \to b]\to [f\; a \to f\; b]] )`$ はパラメータ $`f, a, b`$ を含んでいるので、$`\Phi(f, a, b)`$ と書きましょう。$`(f, a, b)`$ を決めれば、集合 $`\Phi(f, a, b)`$ が決まるので、$`\Phi`$ は次のような関数です。

$`\quad \Phi : \mrm{TyCtor}(\cat{C})\times |\cat{C}| \times |\cat{C}| \to |{\bf Set}| \In {\bf SET}`$

型構成子 $`f \in \mrm{TyCtor}(\cat{C})`$ を固定してみると、2つの型のペアに集合を対応させる関数になります。

$`\quad \Phi_f : |\cat{C}| \times |\cat{C}| \to |{\bf Set}| \In {\bf SET}\\
\quad \Phi_f(a, b) := \Phi(f, a, b)
%`$

この関数（2つの型のペアでインデックス付けられた集合の族）からシグマ型を作ります（シグマ構成します）。$`(a, b) \in |\cat{C}| \times |\cat{C}|`$ を動かして、集合をすべて寄せ集めます。

$`\quad \sum_{(a, b)\in |\cat{C}| \times |\cat{C}|} \Phi_f(a, b)`$

これは集合であり（$`\cat{C}`$ の対象ではない）、要素を持ちます。その要素は $`\cat{C}`$ の関数型値です。

固定していた型構成子 f を動かすと、次のような関数が作れます。

$`\quad \mrm{TyCtor}(\cat{C}) \ni f \mapsto \sum_{(a, b)\in |\cat{C}| \times |\cat{C}|} \Phi_f(a, b) \in |{\bf Set}| \In {\bf SET}`$

これは、型構成子でインデックス付けられた集合の族なので、再びシグマ型を作れます。$`f \in \mrm{TyCtor}(\cat{C})`$ を動かして、集合をすべて寄せ集めます。

$`\quad \sum_{f \in \mrm{TyCtor}(\cat{C})}\left( \sum_{(a, b)\in |\cat{C}| \times |\cat{C}|} \Phi(f, a, b) \right)`$

自己関手をエンコードするための空間は上記のような繰り返されたシグマ型です。すべての自己関手は、とある写像〈エンコーディング〉$`\mrm{Enc}`$ により、シグマ型の空間〈集合〉に埋め込まれます。そのとき、次の図式は可換になります。$`\pi`$ はシグマ型の標準的な〈canonical〉射影です。

$`\require{AMScd}
\begin{CD}
\mrm{EndFtor}(\cat{C}) @>{\mrm{Enc} }>>
\sum_{f \in \mrm{TyCtor}(\cat{C})}\left( \sum_{(a, b)\in |\cat{C}| \times |\cat{C}|} \Phi(f, a, b) \right)\\
@V{U}VV @VV{\pi}V\\
\mrm{TyCtor}(\cat{C}) @= \mrm{TyCtor}(\cat{C})
\end{CD}\\
\:\\
\text{commutative in }{\bf Set}
`$

型構成子から自己関手への増強

記述を簡略化するために、次のように定義します。

$`\For f\in \mrm{TyCtor}(\cat{C})\\
\quad \Psi(f) := \sum_{(a, b)\in |\cat{C}| \times |\cat{C}|} \Phi(f, a, b) \\
\qquad\quad = \sum_{(a, b)\in |\cat{C}| \times |\cat{C}|} \cat{C}({\bf 1}, [[a \to b]\to [f\; a \to f\; b]] )
`$

すると、前節の可換図式は次のように書けます。

$`\begin{CD}
\mrm{EndFtor}(\cat{C}) @>{\mrm{Enc} }>>
\sum_{f \in \mrm{TyCtor}(\cat{C})} \Psi(f) \\
@V{U}VV @VV{\pi}V\\
\mrm{TyCtor}(\cat{C}) @= \mrm{TyCtor}(\cat{C})
\end{CD}\\
\:\\
\text{commutative in }{\bf Set}
`$

今、忘却写像 $`U`$ に対する増強 $`E`$ があったとして、その定義域を
$`\quad \mrm{FunctorTyCtor}(\cat{C}) \subseteq \mrm{TyCtor}(\cat{C})`$
とします。次の図式を可換にする $`E'`$ を考えます。

$`\begin{CD}
\mrm{EndFtor}(\cat{C}) @>{\mrm{Enc} }>>
\sum_{f \in \mrm{TyCtor}(\cat{C})} \Psi(f) \\
@A{E}AA @AA{E'}A\\
\mrm{FunctorTyCtor}(\cat{C}) @= \mrm{FunctorTyCtor}(\cat{C})
\end{CD}\\
\:\\
\text{commutative in }{\bf Set}
`$

増強の表現である $`E'`$ は、型クラス Functor のインスタンス定義のことです。むしろ、$`E'`$ が先にあって、そのセマンティクスが $`E`$ と考えるのが実情にあってます。$`E'`$ を $`\mrm{FunctorInstance}`$ という名前で呼ぶと、可換図式は次のようになります。

$`\begin{CD}
\mrm{EndFtor}(\cat{C}) @>{\mrm{Enc} }>>
\sum_{f \in \mrm{TyCtor}(\cat{C})} \Psi(f) \\
@A{E}AA @AA{\mrm{FunctorInstance}}A\\
\mrm{FunctorTyCtor}(\cat{C}) @= \mrm{FunctorTyCtor}(\cat{C})
\end{CD}\\
\:\\
\text{commutative in }{\bf Set}
`$

型構成子に総称関数を対応させる関数 $`\mrm{FunctorInstance}`$ は、部分関数かも知れません（多くの場合、全域ではない部分関数です）。

$`\quad \mrm{def}(\mrm{FunctorInstance}) = \mrm{FunctorTyCtor}(\cat{C}) \subseteq \mrm{TyCtor}(\cat{C})`$

関手とは何か？

前節の最後の可換図式を使うと、冒頭で述べた「メンタルモデルの食い違い」を説明できます。

圏 $`\cat{C}`$ の自己関手を「関手」と呼ぶ前提で、「関手とは何か？」と問われれば、関手とはもちろん $`\mrm{EndFtor}(\cat{C})`$ の要素です。

$`\quad \mrm{IsFunctor}(x) :\Iff x \in \mrm{EndFtor}(\cat{C})
%`$

関手のエンコードである総称関数の側で考えるならば、関手と呼ぶべき総称関数は写像 $`\mrm{Enc}`$ の像に入る総称関数のことです。

$`\quad \mrm{IsFunctor'}(x) :\Iff x \in \mrm{Img}(\mrm{Enc})
%`$

もう少し詳しく書けば：

$`\quad \mrm{IsFunctor'}(x) :\Iff \\
\qquad x \in \sum_{f \in \mrm{TyCtor}(\cat{C})} \Psi(f) \\
\qquad \land \\
\qquad \exists F \in \mrm{EndFtor}(\cat{C}). \mrm{Enc}(F) = x
%`$

しかし、インスタンス定義 $`\mrm{FunctorInstance}`$ のほうに目が向いていると、次のように考えることがあるようです。

$`\quad \mrm{IsFunctor''}(x) :\Iff x \in \mrm{Img}(\mrm{FunctorInstance})
%`$

あるいは：

$`\quad \mrm{IsFunctor''}(x) :\Iff \\
\qquad x \in \sum_{f \in \mrm{TyCtor}(\cat{C})} \Psi(f)\\
\qquad \land \\
\qquad \exists f \in \mrm{FunctorTyCtor}(\cat{C}).\, \mrm{FunctorInstance}(f) = x
%`$

もっと極端になると、次が「関手とは何か？」の答になります。

$`\quad \mrm{IsFunctor'''}(x) :\Iff x \in \mrm{FunctorTyCtor}(\cat{C})
%`$

この発想だと、「関手とは型構成子の特別なモノ」となります。なぜなら：

$`\quad \{x \mid \mrm{IsFunctor'''}(x)\} = \mrm{FunctorTyCtor}(\cat{C}) \subseteq \mrm{TyCtor}(\cat{C})
%`$

「エンコーディング写像 $`\mrm{Enc}`$ の像」という理解はときに役立ったりしますが、インスタンス定義 $`\mrm{FunctorInstance}`$ を介入させると、“関手という概念”とは食い違ってきます。$`\mrm{FunctorInstance}`$ は忘却に対する増強の表現です。個別の $`f\in \mrm{FunctorTyCtor}(\cat{C})`$ に対する $`\mrm{FunctorInstance}(f)`$ はひとつの自己関手（の表現）ですが、“すべての自己関手”の集合、あるいは“自己関手”という概念を表現しているわけではありません。

おわりに

関数や関手のような概念と、それを表現するために手段が混同され混乱することがあります。

集合圏に限らず、計算のモデルとなる圏の射を「関数」と呼ぶのは別に悪くないでしょう。その意味での関数〈射〉が、特別な形の射である関数型値で表現されます。

自己関手は、型構成子と総称関数の組で表現されます。自己関手の表現である型構成子・総称関数ペア（依存ペア）を「関手」と呼ぶのも悪くはない気がします。が、“関手から対象パートへの忘却”に対する増強を「関手」と呼ぶのは行き過ぎだと思います。

いずれにしても、概念とそれを表現するための手段は区別しておくのが無難（災難を避けられる）です。

*1:結合律子 α 、左単位律子 λ 、右単位律子 ρ などの詳細情報は省略します。

*2:自然変換を議論の対象にする気はないので、前もって自然変換は捨てておきます。