Functional Programming with Bananas, Lenses, Envelopes and Barbed Wire

original paper: https://maartenfokkinga.github.io/utwente/mmf91m.pdf

注意この記事はあまり形式的な圏論で記述されてない. 考えてる圏は Hask 圏かもしくはせいぜい Set 圏である. 射のことを関数と書いてあったり, 対象の「要素」なるものを前提なしに取り上げている.

概要

一般の再帰的データ構造について, ちょうど, リストに対する畳み込み (fold) といったような4種類の操作 (catamorphism, anamorphism, hylomorphism, paramorphism) を統一的に与える.

表記

この論文では独特な括弧が4種類導入されている. できるだけオリジナルの見た目を模倣して, ここでは次のように表記する.

名称	表記	代替表記	備考
バナナ括弧	$(\|_\|)$	`(\| \|)`	果物のバナナ
レンズ括弧	$[(_)]$	`[( )]`	凹レンズ
封筒括弧	$[[_]]$	`[[ ]]`
有刺鉄線	$[⟨_⟩]$	`[< >]`	$[$ と $⟨$ の重ねあわせ

他にこの論文で使われてる表記で次のものをこの文書でも用いる.

$c^{∙}$
- 型 $C$ の値 $c$ (或いは $c \in C$ ) と任意の型 (集合) $A$ について, $A \to C$ なる定数関数のこと
- $\forall a \in A, c^{∙} (a) = c$

またこの論文で使われている表記で, あまり一般的に思えないものについては次の一般的な表記を用いる.

$A \times B$
- 対象 $A, B$ の積
- タプル型, 集合の直積
$A + B$
- 対象 $A, B$ の直和
- 直和型, 集合の直和
$f : A \to B$
- $f$ は $A$ から $B$ への射
- あるいは関数, 演算
$[A]$
- 型 $A$ の要素に持つリストの型

リストの場合

$[A]$ 型の場合を考える.

catamorphism

"cata-" は catastrophic のそれであって, 下方へ, といった意味らしい. リストについての catamorphism は如何のような関数 $h$ である.

$h : [A] \to B$
$h [] = b$
$h (cons (a, a s)) = a \oplus h (a s)$

ここで $b$ は $B$ の定数. $\oplus$ は $A \times B \to B$ なる二項演算子. このような形の $h$ は Haskell のような言語では foldr として知られており

h = foldr (b, \oplus)

のように書ける. すなわち $h$ という関数は $b, \oplus$ によって決定するから, ここでは バナナ括弧 で括ることで

h = (| b, \oplus |)

と書くことにする.

例えばリストの長さを取る関数は $(| 0, (_, n) \mapsto n + 1 |)$ と書けることが分かる. 他に filter もこの形で定義できる.

anamorphism

ちょうど catamorphism の逆のもので, unfold のような名前で知られている関数 $h$ を次のように定義する.

$h : B \to [A]$
$h b = {\begin{cases} [] & when p b \\ cons (a, h b^{'}) & otherwise, where (a, b^{'}) = g b \end{cases}$

ただしここで $p$ は $B \to Bool$ なる述語関数 ( $Bool$ は普通の意味で). $g$ は $B \to A \times B$ なる関数.

やはりこの $h$ は $p, g$ で決まる関数なので, 今度はレンズ括弧で括って

h = [(g, p)]

と書いて表す.

例えば, 関数 $f : A \to A$ を繰り返し適用する iterate f という関数 $A \to [A]$ は $[(a \mapsto (a, f a), {false}^{∙})]$ と書ける.

map 関数

リスト $[A]$ と関数 $f : A \to B$ があるときに, リストの各要素に $f$ を適用することで $[A] \to [B]$ という関数を構成することができる. Haskell では map f とこれを書くが, 論文に倣って $f *$ と書くことにする. これは $[A]$ からの catamorphism として書くこともできるし, $[B]$ への anamorphism と書くこともできる.

$f * = (| [], (a, b) \mapsto cons (f a, f * b) |)$
$f * = [(cons (a, a s) \mapsto (f a, a s), nil)]$
- where
  - $nil [] = true$
  - $nil cons (x, x s) = false$

hylomorphism

リストに関する hylomorphism とは, 例えば木構造をリストにしてやるような「線形再帰関数」のもの. 具体的には

h : A \to C

h a = {\begin{cases} c & when p a \\ b \oplus h a^{'} & otherwise, where (b, a^{'}) = g a \end{cases}

と書き表されるもの. ここで $c : C$ , $g : A \to B \times A$ , $\oplus : B \times C \to C$ であって $h : A \to C$ である.

今度の $h$ は $c, \oplus, g, p$ によって決定されるので

h = [[(c, \oplus), (g, p)]]

と書き表すことにする.

そしてこれは明らかに

[[(c, \oplus), (g, p)]] = (| c, \oplus |) \circ [(g, p)]

という合成の形に分解できる. この証明は論文にはあるが省略. リストが一見登場しないが, この合成の形を見れば, 中間でリストを経由してることが分かる.

例えば自然数の階乗を計算する関数 $N \to N$ は $[[(1, \times), ((1 + n) \mapsto (1 + n, n), zero)]]$ と書ける. ここで $zero$ は引数がゼロかを判定する述語とする. つまり $[(g, zero)] (m) = [m, m - 1, \dots, 1]$ であって $(| 1, \times |)$ はそれを乗算しながら畳み込む関数である.

paramorphism

原始再帰のパターンを提供するのが paramorphism であって, リストに関する paramorphism は次のように定義される.

$h : [A] \to B$
$h [] = b$
$h cons (a, a s) = a \oplus (a s, h a s)$

ここで $b : B$ , $\oplus : A \times ([A] \times B) \to B$ である. このような $h$ はやはり $b, \oplus$ で決定されるので,

h = [⟨ b, \oplus ⟩]

と書くことにする.

$\oplus$ の型が豪華になったので, 値を蓄積しながらのような関数が書けるようになった. 例えば tails は $[⟨ cons (Nil, Nil), (a \oplus (a s, a c) = cons (cons (a, a s), a c)) ⟩]$ と書ける.

代数的データ型 (Algebraic data types)

双関手 (bifunctor)

双関手とは2つの対象の組を対象に写して2つの射の組を射に写すようなもので, $f : A \to B$ と $g : C \to D$ を $f † g : A † C \to B † D$ とするような $†$ といったもの. ただし $1 † 1 = 1$ , $(f † g) \circ (h † j) = f h † g j$ となるもの. 双関手の変数として $†, ‡$ を用いる.

積

2つの対象 $A, B$ の積とは $A \times B$ なる対象. $\times$ は双関手であり, $f : A \to B$ と $g : C \to D$ とに対して $f \times g : A \times C \to B \times D$ を定める.

また任意の $A, B$ に対して射影関数 $π_{1} : A \times B \to A$ と $π_{2} : A \times B \to B$ を伴う.

関数的に書くと

$(f \times g) (x, x^{'}) = (f x, g x^{'})$
$π_{1} (x, x^{'}) = x$
$π_{2} (x, x^{'}) = x^{'}$

また二項演算子 $Δ$ を

$(f Δ g) x = (f x, g x)$

と定める. 例えば $f \times g = (f π_{1}) Δ (g π_{2})$ である. また簡単に $Δ$ を単項コンビネータとして用いて $Δ x = (x, x)$ とする. これを用いると $f Δ g = (f \times g) Δ$ と書ける.

和

対象 $A$ と $B$ の和を, $A$ と $B$ と加えて ${⊥}$ との直和として定める.

A + B = A ⨿ B ⨿ {⊥}

$f : A \to B, g : C \to D$ に対して $f + g : A + C \to B + D$ を定める. これは関数的に書くと, $A$ のものは $f$ によって $B$ に, $C$ のものは $g$ によって $D$ に, そして $⊥$ は $⊥$ に写すもの.

$(f + g) : A + C \to B + D$
$(f + g) a = f a$
$(f + g) c = g c$
$(f + g) ⊥ = ⊥$

自明な埋め込み射 $A \to A + B$ と $B \to A + B$ が存在する.

$i_{1} : A \to A + B$
$i_{1} a = a$
$i_{2} : B \to A + B$
$i_{2} b = b$

積の時と同様に $▽$ という射に関する二項演算子を導入する. これは選択的に射を適用するようなもので $f : A \to B, g : C \to B$ について

$(f ▽ g) : A + C \to B$
$(f ▽ g) a = f a$
$(f ▽ g) c = g c$

のようなもの.

例えば $f : A \to B, g : C \to D$ について後ろに $i$ を合成すれば $f + g = i_{1} f ▽ i_{2} g$ と書ける. そしてやはり単項コンビネータとしても流用して,

$▽ ⊥ = ⊥$
$▽ (a \in A + C) = (a \in A)$
$▽ (c \in A + C) = (c \in C)$

のように使う.

矢印

二項演算子 $\to$ を定める. 対象 $A, B$ について $A \to B$ とは対象であって, $A$ から $B$ への射全体の集まりを表す. そしてこのような対象には次の射が考えられる.

2つの射 $f : A \to C$ と $g : C^{'} \to B$ について

(f \to g) : (C \to C^{'}) \to (A \to B)

h \mapsto g \circ h \circ f

を定める.

\begin{matrix} A & \overset{f}{\to} & C & \overset{h}{\to} & C^{'} & \overset{g}{\to} & B \end{matrix}

$(f \to g)$ とはその間を埋める射を受け取って全体を合成して出来る射を返すもの

$(g \leftarrow f)$ を $(f \to g)$ と同じ意味で用いる.

関手 $F$ があるときに次のような矢印記法を用いる.

(f \overset{F}{\to} g) = g \circ F h \circ f

また次の合成則がある.

(f \to g) \circ (h \to j) = (h \circ f) \to (g \circ j)

\begin{matrix} A & \overset{f}{\to} & B & \overset{h}{\to} & C & \overset{}{\to} & D & \overset{j}{\to} & E & \overset{g}{\to} & F \end{matrix}

恒等関手, 定数関手

恒等関手 $1$ とは対象と射について恒等的に返すもので $1 D = D, 1 f = f$ .

自由に選んだ対象 $D$ に対して, 全ての対象を $D$ に写すような関手 $\underset{―}{D}$ を定数関手という. ただし射は全て $1_{D}$ に写すとする.

Lifting

関手 $F, G$ に対して関手 $F G$ を次のように定める:

$F G (D) = G (F D)$
$F G f = G (F f)$

また更に双関手 $†$ があるときに関手 $F † G$ を次で定める:

$(F † G) D = F D † G D$
$(F † G) f = F f † G f$

Sectioning

二項演算子 $\oplus$ があるとき, 関数 $(a \oplus)$ を $(a \oplus) b = a \oplus b$ で定める. 同様に関数 $(\oplus b) a = a \oplus b$ を定める. この書き方を sectioning という. 必ず括弧で括る.

以上の記号を用いると, 例えば対象 $A, B$ について $(\underset{―}{A} † 1) (B) = A † B = (A †) B$ なので $\underset{―}{A} † 1 = (A †)$ だと言える.

その他

終対象 (単集合) を $1$ と書く. またこれの要素を $() \in 1$ と書いて void と呼ぶ.

さて述語関数 $p : A \to Bool$ に対して関数 $p ?$ を次のように定める:

$p ? : A \to A + A$
$p ? a = {\begin{cases} ⊥ & when p a = ⊥ \\ i_{1} & when p a = true \\ i_{2} & when p a = false \end{cases}$

例えば $(f ▽ g) \circ p ?$ は我々がよく知る if 文 if p then f else g を表現している.

任意の値を $()$ に写す定数関数を $VOID$ と呼ぶことにする. $VOID \circ f = VOID$ である.

再帰を作るために $μ : (A \to A) \to A$ を定義する.

$μ f = x$
- where $x = f x$

2つの関手 $F, G$ とがあるとき, 対象 $A$ に $φ_{A} : F A \to G A$ を与えるような $φ$ をポリモーフィズム (polymorphism, 多相関数) といい $φ : F \to G$ と書く. 自然関手とは可換性を保つポリモーフィズムだと言える. $φ$ が自然変換であるとはポリモーフィズムであって, 射 $f : A \to B$ があるならば, $φ_{B} \circ F f = G f \circ φ_{A}$ という可換性を満たすもののこと.

再帰型

以上の操作を再帰的に行って得られる型を再帰型という (ってことだよね).

ここで次のような定理が知られている.

関手 $F$ であって連続なものを考えると, ある対象 $L$ があって, 次を満たす2つの射 $i n : F L \to L$ と $o u t : L \to F L$ がある:

$i n \circ o u t = 1$
$o u t \circ i n = 1$
$1 = μ (i n \overset{F}{\leftarrow} o u t)$

$F$ に対して上記のような $(L, i n)$ のことを $μ_{F}$ と書いて最小不動点と呼ぶ.

例として関手 $L X = 1 + A \times X$ を考えると, その最小不動点は $μ_{L} = ([A], ({Nil}^{∙} ▽ cons))$ であって正にリストとその構成を表している. 同様に $N X = 1 + N$ の最小不動点は $(N, (0^{∙} ▽ (1 +)))$ である.

再帰スキーム

一般の再帰型について cata-, ana-, hylo-, paramorphism を与えることをする.

関手 $F$ に対して $(L, i n) = μ_{F}$ であるとする. 3つのポリモーフィズム

$φ_{A} : F A \to A$
$ψ_{A} : A \to F A$
$ξ_{A} : F (A \times L) \to A$

があるとき次を定める.

catamorphism
- $(| φ |)_{F} = μ (φ_{A} \overset{F}{\leftarrow} o u t)$
anamorphism
- $[(ψ)]_{F} = μ (i n \overset{F}{\leftarrow} ψ_{A})$
hylomorphism
- $[[φ, ψ]]_{F} = μ (φ_{B} \overset{F}{\leftarrow} ψ_{A})$
paramorphism
- $[⟨ ξ ⟩]_{F} = μ (f \mapsto ξ_{A} \circ F (1_{L} Δ f) \circ o u t)$

ここで $A, B$ は任意の対象. また左辺の括弧にはどの関手によって定めるものかを表す添字 $_{F}$ があるが, これは誤解がない限り省略する.

1つ目の $φ_{L} \overset{F}{\leftarrow} o u t$ は $f : L \to A$ を取って $A \overset{φ_{A}}{\leftarrow} F A \overset{F f}{\leftarrow} F L \overset{o u t}{\leftarrow} L$ の合成を返す関数. これの $μ$ なので $f = φ_{L} \circ F f \circ o u t$ なる $f$ が $(| φ |)$ .

2つ目以降について型だけ書くと $[(ψ)] : A \to L$ , $[[φ, ψ]] : A \to B$ , $[⟨ ξ ⟩] : L \to L$ .

リストの場合を思い出すと $(| e, \oplus |)$ などと書いてたものは $(| e^{∙} Δ \oplus |)$ と同等のものであったことが分かる. 同様に $[(g, p)]$ と書いていたものは $[((VOID + g) \circ p ?)]$ と書き直される. 具体的には次に計算規則として見ていく.

計算規則

cata, ana, para については共通に Evaluation Rule (対訳不明), Uniqueness Property (唯一性?), Fusion Law (融合則) が成り立つことを見ていく. その中で次の幾つかの定理を用いる.

Fixed point fusion (Free theorem)

関数 $f$ が正格で, $f \circ g = h \circ f$ ならば

f (μ g) = μ h

hylo については ana と cata とに分解できることと次の定理を利用する.

g \circ h = 1

ならば

μ (f \overset{F}{\leftarrow} g) \circ μ (h \overset{F}{\leftarrow} j) = μ (f \overset{F}{\leftarrow} j)

Evaluation Rule for Catamorphism (CataEval)

catamorphism の evaluation rule は次のようなものである:

関手 $F$ とポリモーフィズム $φ : F \to 1$ とその射 $φ_{A} : F A \to A$ について, $μ_{F} = (L, i n)$ とすると

(| φ |) \circ i n = φ_{A} \circ F (| φ |)

\begin{matrix} L & \overset{i n}{\leftarrow} & F L \\ (| φ |) ↓ & F (| φ |) ↓ \\ A & \overset{φ_{A}}{\leftarrow} & F A \end{matrix}

これは $(| φ |)$ の定義から従う. $(| φ |) = μ (φ_{A} \overset{F}{\leftarrow} o u t)$ であったが $μ$ の定義より $(| φ |) = φ_{A} \circ F (| φ_{A} |) \circ o u t$ . 両辺の右に $i n$ を掛けると, $i n$ は $o u t$ の逆射だったので $(| φ |) \circ i n = φ_{A} \circ F (| φ_{A} |)$ を得る.

さてこの法則は evaluation rule という名前の通り, $(| φ |)$ を具体的に計算するための方法を示している.

例

リストの foldr は次のようなものだった

関手 $L X = 1 + A X$
$μ_{L} = ([A], i n)$
- $i n = {Nil}^{∙} ▽ cons$
ポリモーフィズム $φ_{X} = c^{∙} ▽ \oplus$
- $c^{∙} : 1 \to X$
- $\oplus : A \times X \to X$

これらに対して $(| φ |)$ が foldr. では具体的な値について foldr の計算をしてみる.

ただし $L [A] = 1 + A [A]$ について $() \in 1$ の場合と $(a, a s) \in A [A]$ の場合に分ける. これは $i n () = Nil$ と $i n (a, a s) = cons (a, a s)$ の場合に分けてるのと同等 ( $i n$ は同型射なので).

\begin{aligned} (| φ |) Nil & = (| φ |) \circ i n () \\ = φ \circ L (| φ |) () \\ = φ \circ (1 + 1_{A} (| φ |)) () \\ = φ () \\ = (c^{∙} ▽ \oplus) () \\ = c \end{aligned}

\begin{aligned} (| φ |) cons (a, a s) & = (| φ |) \circ i n (a, a s) \\ = φ \circ L (| φ |) (a, a s) \\ = φ \circ (1 + 1_{A} (| φ |)) (a, a s) \\ = φ (a, (| φ |) a s) \\ = (c^{∙} ▽ \oplus) (a, (| φ |) a s) \\ = a \oplus ((| φ |) a s) \end{aligned}

これで全ての場合を網羅できている.

Uniqueness Property for catamorphism (CataUP)

f = (| φ |)_{F} ⟺ f ⊥ = (| φ |)_{F} ⊥ \land f \circ i n = φ \circ F f

すなわち, 先の Evaluation Rule を満たすような $(| φ |)$ は唯一しか存在しないことを主張する.

これもほぼ自明. $(\Rightarrow)$ は Evaluation Rule のまんまなので自明. $(\Leftarrow)$ . $f i n = φ F f ⟹ f = φ F f o u t ⟹ f = μ (φ \overset{F}{\leftarrow} o u t) = (| φ |)$ .

Fusion Law for catamorphism (CataFusion)

f \circ φ = ψ \circ F f

のとき

f \circ (| φ |) = (| ψ |)

どう証明してもいいけど, $(| |)$ の定義のを開けば

\begin{aligned} (| φ |) & = μ (φ \overset{F}{\leftarrow} o u t) \\ = φ \circ F (| φ |) \circ o u t \end{aligned}

両辺に左から $f \circ$ を掛けて

\begin{aligned} f \circ (| φ |) & = f \circ φ \circ F (| φ |) \circ o u t \\ = ψ \circ F f \circ F (| φ |) \circ o u t \\ = ψ \circ F (f \circ (| φ |)) \circ o u t \end{aligned}

というわけで $f \circ (| φ |)$ は $μ (ψ \overset{F}{\leftarrow} o u t)$ である. 一方で $(| ψ |)$ もその $μ$ である. catamorphism の唯一性 (CataUP) よりそれらは等しく

(| ψ |) = f \circ (| φ |)

である.

論文では $f \circ (φ \overset{F}{\leftarrow} o u t) = (ψ \overset{F}{\leftarrow} o u t) \circ f$ であることと fixed point fusion を用いて証明できる, と言っている.

リスト畳込み ( `foldr` ) の融合則

2つのリストの畳込み $(| φ |) = (| c ▽ \oplus |)$ と $(| ψ |) = (| d ▽ \otimes |)$ について, ある $f$ があって,

$d = f c$ ,
$f (x \oplus x s) = y \otimes f (x s)$

のとき

f \circ (| φ |) = (| ψ |) .

包含射は catamorphism

射 $f : A \to B$ に左単位射 $g$ ( $g f = 1$ ) があるとすると, $F g$ は $F f$ の逆射になるので $f \circ φ = (f \circ φ \circ F g) \circ F f$ である. CataFusion で $ψ = f \circ φ \circ F g$ を代入すれば $f \circ (| φ |) = (| f \circ φ \circ F g |)$ を得る.

\begin{matrix} L & \overset{i n}{\leftarrow} & F L \\ (| φ |) ↓ & F (| φ |) ↓ \\ A & \overset{φ}{\leftarrow} & F A \\ f ↓ & F g ↑ \\ B & F B \end{matrix}

上の図式で $A = L, φ = i n$ の場合を考える. 唯一性より $(| i n |) = 1$ を得る. これらを代入することで,

f = (| f \circ i n \circ F g |)

を得る. これに $B = F L, f = o u t, g = i n$ を代入すると,

\begin{matrix} L & \overset{i n}{\leftarrow} & F L \\ (| i n |) ↓ & F (| i n |) ↓ \\ L & \overset{i n}{\leftarrow} & F L \\ o u t ↓ & F i n ↑ \\ F L & \overset{F i n}{\leftarrow} & F F L \end{matrix}

一番下の $F (i n) : F^{2} L \to F L$ の catamorphism を考えることで

(| o u t \circ i n \circ F (i n) |) = (| F (i n) |) = o u t

を得る.

catamorphism は正格性を保つ

まず関手 $F$ が正格性を保つ, すなわち $f ⊥ = ⊥ ⟺ E f ⊥ = ⊥$ とする. このとき

φ ⊥ = ⊥ ⟺ (| φ |)_{F} ⊥ = ⊥

が成り立つ. 添字の $F$ は $F$ の下でのバナナであることを表したのに註意.

$(\Rightarrow)$ . $(| φ |) = ⊥$ を仮定すると

\begin{aligned} ⊥ & = (| φ |) ⊥ \\ = (| φ |) i n ⊥ \\ = φ F (| φ |) ⊥ \\ = φ ⊥ \end{aligned}

より従う. ここで最後の式変形には $F$ が正格性を保存することと $(| φ |) ⊥ = ⊥$ を仮定していることから $F (| φ |) ⊥ = ⊥$ を用いた.

Evaluation Rule for Anamorphism (AnaEval)

関手 $F$ とその $μ_{F} = (L, i n)$ について, $ψ_{A} : A \to F A$ に対して $[(ψ)] = μ (i n \overset{F}{\leftarrow} ψ)$ が定義だったので,

[(ψ)] = i n \circ F [(ψ)] \circ ψ

である. この両辺に左から $o u t \circ$ を掛けることで次を得る.

AnaEval

o u t \circ [(ψ)] = F [(ψ)] \circ ψ

\begin{matrix} X & \overset{ψ}{\to} & F X \\ [(ψ)] ↓ & F [(ψ)] ↓ \\ L & \overset{o u t}{\to} & F L \end{matrix}

これはやはり

[(ψ)]

に関する評価規則を示している.

例. unfold

$A$ のリスト型 $F : X \to 1 + A X$ について, リストのunfoldは $g : X \to A X$ と $p ? : X \to X + X$ によって $[(ψ)] = [((V O I D + g) \circ p ?)]$ と表されると言った. これの評価を考える.

\begin{aligned} [(ψ)] x & = i n F [(ψ)] ψ x \\ = {\begin{cases} ⊥ & when p x = ⊥ \\ i n F [(ψ)] () & when p x = true \\ i n F [(ψ)] (a, x^{'}) & when p x = false, (a, x^{'}) = g x \end{cases} \end{aligned}

ここで $F [(ψ)] = 1 + 1 \times [(ψ)]$ であるので,

$i n F [(ψ)] () = i n () = Nil$
$i n F [(ψ)] (a, x^{'}) = i n (a, x^{'}) = cons (a, x^{'})$

となっていわゆる unfold を得る.

例. iterate

$f : A \to A$ とリスト型 $F : X \to 1 + A X$ について $ψ_{A} = 1_{2} \circ (1_{A} Δ f) : A \to F A$ とする.

\begin{aligned} ψ_{A} x & = i_{2} (1 Δ f) x \\ = i_{2} (x, f x) \\ = (x, f x) \in 1 + A X \end{aligned}

\begin{aligned} o u t [(ψ)] x & = F [(ψ)] ψ x \\ = (1 + 1 \times [(ψ)]) (x, f x) \\ = (x, [(ψ)] (f x)) \end{aligned}

(左からinを掛けることで)

[(ψ)] x = cons (x, [(ψ)] (f x))

を得る. これは Haskell なのでは iterate f として知られる.

anamorphism の唯一性 (AnaUP)

f = [(ψ)]_{F} ⟺ o u t \circ f = F f \circ ψ

anamorphism の融合則 (AnaFusion)

$φ \circ f = F f \circ ψ$ のとき

[(φ)] \circ f = [(ψ)]

唯一性より従う.

全射は anamorphism

以上のことは単に catamorphism の双対を取れば導けた. 全く同様に, 包含射即ち左単位射を持つ射が catamorphism であったことから, 全射即ち右単位射を持つ射は anamorphism である.

全射を $f$ として, ある $g$ によって $f g = 1$ であるとすると,

f = [(F g \circ o u t \circ f)]

が成立する.

これに $f = i n, g = o u t$ を代入することで,

[(F (o u t) \circ i n \circ i n)] = [(F (o u t))] = i n

を得る.

Splitting Hylomorphism (HyloSplit)

$g h = 1$ のとき, 合成則 $μ (f \overset{F}{\leftarrow} g) \circ μ (h \overset{F}{\leftarrow} j) = μ (f \overset{F}{\leftarrow} j)$ が成り立つ. これによって次の定理が成り立つ.

[[φ, ψ]] = (| φ |) \circ [(ψ)]

Shifting Law for Hylomorphism (HyloShift)

関手 $F, M$ があり, $φ : M L \to B$ , $ψ : A \to F A$ , $ξ : F \to M$ とする.

\begin{matrix} A & \overset{ψ}{\to} & F A & \overset{ξ_{A}}{\to} & M A \\ ↓ \\ B & \overset{φ}{\leftarrow} & M L & \overset{ξ_{B}}{\leftarrow} & F B \end{matrix}

上の図式において $[[\dots]] : A \to B$ は $F$ に於いても $M$ に於いてでも正しく定まり,

[[φ_{B} ξ_{B}, ψ_{A}]]_{F} = [[φ_{B}, ξ_{A} ψ_{A}]]_{M}

が成り立つ.

これは cata や ana と違って陽に $μ_{F}, μ_{M}$ が登場しないからこういうことが出来る.

cata と ana の関係

μ_{F} = (L, i n_{F})

μ_{M} = (L, i n_{M})

でこの間にポリモーフィズム

φ : F \to M

があるとき,

(| i n_{M} \circ φ |)_{F} = [(φ \circ o u t_{F})]_{M}

\begin{matrix} L & \overset{out}{\to} & F L \\ φ ↓ \\ L & \overset{in}{\leftarrow} & M L \end{matrix}

ψ \circ φ = 1

のとき,

μ

の合成則より

[(ψ)] \circ (| φ |) = 1

例えば foldr してから unfold した結果が元に戻るための十分条件として, ポリモーフィズムのレベルで合成が $1$ であることがある.

Evaluation Rule for Paramorphism (ParaEval)

定義がだいぶ前なので, 改めて paramorphism の定義を書くと, $μ_{F} = (L, i n)$ についてポリモーフィズム $ξ_{A} : F (A L) \to A$ があるとき $[⟨ ξ ⟩]$ とは, $f : L \to L$ なる射によって

[⟨ ξ ⟩] \equiv μ (f \mapsto ξ_{L} \circ F (1 Δ f) \circ o u t)

と書かれるもの.

従って

[⟨ ξ ⟩] = ξ_{L} \circ F (1_{L} Δ [⟨ ξ ⟩]) \circ o u t

両辺に右から $i n$ を掛けることで

[⟨ ξ ⟩] \circ i n = ξ_{L} \circ F (1_{L} Δ [⟨ ξ ⟩])

を得、これが paramorphism の評価規則になっている.

例. リスト

$F X = 1 + A X$ について $ξ_{A} : F (A L) \to A$ の paramorphism を考える.

$F (1_{L} Δ [⟨ ξ ⟩]) x = (1 + 1 \times (1_{L} Δ [⟨ ξ ⟩])) x$ は $x \in 1$ なら $() \in 1$ , さもなくば $x = (a, b) = A \times L$ であって値は $(a, (b, [⟨ ξ ⟩] b))$ であることに註意すると,

\begin{aligned} [⟨ ξ ⟩] Nil & = [⟨ ξ ⟩] i n () \\ = ξ F (1 Δ [⟨ ξ ⟩]) () \\ = ξ () \end{aligned}

\begin{aligned} [⟨ ξ ⟩] cons (a, a s) & = [⟨ ξ ⟩] i n (a, a s) \\ = ξ F (1 Δ [⟨ ξ ⟩]) (a, a s) \\ = ξ (a, (a s, [⟨ ξ ⟩] a s)) \end{aligned}

唯一性 (ParaUP)

f = [⟨ ξ ⟩]_{F} ⟺ f \circ i n = ξ \circ F (1 Δ f)

融合則 (ParaFusion)

f \circ φ = ψ \circ F (1 \times f)

のとき

f \circ [⟨ φ ⟩] = [⟨ ψ ⟩]

\begin{matrix} L & \overset{o u t}{\to} & F L \\ [(ψ)] ↓ \\ L & \overset{φ}{\leftarrow} & F (1 \times L) \\ f ↓ & ↓ F (1 \times f) \\ L & \overset{ψ}{\leftarrow} & F (L \times L) \end{matrix}

定理

f = [⟨ f \circ i n \circ F π_{1} ⟩]

Parameterized Types (パラメータ化された型)

最初のほうで map 関数というものをやった. 即ち型 $A, B$ に対しては型 $[A], [B]$ というものを定義することが出来, 射 $f : A \to B$ に対して $f * : [A] \to [B]$ というものを定めることが出来た. また明らかに $1 * = 1$ , $f * \circ g * = (f g) *$ が成り立つ. この意味で $*$ は関手である $(A * = [A])$ . これを一般化する.

Sectioning について (復習???)

双関手 $†$ とある対象 $A$ について,

(A †) = \underset{―}{A} † 1

であった. つまりこれは関手であって,

$(A †) B = A † B$
$(A †) f = (\underset{―}{A} † 1) f = 1_{A} † f$

と写す.

射 $f : A \to B$ について $(f †)$ はポリモーフィズムであって (!!),

$(f †) : (A †) \to (B †)$
$(f †)_{X} : (A † X) \to (B † X)$
$(f †)_{X} = f † 1_{X}$

Maps

関手 $*$ を次のように定義し直す.

ある双関手 $†$ と対象 $A$ について $μ (A †) = (A *, i n_{A})$ であると定義する. 同様に対象 $B$ については $μ (B †) = (B *, i n_{B})$

ある射 $f : A \to B$ があるとき,

φ = i n_{B} \circ (f †)_{B *} : A † B * \to B *

が定まる. この catamorphism を $f *$ であると定義する.

f * = (| i n_{B} \circ (f †)_{B} * |)_{(A †)}

\begin{matrix} A * & \overset{i n_{A}}{\leftarrow} & A † A * \\ f * = (| φ |) ↓ \\ B * & \overset{i n_{B}}{\leftarrow} & B † B * & \overset{(f †)_{B *}}{\leftarrow} & A † B * \end{matrix}

先の "cata と ana の関係" でも見たように,

f * = [((f †)_{A *} \circ o u t_{A})]_{(A †)}

\begin{matrix} A * & \overset{o u t_{A}}{\to} & A † A * & \overset{(f †)}{\to} & B † A * \\ f * = [(ψ)] ↓ \\ B * & \overset{i n_{B}}{\leftarrow} & B † B * \end{matrix}

と書き直すことも出来る.

以上で関手 $*$ が定義された. これはリストのマップとして定義した $*$ の一般化になっている. $A † B = 1 + A \times B$ とすればリストの場合が導出出来る.

合成

合成に関して次が成立する.

\begin{aligned} f * \circ g * & = (| i n \circ (f †) |) \circ (| i n \circ (g †) |) \\ = (| i n \circ (f †) \circ (g †) |) \\ = (| i n \circ ((f \circ g) †) |) \\ = (f \circ g) * \end{aligned}

Map-Reduce

関手 $F$ と対象 $A$ について $A † X = A + F X$ としたときの $(A *, i n) = μ (A †)$ を $A$ の上の free $F$ -type と呼ぶ.

$f : A \to B$ について, $f * = (| i n_{B} \circ (f †)_{B *} |)$ であったが, 今 $τ_{B} = i n \circ i_{1} : B \to B *$ , ${join}_{B} = i n \circ i_{2} : B * \to B *$ とすると,

f * = (| (τ_{B} \circ f) ▽ {join}_{B} |)

と書き直せる.

射 $φ$ に対して次で定める $φ /$ を $φ$ の reduction と呼ぶ:

φ / = (| 1 ▽ φ |)

これに関して次が成り立つ.

\begin{aligned} (| f ▽ φ |) & = (| (1 ▽ φ) \circ (f + 1) |) \\ = (| 1 ▽ φ |) \circ f * \\ = φ / \circ f * \end{aligned}

さて実は $τ, join$ は自然変換である.

\begin{matrix} A & \overset{f}{\to} & B \\ τ_{A} ↓ & τ_{B} ↓ \\ A * & \overset{f *}{\to} & B * \end{matrix}

\begin{matrix} F A * & \overset{F f *}{\to} & F B * \\ {join}_{A} ↓ & {join}_{B} ↓ \\ A * & \overset{f *}{\to} & B * \end{matrix}

このことから $f *$ の評価規則を得る:

$f * \circ τ = τ \circ f$
$f * \circ join = join \circ F f *$

一方で $φ /$ の評価規則は普通に CataEval から次のようになる:

$φ / \circ τ = 1$
$φ / \circ join = φ \circ F (φ /)$

モナド

free type があるとき, モナドを次のようにして与えることが出来る. つまり

関手 $*$
自然変換 $τ : 1 \to *$
自然変換 $join / : * * \to *$

について

$join / \circ τ = 1$
$join / \circ τ * = 1$
$join / \circ join / = join / \circ join / *$