蒸し返し：アドホック多相 vs パラメトリック多相 - 檜山正幸のキマイラ飼育記 (はてなBlog)

一年ほど前に「「アドホック多相 vs パラメトリック多相」をマジメに考えてはいけない」という記事を書きました。多相性を二種類に分類できるわけではなくて、パラメトリック性（あるいはアドホック性）はしょせん程度問題だ、という話です。「関数定義がひとつで済む多相はパラメトリック多相」なんていう曖昧な定義はあまり意味がありません。

しょせん程度問題だとすると、その“程度”を測って比較したいとは思います。「「アドホック多相 vs パラメトリック多相」をマジメに考えてはいけない // それでもマジメに考えたいのなら」に次のように書きました。

多相関数を自然変換として定式化して、自然変換のあいだの関係をアドホック性を計る尺度に用います。実際、いくつかの方法で自然変換のあいだの順序を定義できます。その順序は、アドホック性の程度とみなせます。

上記の方法でパラメトリック性（アドホック性）を実際に測って比較してみます。

内容：

例題はlength関数
自然変換としてのlength関数
Haskell風 vs 圏論風
3人のプログラマにlengthを作ってもらう
部分圏と自然性
部分圏に相対的なパラメトリック性

続きの記事：

例題はlength関数

例題として、リストの長さを求める関数lengthを考えます。多相関数としてのlengthを、型理論では割と標準的（でHaskell風の）書き方で導入します。

lengthの入出力の仕様〈プロファイル〉は次のように宣言されます。

$length :: \forall\alpha. \mathrm{List}\, \alpha \to Int$

コロン2個はHaskellの構文で、普通の（多数派の）記法ならコロン1個です。また、型理論の習慣として、型を表す変数はギリシャ小文字にします。なので、αは型変数〈型パラメータ〉です。関数が、単一の型ではなくて色々な型に適用可能であることを記号'∀'を使って表します。'∀'は、もともとは記号論理の全称限量子〈universal quantifier〉の記号です。僕は、ここに'∀'を使うのは好きではありません、だって論理の'∀'とあんまり似てないもんね。まー、意味ではなくて単に記号だけテキトーに借用していると解釈しましょう。「∀α. ‥‥」は、「色々な型αに関して ‥‥」と読みます。

$\mathrm{List}\, \alpha$ は、型αの項目〈成分 | 要素〉からなるリストの型です。型構成子〈type constructor〉であるListはローマン体で書きます（そういう習慣もある、というだけ）。Intは整数型です（具体的な型名はラテン大文字始まりの名前、という約束）。よって、上の記号的表現は次のように読めます。

length は、色々な型αに関して、型αの項目からなるリストの型から整数型への関数である。

特定の型ξに対するlengthのインスタンス（型パラメータの具体化）は length_ξ のように書きます。下付きが書けないときは、length<ξ>, length[ξ] などとします。

多相関数lengthがパラメトリックであること〈parametricity property〉は次の等式で表現します。

$length_\beta \,(map\, f\, x) = length_\alpha\, x \:\:\:\:\mbox{for }f :: \alpha \to \beta$

ここで、map（fmapと書かれることも多い）は、List型構成子にともなうマップ化高階関数で、任意の関数 f::α → β（普通の書き方なら f:α → β）を引数として新しい関数 map f = map(f) : List α → List β を返します。

上の等式は、マップ化高階関数でマップ化した関数を適用した後でもリストの長さは変わらないことを主張しています。

自然変換としてのlength関数

List型構成子の引数となる型は集合と解釈しましょう。よく使う型は：

型	対応する集合
Bool	{True, False}
Int	Z
Real*1	R
Char	Ch = (Unicodeのすべての文字からなる集合)

集合圏をSetとすると、List型構成子は List:|Set| → |Set| とみなせます。List(f) := map(f) とすれば、ListはSet上の自己関手になります。

List:Set → Set は関手。

別な関手K_Zを次のように定義します。

For X∈|Set|, K_Z(X) := Z
For X, Y∈|Set|, f:X → Y in Set, K_Z(f) := id_Z

多相関数lengthは、関手Listから関手K_Zへの自然変換として定義します。

length::List ⇒ K_Z:Set → Set

ここでのコロン2個は、Haskellの構文とは関係ありません。自然変換は、“圏の圏”の2-射なのでコロンを2個（矢印も二重）にしています。まったく違った習慣からのコロン2個です。lengthが自然変換であるためには、次の可換図式が要求されます。

$\require{AMScd} \forall f:X \to Y \:\mbox{ in }{\bf Set} \\ \:\\ \begin{CD} \mathrm{List}(X) @>{length_X}>> \mathrm{K}_{\bf Z}(X) \\ @V{\mathrm{List}(f)}VV @VV{\mathrm{K}_{\bf Z}(f)}V \\ \mathrm{List}(Y) @>{length_Y}>> \mathrm{K}_{\bf Z}(Y) \\ \end{CD} \\ \:\\ \mbox{commutative in }{\bf Set}$

関手K_Zの定義から簡略化できて：

$\forall f:X \to Y \:\mbox{ in }{\bf Set} \\ \:\\ \begin{CD} \mathrm{List}(X) @>{length_X}>> {\bf Z} \\ @V{\mathrm{List}(f)}VV @| \\ \mathrm{List}(Y) @>{length_Y}>> {\bf Z} \\ \end{CD} \\ \:\\ \mbox{commutative in }{\bf Set}$

この可換図式を等式で書けば：

$\forall( f:X \to Y \:\mbox{ in }{\bf Set}).(length_Y \circ \mathrm{List}(f) = length_X )$

これは、書き方が多少違うだけで、パラメトリック性を表す等式（下に再掲）と同じです。

$length_\beta \,(map\, f\, x) = length_\alpha\, x \:\:\:\:\mbox{for }f :: \alpha \to \beta$

つまり：

多相関数とは自然変換のことである。
パラメトリック性とは自然性〈naturality〉のことである。

これで、多相関数とそのパラメトリック性を圏論の枠組みで議論する準備ができました。

Haskell風 vs 圏論風

二種類の書き方が混じっていたので、おおよその翻訳を示しておきます。

Haskell風	圏論風
$\alpha, \beta, \cdots$	A, B, ..., X, Y
$Int$	Z
$Float, Double$	R
$f:: \alpha \to \beta$	f:X → Y または f:1 → [X, Y]
$f:: \alpha \to \beta \to \gamma$	f:X → [Y, Z] または f:1 → [X, [Y, Z]]
$f \,x$	f(x) または x;f または ev(f, x)
$\mathrm{List}\,\alpha$	List(X) （Xは対象）
$map\, f$	List(f) （fは射）
$f::\forall\alpha. \mathrm{List}\,\alpha \to \beta$	ψ::List ⇒ K_Y （自然変換）
$f_\xi :: \mathrm{List}\,\xi \to \beta$	ψ_A:List(A) → Y （自然変換の成分）

前節でも注意したように圏論風のコロン2個は自然変換だからです。正確には、ψ::List ⇒ K_Y:Set → Set （集合圏の自己関手のあいだの自然変換）です。プログラミング言語だと関手（型構成子とマップ化関数）の域・余域を記述できる機能はあまり見かけないです*2。

実数に Float, Double があるのはコンピュータ特有の事情なので、Rに対応する型は（実際とは違い） Real とすることにします（前節でRealを既に使っている）。以下では、主に圏論風記法を使うことにします。が、プログラミング的文脈では、テキトーな疑似コードを使います。

3人のプログラマにlengthを作ってもらう

3人のプログラマ、A君、B君、C君がいます。上司のXさんが次の指示を出しました。

A君に： length : List<Int> -> Int という関数を書け。
B君に： length : List<Char> -> Int という関数を書け。（List<Char> は文字列型）
C君に： length : List<Real> -> Int という関数を書け。

A君とB君は、リストの項目〈要素 | 成分〉の個数を勘定する関数を書きました。C君は次の定義に基づきlength関数を書いたとします。

$\mathrm{round}\left(\sqrt{ {x_1}^2 + {x_2}^2 + \cdots + {x_n}^2}\right)$

つまり、List<Real>（List(R)）の要素をn次元ユークリッド空間のベクトルだと解釈し、その長さ（ユークリッド・ノルム）を求めたのです。ユークリッド・ノルムそのままだと実数なので四捨五入して整数にしています。

A君、B君、C君が作ったlength関数を、一旦それぞれ別な名前にして、Xさんが1つの関数にまとめたとしましょう。

function length<Int> = lengthByA
function length<Char> = lengthByB
function length<Real> = lengthByC

型引数の具体化は、呼び出し時に明示的に指定（length<Char>("hello") のように）してもいいし、コンパイラが型推論して補ってくれると考えてもいいです。あるいは、実行時の型場合分け〈type case〉が使えるとして：

function length = lambda(x) {
  typecase (x) {
     List<Int> => lengthByA(x)
     List<Char> => lengthByB(x)
     List<Real> => lengthByC(x)
  }
}

いずれにしても、項目の型が Int, Char, Real であるリストに適用可能な多相関数lengthができました。この多相関数は、その作り方からいってアドホックです。型ごとの担当者は、関数名の印象だけから勝手に実装しています。A君とB君が共通の仕様の関数を実装したのは偶然です*3。

今定義したlengthは、パラメトリック性 -- つまり自然性を持つでしょうか？

部分圏と自然性

多相関数lengthの自然性の条件を下に再掲します。

$\forall f:X \to Y \:\mbox{ in }\mathcal{C} \\ \:\\ \begin{CD} \mathrm{List}(X) @>{length_X}>> K_{\bf Z}(X) \\ @V{\mathrm{List}(f)}VV @VV{K_{\bf Z}(f)}V \\ \mathrm{List}(Y) @>{length_Y}>> K_{\bf Z}(Y) \\ \end{CD} \\ \:\\ \mbox{commutative in }{\bf Set}$

最初に出した条件と一箇所だけ違いがあって、最初の行の「圏Set」が「圏C」に変わっています。考えるべき関手 List, K_Z が、Set → Set ではなくて、C → Set でもいいとしています。ただし、CはSetの部分圏であり、もとの List, K_Z を部分圏に制限して考えます。

Setの部分圏S1を次のように定義します。Chは型Charに対応する集合でした。

|S1| := {Z, Ch, R}
For X, Y∈|S1|, S1(X, Y) := Set(X, Y)
射の結合と恒等射はSetと同じ。

S1は3つの対象を持つSetの部分圏です（充満部分圏と呼ばれます）。すぐ上の自然性の条件において、C = S1 と置いたとき、自然性は成立するでしょうか？ダメですね。例えば、f:Z → R として単純・常識的な埋め込み写像をとるとき length<Int>( (3, 3) ) と length<Real>( (3, 3) ) は一致しません。

「あー、やっぱりアドホックだな」と思うでしょう。しかし、部分圏S2を次のように定義することもできます。

|S2| := {Z, Ch, R}
For X, Y∈|S2|,
S2(X, X) := {id_X}
X ≠ Y ならば S2(X, X) := {}
射の結合と恒等射はSetと同じ。

S2も3つの対象を持つSetの部分圏です（離散部分圏と呼ばれます）。C = S2 と置いたとき、自然性は成立します。 $\forall f:X \to Y \:\mbox{ in } {\bf S2}$ において選べるfが、id_Z, id_Ch, id_R しかなく、図式が可換となるのは自明です。

S1とS2の中間の圏として、部分圏S3を定義してみます。

|S3| := {Z, Ch, R}
ホムセット
- X, Y∈{Z, Ch} ならば、S3(X, Y) = Set(X, Y)
- S3(R, R) = {id_R}
- その他の S3(X, Y) = {}
射の結合と恒等射はSetと同じ。

S2 でもlengthの自然性は成立します。

多相関数を構成する関手と写像の族に対して、定義域となる圏の取り方を変えると、自然性（＝パラメトリック性）は成立したりしなかったりします。

部分圏に相対的なパラメトリック性

次の状況を考えましょう。

F, G:Set → Set は関手。
Kは集合の集合。同じことだが K⊆|Set| 。
ψ:K → Mor(Set) つまり、ψは、Kの要素（それは集合）でインデックスされた関数の族。
dom(ψ_X) = F(X), cod(ψ_X) = G(X) 。
C, D などはSetの部分圏で、|C| = |D| = K 。

前節の話はこの状況になっています。

List, K_Z は関手。
{Z, Ch, R} は集合の集合。
length:{Z, Ch, R} → Mor(Set) は、{Z, Ch, R} の要素でインデックスされた関数の族。
dom(length_X) = List(X), cod(length_X) = K_Z(X) 。
S1, S2, S3 はSetの部分圏で、|S1| = |S2| = |S3| = {Z, Ch, R} 。

一般的に、ψが自然性を持つか（自然変換になっているか）は、部分圏Cの選び方によります。ある部分圏Cに対してψが自然性を持つとき次のように書きましょう。

ψ is-natural-on C

「「アドホック多相 vs パラメトリック多相」をマジメに考えてはいけない」の脚注として次のように書きました。

アドホック多相関数は自然変換にならない、と思っている人がいるかも知れません。そんなことはありません。アドホック多相関数（と呼ばれているもの）でも自然変換に仕立てることができます。

部分圏Cを離散圏に取れば、離散圏Cに対して、ψ is-natural-on C は必ず成立します。どんなにアドホックな多相関数でも、離散圏に対してはパラメトリック〈自然〉なのです。しょせん程度問題です。

今述べたセッティングでは、パラメトリックな程度（アドホックな程度）は、ψ is-natural-on C となる部分圏Cの“大きさ”で測れます。それは、そういう基準で計ると約束したからです。パラメトリック性（アドホック性）を別な基準で計ることもあるでしょう。圏論を使わない基準もあるかも知れません。ですが、基準をハッキリと決めないで「アドホック vs パラメトリック」と言っても、それは無意味です。

*1:Realについは次の節に書いてあります。

*2:自然変換の生息地〈habitat | アビタ〉は、圏の圏CATです。自然変換の記述をさらに正確にすると、ψ::List ⇒ K_Y:Set → Set in CAT。プログラミング言語のデータ型の世界をCATまで広げるのは大変ではあります。

*3:「「アドホック多相 vs パラメトリック多相」をマジメに考えてはいけない」では、「たまたま"square"という同じ名前で呼ばれる3つの関数」「たまたま"increase"という同じ名前で呼ばれる2つの関数」の例を出しています。