HaskellでCPS変換とか調べているとデータ型のCPS変換というのが出てくる.

関数のCPS変換は継続を引数に追加して末尾再帰の形にすればだいたいOKなのでまあわかるのだけど, データ型のCPS変換というのは何なんだという話.
継続は何を継続しているのかがいまいち分からないので何故そのデータ型はCPS変換するとその型になるんだと不思議に思っていたのがちょっと解決したのでそれについて書く.

関数 is っょぃ

パフォーマンスのことを考えれば, 関数型と基本型(ground type)が型の中では圧倒的に偉い.
基本型というのはまぁproductとかrecursionとかdependent typeとかを含まない基本的な型のこと. 例えばIntとか(Haskellのような言語ではIntというのは計算機の都合上特別扱いされているので, ここでのIntはN×Nにring構造を入れたもののことではない).

基本型は基本的にコンパイラのサポートが受けられるので特別な形で処理されるから処理は速い.
関数型は作ったり壊したり(introしたりelimしたり)が速いので速い.
その他の型, つまりproductとかcoproductとかなんかそういうのが遅いのはコンストラクタに対するパターンマッチを何度も繰り返すからで, パターンマッチをさせない書き方ができれば処理が速くなる可能性がある.

そこでデータ型を関数型と基本型の組み合わせでそれと同型なものに変換できない？という発想になる.

Cont iso

初めに, 次が成り立つ:

型Aに対し, Aと∀P. (A -> P) -> Pはiso.
(Prf) a:A ==> λ(f:A->P). f(a):P, h:(A->P)->P ==> h(id:A->A):A は同型を与える.

この対応は(名前があるのか知らないけど)至るところに現れる.
例えばP=bottomの時は右辺の型は¬¬Aのことだし, ContモナドはCont r a = (a -> r) -> rだったし, そもそもA -> (A -> P) -> Pは単なる関数適用のflip版のことだった. さらに言えば, この同型はyoneda lemmaのId functorに適用した形になっているとも言える.
Contモナドの名前的に明らかにこのことは継続とかそういうのと関係しているのだけどこれだけでは何のことかはわからない. わからないのでもう少し話を進めてみることにする.

直和型

A+Bの直和型を特徴づけるものといえば当然elim ruleになる.(何故かは下で分かる) というのも, 直和型のelim ruleはちょうどcoproduct図式のUMPをもつ射に対応する.

A+Bのelim rule: ∀P. (A -> P) -> (B -> P) -> (A+B -> P)

これは次と同値: A+B -> ∀P. (A -> P) -> (B -> P) -> P

偶然(要出典), 最初にやった同型と同じ * -> (∀P. (..) -> P) の形が出てきた.
で, coproductはup to isoに決まるので∀P. (A -> P) -> (B -> P) -> PはそもそもA+Bと同型になる. これによって次のことがわかる.

A+B = (∀P. (A -> P) -> (B -> P) -> P) と定義してよい. 右辺はパターンマッチが起こらないので速い.

elim ruleとは何か

で, このelim ruleとは何なのかという話だけど, これは次のようにして導出される:

A+B = ∀P. (A+B -> P) -> P    : 最初の同型
= ∀P. hom(A+B, P) -> P
= ∀P. hom(A,P) × hom(B,P) -> P    : homはcoproductをproductに変える
= ∀P. (A -> P) × (B -> P) -> P
= ∀P. (A -> P) -> (B -> P) -> P    : 直積と冪の随伴(curry化)

一般に, inductive datatypeというのはelim ruleが本質的に効いてくる.
(これはinductionがelim ruleになってるということを表している)
その場合は上のような変換で簡単な形に変形できる.

直積型

直積は上の双対なのでintro ruleが対応するけれど, こちらは上のようなほしい形と一致しない.
けれど, なんと直積はCCCでは(後で補足する)左随伴なのでいい感じに変形ができる.

A×B = ∀P. (A×B -> P) -> P
= ∀P. (A -> B -> P) -> P    : 直積と冪の随伴(curry化)

例: List

あとは上のことを使って機械的に変形するだけで単純な形のデータ型なら大体いい感じの型が作れる.

例) List

[a] = 1 + a × [a]
= ∀P. ((1 + a × [a]) -> P) -> P
= ∀P. ((1 -> P) -> (a × [a] -> P) -> P) -> P    : coproductのPR変換
= ∀P. ((1 -> P) -> (a -> [a] -> P) -> P) -> P    : productのPR変換
= ∀P. (P -> (a -> [a] -> P) -> P) -> P    : CCCならhom(1,P)=P

この定義でhead, tailなどは簡単に実装できる.

まとめ

以上により, データ型はパターンマッチを含まないより速い形に書き換えられることがわかった.
このようにして書き換えたものの中で, 継続渡しっぽさを含むものをCPS変換されたデータ型と呼ぶっぽい.
(ちなみに, (... -> P) -> Pが割と継続渡しっぽさがある)

ちなみにこのようなぽさを含むもの全体が上で変換された全体と一致するかどうかは私は知らない.

軽いまとめ:

直積とか直和はいい感じに変形できて便利.
関数型がめっちゃ偉い.
上の記述はだいたいHaskellとかで考えていたけれど, CCCな型システムを持つ言語なら同じことが出来ると思う

Haskellの型システムってCCCじゃないですよね？？？？*1

ﾔ,ﾔﾒﾛｫ〜〜〜(今回はundefinedとかいう邪悪なものは考えてない)

はじめに

初めに書きたかったことを書く.
CPS変換でググると, CPS変換とは継続をうんたらかんたらとかいう文章がヒットしまくるけど何の説明にもなっていないということがすでに人生で5億回くらいあった.

一応自分の中では「関数の」CPS変換と「データ型の」CPS変換という2種類の言葉があり, 前者はContモナドを使った書き方で後者は今回説明したようなことに対応しているのだろうという理解でいる.
本来のCPS変換は前者で, 前者は主に末尾再帰とかそういう話だと思うんだけど, HaskellとCPS変換の話をググると(他の言語でもそうかも？)後者のCPS変換も結構ちょくちょく出てくる.

とりあえずCPS変換の言語に依らないちゃんとした定義を発見するか自分で作ることができれば, この腑に落ちない感じも少しは改善するのかも.

あと, 上のことはCPS変換と何の関係もないかもしれない.
(CPS変換の定義が分からないので関係があるかどうかもわからない)
でも上の操作でパターンマッチは確実に減るので, まあ誰かの役に立てばいいなと思いました.