#はじめに
前回の投稿から少々考えていたのだが、やや理解が固まったので書いてみる、ただ中身は前回から少しも増えていない。
何を考えていたかというと、リストから差分リストへ変えたことで効率が上がったが、これはたまたまこの場合のみ使えるテクニックなのかあるいは何か背景があるのか？という疑問である。
これの答えはある程度肯定的であって、普通のリストと差分リストの間のような関係がもっと一般的に存在することが分かった、しかもその間を結ぶのが（お気に入りの）米田の補題である、なんと。
つまり、ある種の最適化問題はデータあるいは関数の型を継続渡しスタイルというのに変えるということに帰着していて、かつこれは必ず実行可能である、ということらしい。
元ネタはこれ
多分書いたのはこの人Dr. Georg Martius
#継続渡し
CPSと略されるこの形式の一般論には深く立ち入らないことにする、というかよく知らない。
ここでは元ネタからの引用のみにしておく、興味ある人は調べて下さい、知ってる方は教えて下さい。
CPS is a way to write a function that explicitly tracks what is being done with its return value.
In CPS every function is tail-recursive and the rest of the computation is handled in the new continuation that is handed to the recursive call.
#米田の補題
圏論の試金石的な大定理、手前味噌的に自分の過去の資料を貼ってみる
ついでに絵算も宣伝がてら。
つまり以下の同型（一対一写像が存在する）が言えるということだ
Nat(C(A,-),F) \equiv FA
左辺は(arrowからarrowへの）arrowで右辺はobjectにあたり、この場合左辺のCPSと右辺の普通のスタイルが一対一に対応してますよ、ということになる。
#リストと差分リスト（おさらい）
リストと差分リストは両方共モノイドである、つまりconcatenationなる二項演算（つまりは積）があって連結できる、がその連結の仕方が微妙に異なるのである、ここがみそ。
普通のリストは
"cat"
みたいなもので、これの結合は(++)関数。
それに引き換え差分リストは
\xs -> "cat" ++ xs
という定義でかつ結合はなんと関数適用(.)、念のため定義を書くと
g.f = \x -> g (f x)
となっている。
さてでは前回の投稿
から例を拝借して説明してみる、まずは普通のかつ効率のよいリストの結合
"cat" ++ ("fish" ++ "burger")
諸事情によりこの連結が出来ずに泣く泣く
("cat" ++ "fish") ++ "burger"
の順番でしか結合できないとする。
さて差分リストは定義からすでに矢印的であり、詳細は前回の投稿にある通り
\xs -> "cat" ++ ("fish" ++ ("burger" ++ xs)
となって効率良い連結順になる、というわけである。
しかも差分リストの連結は関数の積であり、これはまさにCPSであると言える、バンザイ。
#間の対応
Yoneda’s lemma now states that programs in regular style and CPS are isomorphic.
リストと差分リストの間の一対一対応はほとんど見て明らかだが、圏論的に考えればこれは一般的に成り立つ事実である、ということである。
#おわりに
少々尻切れトンボな感じが否めないが、もともとモナドについて調べ物している時の副産物なので平にご容赦を、あと全体的にあまり正誤に自信がないので詳しい方いらしたら教えて下さい。