2014-11-03

Codensity Monad

Agda Haskell

Codensity という型がある. 定義は以下.

newtype Codensity m a = Codensity { runCodensity :: forall b. (a -> m b) -> m b }

instance Functor (Codensity k) where
  fmap f (Codensity m) = Codensity (\k -> m (k . f))

instance Monad (Codensity f) where
  return x = Codensity (\k -> k x)
  m >>= k = Codensity (\c -> runCodensity m (\a -> runCodensity (k a) c))

これの何が良いかと言うと, これは以下のようにMonadFreeな作用を持つ.

instance (Functor f, MonadFree f m) => MonadFree f (Codensity m) where
  wrap t = Codensity (\h -> wrap (fmap (\p -> runCodensity p h) t))

Codensityはnewtypeで実装されているから, 実行時には Codensity や runCodensity によるオーバーヘッドは考えなくて良い. だから, m のMonadFreeのメソッドを直接呼ぶよりも効率よくなる可能性が高い. 特に, 元々のmが「重い」モナドなら, Codensity をかぶせるだけで劇的に速くなることがある.

Codensityのパフォーマンスの話は http://www.iai.uni-bonn.de/~jv/mpc08.pdf などを参考にしてもらうことにして, 以下ではCodensityの(圏論的な)説明をしてみる.

以下, 定義などは逐一述べないので必要に応じてnLabなり参考文献に挙げたものを参照してください.

RanとCodensity

functor p : C → Dに対し, functor $p^{-1} \colon \mathcal{E}^\mathcal{D} → \mathcal{E}^\mathcal{C}$ を, $p^{-1}(F) = F \circ p$ によって定める. ただしここで $\mathcal{E}^\mathcal{D}$ とはDからEへの関手のなす関手圏のこと.

functor f : C → E, p : C → Dに対し, pに沿ったfの右Kan拡張 $p \ddagger f$ を考える.
$p \ddagger$ が存在すれば, これは $p^{-1}$ の右随伴である.

D
↑　↘ p‡f
| ⇓ ↘
C ――→　E

随伴の定義から,

$\hom(p^{-1}(-),f) \cong \hom(-,p \ddagger f)$

ここで, $\mathcal{C}$ の対象aを一つ固定し, 米田関手yを用いて

$\hom(p^{-1}(ya),f) \cong \hom(ya,p \ddagger f)$

$p^{-1}$ の定義に戻れば,

$\hom(ya \circ p,f) \cong \hom(ya,p \ddagger f)$

さらに右辺で(共変)米田の補題を用いて,

$\hom(ya \circ p,f) \cong \hom(ya,p \ddagger f) \cong (p \ddagger f)(a)$

なる同型を得る. ゆえに $(p \ddagger f)(a)$ が存在したとすれば最左辺と同型になる.
さて今はHaskellでの話がしたいので, 対象とは型であり, 射とは函数である. $\hom(ya \circ p,f)$ とは, 自然変換の集合であるが, これを $ya \circ p \rightarrow f$ なる自然変換からなる型と同一視する.

このような仕方で $(p \ddagger f)(a)$ を最左辺で定義すると,
自然変換 ya . p ~> f は RankNTypes を用いて, forall b. (a -> p b) -> f b なる型を持つ.

よって,

newtype Ran p f a = Ran (forall b. (a -> p b) -> f b)

を得る. これは http://hackage.haskell.org/package/kan-extensions-4.1.0.1/docs/Data-Functor-Kan-Ran.html で定義されている.

最後に, pもfもmで固定してしまうと,

newtype Ran     m m a = Ran       (forall b. (a -> m b) -> m b)
newtype Codensity m a = Codensity (forall b. (a -> m b) -> m b)

により, Codensityが得られた.

HaskellでのFunctor, Monad

上のような操作でCodensityは得られるが, 上の操作では pやfは関手 であった.
しかしCodensityはFunctorのinstanceで(Functor m) =>を要求しない (つまり, mがFunctorやMonadでなくとも, CodensityはFunctorおよびMonadになる).

最初の実装で確かにCodensityがFunctorやMonadになることは確認が必要なので, Agdaで証明を書いてみた.

確かに,

instance Functor (Ran p f)
instance Functor (Codensity k)
instance Monad (Codensity f)

なるインスタンスが正しく実装されていることが分かる.

参考文献

http://alg-d.com/math/category/ 日本語で読める圏論pdfで, Kan拡張についても記述があるサイト.
http://hackage.haskell.org/package/kan-extensions-4.1.0.1 package kan-extensions (by ekmett)
http://comonad.com/reader/2011/free-monads-for-less/ Codensityについての解説.

2014-10-29

Agdaで集合論をやろうとして上手く行かなかった

Agda 後で考える

この前の記事の方針でゴリゴリ公理を追加していたら, 問題が発生した.

写像の定義を

_⟶_ A B = ∀ x → x ∈ A → ∃ \y → y ∈ B

としたら, (これはとても自然な定義に見えるけれど)例えば A ≡ B から f(A) ≡ f(B) が導けなくなる.
x ∈ A を像の方に押し込めて

_⟶_ A B = ∀ x → ∃ \y → x ∈ A → y ∈ B

のように定義すると, 今度は x ∈ A に依って決まる写像が定義できなくなる.

最初の方法ではZFCから排中律を示すところで引っかかり(本来異なる集合 A,B に対して A ≡ B を言おうとするので型エラーになって上手く行かない), あとの方法では置換公理を使う場面でひっかかる(函数の像を扱うとき).
よっていずれにせよ上手く行かない.

この前の記事のコメントではAgdaの型を用いて ∈ を定義する方法も教えてもらった.

data _∈_ {l} {A : Set l} (x : A) (B : Set l) : Set (suc l) where
  in-eq : A ≡ B → x ∈ B

この方法だと, ∈ の定義がもろにAgdaの型システムに依存しているので, 方針はガラッと変わるはず.
多分これで今やっていることの模倣はできると思うけれど, そもそも何を公理として仮定して良いのかが分からないし, もともとAgdaの型システムではどういうことができるのかもよく分からないのでなんとも言えない.

Agdaの方に上手く寄れば, 多分普通の数学の模倣はできるような気がするけれど, 少なくとも数学のやり方をそのまま持ってくるだけでは上手く行かないのかなぁと思った.
こういうことをするなら, Agdaよりもっと向いている言語を他に探したほうがいいのかもとも思った.
でもAgdaはHaskellerの自分にとっては学びやすかったし, 気に入ったところも多かったので少し残念.

供養

https://github.com/myuon/agda-cate

(圏論はそれなりに上手く行っているので, 圏論方面はもう少し開発を続けるかもしれない)

2014-10-26

矛盾の証明

Agda

矛盾を示すときに使える方法としては主に以下の2つだと思う

命題 ¬P に P をぶつける
矛盾 ⊥ の特徴付けを使う

矛盾の特徴付けというのは, 例えばAgdaだと⊥は空集合の公理を満たすことが示せるから,
空集合の公理がそのまま矛盾の特徴付けになる.
∃ \(A : Set) → (∀ x → ¬ (x ∈ A))

否定命題にPをぶつけるというのは口で言うほど簡単ではなくて, まずどの否定命題を選んでくるかからよく考えないといけない.

一体何の話かというと, Agdaで「ZFC ⇒ 排中律 (P ∨ (¬ P))」を示すときに,

https://myuon.github.io/agda-cate/Sets.Sets.NonDatur.html#660

A = ⟦ x ∈ [0,1] ∣ x ≡ 0 ∨ P ⟧　-- A := {x ∈ {0,1} ∣ x = 0 ∨ P}
B = ⟦ x ∈ [0,1] ∣ x ≡ 1 ∨ P ⟧　-- B := {x ∈ {0,1} ∣ x = 1 ∨ P}
X = [ A , B ] -- X := {A,B}

みたいにするんだけど, 以下の議論では, ここにさらっとでてくる自然数0と1が異なることが仮定されている.

0と1は上のように非順序対を作って使うので適当なsetでないといけないんだけど, 当然AgdaのData.Natで定義されているNatの元は(inductive data typesで定義されているから)setではない.
そこで 0 = ∅, 1 = ∅ ∪ {∅} に戻って0と1が異なることを示さないといけなかったけれど, これには空集合の公理や対の公理や和集合の公理が必要で, しかもそんなに明らかなことでもない.
https://myuon.github.io/agda-cate/Sets.Sets.Natural.html#793

Natの世界でもSetの世界でも0と1が異なることを示すには, 0=1を仮定して矛盾を導かなければいけないので, それがいつも自明なことではないなと実感した.

というかむしろ, Agdaの場合は同値なものがrewriteによって書き換えるだけで証明が済んでしまうことが多いので, 等しさが特別扱いやすいだけなのかもしれないけど.