zipと言っても、圧縮＆アーカイブのツールではありません。リスト処理の話です。ファスナーをしめる操作を連想させるのでzipと呼ぶのでしょう。今ここでは、「あのzipです」という以上の説明はしません。あのzipを型付けすると、自然変換だと解釈できます。二項関手のあいだの自然変換なので、モナド（の台関手）などとは違った雰囲気のものです。
集合圏の小さい部分圏Cを固定して、ここを舞台に考えます。C内で直積や直和は自由に作れるとします。もうひとつの圏Dがあるとして、F:D→C が関手のとき、Fの対象部分（object part）をF0、射部分（morphism part）をF1とします。さらに、射部分は対象の対ごとに分割して F1A,B:D(A, B)→C(F0(A), F0(B)) のようにも書きます。関手Fは、写像F0:|D|→|C| と (A, B)∈(|D|×|D|) で添字付けられた写像の族 F1A,B:D(A, B)→C(F0(A), F0(B)) として記述できます。
L:C→C はリスト関手とします。A∈|C| （Aは集合）に対して、L0(A) はAの要素を項目とするリストの全体です。f:A→B に対する L1A,B(f):L0(A)→L0(B) はリストのmap高階関数のことです。L(f) = L1A,B(f) は、リストの各項目にfを適用したリストを作ります。
P:C×C→C は、ペアリング関手とします。Pは二項関手（双関手）となります。二項関手の定義域は圏Cの（直積の意味での）二乗です。C×C をDと置くと、Dの対象は (A, B)∈|C|×|C| という対で、D((A, B), (C, D)) に入る射は f:A→C in C と g:B→D in C の対 (f, g) です。ペアリング関手Pを詳しく書くと：
- P0:|C|×|C|→|C|, P0(A, B) = A×B
- P1(A,B),(C,D):(C×C)((A, B), (C, D)) = C(A, C)×C(B, D) →C(A×B, C×D), P(f, g) = f×g
f×g をより具体的に言えば：
- f×g:A×B→C×D
- (a, b)∈(A×B) に対して、(f×g)(a, b) = (f(a), g(b))。(f(a), g(b))∈(C×D)。
f×g とデカルトペアリング <f, g> は区別してください。<f, g>(a) = (f(a), g(a)) です。
さて、L:C→C と P:C×C→C という2つの関手が定義できました。LとPを組み合わせて、PLLを定義します。
- PLL(A, B) = P(L(A), L(B)) : |C|×|C|→|C|
- PLL(A,B),(C,D)(f, g) = P(L(f), L(g)) : (C×C)((A, B), (C, D))→C(PLL(A, B), PLL(C, D))
上付きの0と1は省略しました。同様に、LPを次のように定義します。
- LP(A, B) = L(P(A, B)) : |C|×|C|→|C|
- LP(A,B),(C,D)(f, g) = L(P(f, g)) : (C×C)((A, B), (C, D))→C(LP(A, B), LP(C, D))
ふー、これで準備ができました。
zipは、関手PLLから関手LPへの自然変換です。つまり、zip::PLL⇒LP:C×C→C と書けます。zipは、|C|×|C| の要素(A, B)で添字付けられた写像の族 zipA,B:PLL(A, B)→LP(A, B) として表現されます。実際のリスト処理のzipがそのような多相関数になっていることを確認してみてください。
zipが自然性を持つとは、次の図式が可換になることです。これも具体的に確認できます。
PLL(A, B) - zip_(A,B) → LP(A, B) ｜ ｜ PLL(f, g) LP(f, g) ↓ ↓ PLL(C, D) - zip_(C,D) → LP(C, D)
