Avendia20

日記 (2021 年 7 月 7 日)

Haskell には lens というパッケージがあり、 オブジェクトの一部分を取り出したり書き換えたりする操作を抽象化したレンズと呼ばれる仕組みを提供している。 このページでは、 このパッケージで定義されているレンズの型と、 素朴にゲッターとセッターを対にしたタプル型とが、 実は等価になることを述べた。 今回は、 この事実を圏論的視点から見る。

全体のオブジェクトの型を s で表し、 そのオブジェクトの中の取り扱いたい部分の型を a で表すことにすると、 ゲッターの型とセッターの型はそれぞれ s -> a と s -> a -> s と書けるのであった。 ここではこれを少し一般化して、 セッターを使うときに渡すセットする値の型が a と異なっていたり、 セッターで値をセットした結果得られる全体のオブジェクトの型が s と異なっていたりしても良いことにする。 この場合、 セッターに渡す値の型を a' と書き、 セッターが返す型を s' と書くことにすると、 セッターの型は s -> a' -> s' になる。 この設定のもと、 ゲッターとセッターの対の型は (s -> a, s -> a' -> s') とタプル型として実現される。 以降、 この型の値を素朴レンズと呼ぶことにする。

まずは、 素朴レンズを圏論的に定式化しよう。 これは単純に次のようにすれば良い。 なお、 上記の s, s', a, a' に対応する変数名としてそれぞれ S, 󰔄S, A, 󰔄A を用いる。

定義 1.1.

有限積をもつ圏 󰒚 をとる。 対象 S,󰔄S,A,󰔄A に対し、 2 つの射 g:S→A と p:S×󰔄A→󰔄S から成る組 (g,p) を素朴レンズ (naive lens) と呼び、 (g,p):(S,󰔄S)󰔊→(A,󰔄A) で表す。

素朴レンズを合成することで、 階層的により深い位置にある値を操作する新たな素朴レンズを得ることができた。 このページでは、 この演算を @. という名前で定義している。 圏論的には、 この演算は次のように定式化できる。

定義 1.2.

有限積をもつ圏 󰒚 をとる。 素朴レンズ (g,p):(S,󰔄S)󰔊→(A,󰔄A), (g󰎘,p󰎘):(A,󰔄A)󰔊→(󰔄B,B) に対し、 g󰎙 := ❲SA󰔄Bgg󰎘❲ p󰎙 := ❲S×BS×S×BS×A×BS×󰔄A󰔄SdiagS×idid×g×idid×p󰎘p❲ と定める。 なお、 図式中の diagS:S→S×S は対角射である。 これによって得られる素朴レンズ (g󰎙,p󰎙):(S,󰔄S)󰔊→(󰔄B,B) を (g,p) と (g󰎘,p󰎘) の合成 (composition) という。

この合成によって、 素朴レンズを射とする圏が定義できる。

定義 1.3.

有限積をもつ圏 󰒚 をとる。 圏 NLens(󰒚) を、

によって定義する。

さて、 Haskell の lens パッケージにおけるレンズの型は、 上記のような素朴な (s -> a, s -> a' -> s') ではなく、 forall f. Functor f => (a -> f a') -> (s -> f s') という一見不思議な形になっている。 このページでは、 一方の型の値からもう一方の型の値を作ることができ、 さらにその構成が互いに逆になっていることを観察して、 この 2 つの型が等価であることを述べた。 ここでは、 圏論的にこの 2 つの型の等価性を示そう。 そのためには、 後者の型を圏論的に定式化する必要がある。

型 forall f. Functor f => (a -> f a') -> (s -> f s') の値とはすなわち、 関手 f で添字付けられた (a -> f a') -> (s -> f s') という型の関数の族である。 これを素朴に捉えれば、 圏 󰒚 上の自己関手 F:󰒚→󰒚 で添字付けられた写像 φF:Hom(A,F󰔄A)→Hom(S,F󰔄S) の族 (φF)F が圏論的定式化であろうと思いつく。 しかし、 F に対して φF がバラバラに存在するというのは圏論的に不自然なので、 F に関して φF が自然であることを課すのは理に適っているだろう。 すなわち、 Hom(A,-󰔄A) と Hom(S,-󰔄S) を関手 End(󰒚)→Set と見なして、 自然変換 φ:Hom(A,-󰔄A)⇒Hom(S,-󰔄S) を考えるということである。

残念ながら、 自然変換 φ:Hom(A,-󰔄A)⇒Hom(S,-󰔄S) と素朴レンズ (g,p):(S,󰔄S)󰔊→(A,󰔄A) は 1 対 1 に対応しない。 この原因は、 素朴レンズから上記の自然変換を作ろうとしたときに、 自然変換の添字として使われている F の関手性だけでは構造が足りないためである。 そこで、 自然変換の添字として自己関手に追加の構造を加えたものを考える必要性が出てくるが、 その構造として次で定義する強度という概念が適切であることが知られている。

定義 1.4.

有限積をもつ圏 󰒚 上の自己関手 F:󰒚→󰒚 をとる。 対象 M,󰔄X に対し、 全ての変数に関して自然な射 σM󰔄X:M×F󰔄X⟶F(M×󰔄X) が定まっていて、 任意の対象 M,N,󰔄X に対し、 図式 (M×N)×F󰔄XF((M×N)×󰔄X)M×(N×F󰔄X)M×F(N×󰔄X)F(M×(N×󰔄X))σM×N,󰔄Xid×σN󰔄XσM,N×󰔄X F󰔄X1×F󰔄XF(1×󰔄X)σ1󰔄X が全て可換であるとする。 なお、 ラベルのない射は標準的な同型射を表している。 このとき、 σ を F に対する強度 (strength) といい、 組 (F,σ) を自己強関手 (strong endofunctor) という。

強関手の間の射としては、 次のような強度と適合する自然変換を考える。

定義 1.5.

有限積をもつ圏 󰒚 上の自己強関手 (F,σ),(G,τ):󰒚→󰒚 および自然変換 θ:F⇒G をとる。 任意の対象 M,󰔄X に対し、 M×F󰔄XM×G󰔄XF(M×󰔄X)G(M×󰔄X)id×θ󰔄XθM×󰔄XσM󰔄XτM󰔄X が可換であるとき、 θ を強自然変換 (strong natural transformation) といい、 θ:(F,σ)⇒(G,τ) で表す。

定義から強自然変換は合成に関して閉じていることがすぐに分かるので、 強関手と強自然変換は圏を成す。

定義 1.6.

有限積をもつ圏 󰒚 をとる。 圏 StrEnd(󰒚) を、

によって定義する。

さて、 我々の目的は、 素朴レンズ (g,p):(S,󰔄S)󰔊→(A,󰔄A) と 1 対 1 に対応するような自然変換 φ:Hom(A,-󰔄A)⇒Hom(S,-󰔄S) を得ることであった。 Hom(A,-󰔄A) と Hom(S,-󰔄S) を End(󰒚) からの関手だと見るとこれはうまくいかないが、 StrEnd(󰒚) からの関手だと見ると実はうまくいく。 このように見なした自然変換 φ:Hom(A,-󰔄A)⇒Hom(S,-󰔄S) を、 このエンコーディング方法を考案した人の名前を借りて、 van Laarhoven レンズと呼ぶことにしよう。

定義 1.7.

有限積をもつ圏 󰒚 をとる。 対象 A,󰔄A に対し、 Hom(A,-󰔄A): StrEnd(󰒚) ⟶ Set (F,σ) ⟼ Hom(A,F󰔄A) とおく。 このとき、 対象 S,󰔄S,A,󰔄A に対し、 自然変換 φ:Hom(A,-󰔄A)⇒Hom(S,-󰔄S) を van Laarhoven レンズ (— lens) という。

定義 1.8.

有限積をもつ圏 󰒚 をとる。 圏 LLens(󰒚) を、

によって定義する。

LLens(󰒚) の射としての向きと実体である自然変換としての向きが逆になっていることには注意すること。

では、 ここまでで定式化した 2 種類のレンズが等価であることを示そう。 すなわち、 有限積をもつ圏 󰒚 の任意の対象 S,󰔄S,A,󰔄A に対して、 全単射 HomLLens(󰒚)((S,󰔄S),(A,󰔄A))≅HomNLens(󰒚)((S,󰔄S),(A,󰔄A)) が存在することを示す。 直接この全単射を構成することもできるが、 van Laarhoven レンズの定義に出てくる Hom(A,-󰔄A):StrEnd(󰒚)→Set という形の関手には特別な性質があるので、 それを介して証明することにする。

定理 1.9.

カルテシアン閉圏 󰒚 をとる。 対象 A,󰔄A に対し、 関手 Hom(A,-󰔄A):StrEnd(󰒚)→Set は表現可能である。

証明.

Hom(A,-󰔄A):StrEnd(󰒚)→Set の表現対象を具体的に構成する。 まず、 EA󰔄A: 󰒚 ⟶ 󰒚 󰔄X ⟼ (󰔄A⇀󰔄X)×A とおく。 対象 M,󰔄X に対し、 積と冪の随伴の余単位を ev󰔄A󰔄X:(󰔄A⇀󰔄X)×󰔄A→󰔄X で書くことにし、 射 idM×ev󰔄A󰔄X:M×(󰔄A⇀󰔄X)×󰔄A⟶M×󰔄X を考える。 これを 󰔄A に関して転置すれば (idM×ev󰔄A󰔄X)♯:M×(󰔄A⇀󰔄X)⟶󰔄A⇀(M×󰔄X) が得られ、 さらに右から A との積をとると、 ρM󰔄XA󰔄A:M×(󰔄A⇀󰔄X)×A⟶(󰔄A⇀(M×󰔄X))×A が得られる。 すると、 これは M と 󰔄X の両方に関して自然であり、 さらに強度の公理を満たす。 したがって、 (EA󰔄A,ρA󰔄A) は自己強関手である。

この (EA󰔄A,ρA󰔄A) が実際に Hom(A,-󰔄A):StrEnd(󰒚)→Set の表現対象であること、 すなわち HomStrEnd(󰒚)((EA󰔄A,ρA󰔄A),-)≅Hom󰒚(A,-󰔄A)♡ が成り立つことを以下に示す。

自己強関手 (F,σ) を固定する。 任意の強自然変換 θ:(EA󰔄A,ρA󰔄A)⇒(F,σ) に対し、 id󰔄A:󰔄A→󰔄A の転置を jd󰔄A:1→󰔄A⇀󰔄A と書くことにして、 Φθ:=❲A1×A(󰔄A⇀󰔄A)×AF󰔄Ajd󰔄A×idθ󰔄A❲ とおくと、 これは写像 Φ: HomStrEnd(󰒚)((EA󰔄A,ρA󰔄A),(F,σ)) ⟶ Hom󰒚(A,F󰔄A) θ ⟼ Φθ を定める。

逆に、 射 f:A→F󰔄A および対象 󰔄X に対し、 (Ψf)󰔄X:=❲(󰔄A⇀󰔄X)×A(󰔄A⇀󰔄X)×F󰔄AF((󰔄A⇀󰔄X)×󰔄A)F󰔄Xid×fσ󰔄A⇀󰔄X,󰔄AFev󰔄A󰔄X❲ とおくと、 これは 󰔄X に関して自然なので、 自然変換 Ψf:EA󰔄A⇒F が得られる。 さらにこれは強自然変換 Ψf:(EA󰔄A,ρA󰔄A)⇒(F,σ) にもなっていることが確かめられる。 これにより、 写像 Ψ: Hom󰒚(A,F󰔄A) ⟶ HomStrEnd(󰒚)((EA󰔄A,ρA󰔄A),(F,σ)) f ⟼ Ψf が定まる。

Φ と Ψ は互いに逆になっており、 さらに自然でもあるので、 これより式 ♡ が得られた。

定理 1.10.

カルテシアン閉圏 󰒚 をとる。 対象 S,󰔄S,A,󰔄A に対し、 全単射 HomLLens(󰒚)((S,󰔄S),(A,󰔄A))≅HomNLens(󰒚)((S,󰔄S),(A,󰔄A)) が存在する。

証明.

定理 1.9 と Yoneda の補題により、 HomLLens(󰒚)((S,󰔄S),(A,󰔄A)) = Hom[StrEnd(󰒚),Set](Hom(A,-󰔄A),Hom(S,-󰔄S)) ≅ Hom[StrEnd(󰒚),Set](Hom((EA󰔄A,ρA󰔄A),-),Hom(S,-󰔄S)) ≅ Hom(S,EA󰔄A󰔄S)) ≅ Hom(S,(󰔄A⇀󰔄S)×A) ≅ Hom(S,󰔄A⇀󰔄S)×Hom(S,A) ≅ Hom(S×󰔄A,󰔄S)×Hom(S,A) = HomNLens(󰒚)((S,󰔄S),(A,󰔄A)) が成り立つので、 示された。

この射の間の全単射は圏同型を与えることも知られている。

定理 1.11.

カルテシアン閉圏 󰒚 をとる。 圏同型 LLens(󰒚)≅NLens(󰒚) が成立する。

証明.

定理 1.10 の全単射が合成を保つことを示せば良い。 単純に計算するだけなので、 ここでは詳細は省略する。

以上により、 ゲッターとセッターから成る素朴レンズと、 強関手で添字付けられた自然変換としての van Laarhoven レンズが、 互いに等価であることが示せた。 後者の自然変換としてのレンズは、 以前述べたように Haskell で用いられているレンズのエンコーディング方法である。 レンズにはプロ関手を用いた別のエンコーディング方法もあり、 これは Purecript のレンズライブラリで用いられている。 数学的には、 プロ関手を用いたエンコーディングの方が見通しが良く計算もしやすいという利点があり、 こちらの方がより深く研究されているようである。 次回は、 このプロ関手を用いたエンコーディングについて触れる。

参考文献

  1. B. Clarke et al (2020) 「Profunctor optics, a categorical update」 arXiv:2001.07488
  2. M. Riley (2018) 「Categories of optics」 arXiv:1809.00738