読者です 読者をやめる 読者になる 読者になる

Just $ A sandbox

プログラミングと計算機科学とかわいさ

variable-free type theoryの圏論的な解釈について

myuon-myon.hatenablog.com

の続き. いくつか疑問が解消されたのでそれについて.

var-free type theoryについて

  • syntaxはcontext, type, term, substからなる.
  • contextはtypeの有限列(通常はvariableとそのtypeの組の列だが, 今回はvariable-freeなのでtypeだけの列になる).
  • typeはground typeと関数型A → Bとsubstが代入された型(σ[s]の形をしているもの)のいずれか.
  • termは1と代入された項M[s]のいずれか.
  • substはidと合成f . gとshiftとextension<f:subst, M:term>のいずれか.

termは型付けをde Bruijn indexで考える.
term1はcontextの直近のtypeに対応する項とみなす. 例えば, Γ,σ ⊢ 1:σなどである.

substはcontextの間の変換とみなす.
例えばΓ ⊢ id:Γid(Γ)=Γを表す. また, 合成は通常と逆向きに書くらしい(多分見やすさの都合).
shiftはindexをすべて1つ加算するような変換とみなす. 例えばΓ,σ ⊢ ↑:Γはindexが上に1つずれるので一番新しいtypeσを忘れるものとみなす.

extensionのtyping ruleは次のようなものである:
Γ ⊢ f:Γ', Γ' ⊢ σ, Γ ⊢ M:σ[f] ⇒ Γ ⊢ <f,M>:Γ',σ

これは, Mによってcontextに新しいtypeを付け加える操作と考えることができる.
あるいは, 変換fをMによって拡張したものとみなしてもよい.

locally cartesian closed categoryでの解釈

ML theoryはLCCCとイイカンジに対応する.
ここではcategory with attributesを使った解釈を使うことにする.

すると上で導入したsyntaxはLCCC(cwa)でいい感じに解釈できる.

  • contextはobject, contextΓのtypeはΓ-cod morphismとみなす.
  • type Aをもつtermは, Aに対応するmorphism(shift)のsection.
  • substはmorphismとみなす.

以上の対応で, 上のsyntaxはcwaの構造で超いい感じになる.

  • function typeはPi-typeを使って定義するので一旦忘れる. (論文にあるようなcwaを構成するとdependent product/sum, extensional identity typeを持つ)
  • substidはidentity, 合成はcompositionになる.
  • shiftはcwaのcanonical projection operatorになる.
  • 代入された項M[s](M:Γ → Γ,A, s:Γ'→Γ)はpullbackΓ'×Γ,A[s]overΓのUMPから誘導されるmorphism
  • extension<f,M>はpullbackの対角線にあたるmorphism(Mとfのliftを合成する).
  • 1=<id,id>はpullbackのUMPからつくる.

Set model

上のだけだとよく分からないのでSetで解釈する.

  • shiftはshift写像<gi,a:A> ~> <gi>
  • termはこのsectionなので, A型の値の追加, <gi> ~> <gi,a:A>になる. これはa:Aと同一視できる.
  • 代入項に登場するpullbackはΓ'×Γ,A[s] = {(gi', gi, a) | s(gi')=gi, a=M} = {(gi',M)}と同一視できる.
  • よってM[s]<gi'> ~> (<gi'>,M)とみなせる.
  • extensionは<f,t:A> = ↑*f . t ; <gi'> ~> <gi',t> ~> <f(gi'),t>になる.

特に特徴的なのはextensionの拡張で, fによる変換をtで拡張したもの, i.e. fの変換に加えてtの値を写像に追加するものと考えることができる.
extensionっぽさがあってとてもよい.

余談

もともとML type theoryのcwaでの解釈の話を調べていてvar-free syntaxが出てきたので何かしら関係はあるのだろうと思っていたけど, ちゃんと直感的にいい感じに対応していて超すっきりした.

ついでに, 普通のλ計算とvar-freeなλ計算の変換を具体的に構成したい.
さらに気が向いたらproof formalizationもしたい.

参考文献

データ型のCPS変換について

Haskell

HaskellCPS変換とか調べているとデータ型の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変換は前者で, 前者は主に末尾再帰とかそういう話だと思うんだけど, HaskellCPS変換の話をググると(他の言語でもそうかも?)後者のCPS変換も結構ちょくちょく出てくる.

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

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

参考文献

type theory with variable-free syntax

Agda 後で考える 定理証明

(追記) 解決した: variable-free type theoryの圏論的な解釈について - Just $ A sandbox

--

文献に突然登場して?ってなったので.
調べても情報がヒットしないのでよくわからないけど, simply typed lambda calculusを変数を使わずに定義するものらしい.

で, STLCかなんかでうまく解釈できるかと思ったけど思いつかなかった.

まず, 代入が変数に関数値を代入しているのかと思ったらそうじゃないっぽい(合成の順番が逆だし).
さらに適用みたいな記号で書いてるM∙sは何者なんだという感じ.

でも1はde Bruijn indexに従ってcontextの一番近くの型を取り出しているし, 1[↑] = 2ともみなせるのでなんか意味はありそう.

圏論的な解釈を考えると自然にでてくるんだろうか. 謎.

gist.github.com

参考