【WIP】ゼロから作るLens(和訳)
Lensは狂った型シグネチャを持つという多くの欠点がある.これは,基礎からこのトチ狂ったシグネチャを目まぐるしく導出する文書である.さらなるlensのコードの探求と洗練された型を「通して」理解するための出発点として有用であるかもしれない.
GettingとSetting
最も簡単に言うと,Lensはオブジェクト指向言語のgetterとsetterによく似たgetterとsetterである.これまでにこれらを見たことがない人は,純粋な言語における"get"と"set"が何を意味するのか疑問に思うかもしれない.
Haskellでは,getとsetとは,「大きい」構造とそれのいくつか「小さい」部分との関係を指す.例えば,タプルが与えられた場合,その左側をgetやsetしたいだろう.
code:lens1.hs
get :: (a, b) -> a
get (part, _) = part
set :: a' -> (a, b) -> (a', b)
set part (_, b) = (part, b)
この通り,getは抽出関数で,set xは「より小さな」構造によってパラメータ化された「より大きな」構造への変換である.
始まりのlens
Lensは常に単なる"getter"と"setter"が合わさったものである.最も理解しやすい実装はそれらをタプルにすることである.
code: lens2.hs
data Lens a b
= Lens { get :: a -> b
, set :: b -> a -> a
}
そして,確かにこれは,後に出てくるより賢い派生と共通の性質を大体持っている,申し分なく妥当なLensである.いくつかの「より大きい」ものの中の「より小さい」部分に焦点を絞って,前述と同じようにフィールドセレクタのget lとset lを使ってlens lを作成する.
code:lens3.hs
-- | A *Lens* that focuses on the first element in a tuple.
_1 :: Lens (a, b) a
_1 = Lens (\(part, _) -> part) (\part (_, b) -> (part, b))
:t get _1
get _1 :: (a, b) -> a
:t set _1
set _1 :: a -> (a, b) -> (a, b)
細心の注意を払っていれば,このLensの"setter"は実際に我々が最初の節で書いたものよりわずかに力が弱いことに気づくだろう.これは後で再検討し,修正する.
合成
Lensが提供したのがこれだけであったならそれほど重要ではないかもしれないが,それらをつないで「より大きな」オブジェクトの内側に焦点を絞るlensを,沢山の単純なlensを合わせて作ることもできる.
code: lens4.hs
-- | Lens composition
(>-) :: Lens a b -> Lens b c -> Lens a c
la >- lb = Lens (get lb . get la) $ \part whole ->
set la (set lb part (get la whole)) whole
setterは少しごちゃごちゃしているが,大(a),中(b),小(c)の部分があると考えれば,以下のようなプロセスになる.元の大きな部分と新しい小さな部分が与えられていて,
1. 元の大きな部分から元の中くらいの部分を得る
2. 中くらいの部分を新しい小さな部分に更新する
3. 新しい中くらいな部分で小さい部分を更新する
これは面倒だが,それほど難しいことではない.lensの合成の魔法の一部は,この面倒なボイラープレートのすべてを完全に葬り去ってしまうということである.
code: lens5
:t _1 >- _1 >- _1 >- _1 >- _1 -- useless, but if you didn't have pattern matching
-- this would be very challenging to code
-- ... we don't always have pattern matching,
-- but can always have lenses
_1 >- _1 >- _1 >- _1 >- _1 :: Lens (((((c, b4), b3), b2), b1), b) c
ストアの生成
以上のlensは,完全に機能しているが,これまでに利用してない数学的構造がまだ沢山lensにはある.例えば,"getter"と"setter"はどちらも大きい部分を引数として取る.例えば,それらの関数適用を組み合わせて「タプルから引数を抽出する」ということができる.
code: lens6.hs
type Lens a b = (a -> b, b -> a -> a) -- same as before
type Lens a b = (a -> b, a -> b -> a) -- flip the setter
type Lens a b = a -> (b, b -> a) -- pull the parameter out
この変更を導くための直感は,今やLensは大きな構造を取り,(1)大きな構造の内側にある小さな部分と(2)元の構造の「穴が空いた」バージョンの2つのものを返す関数であるということである.---it demands a small piece like the one it gave us in order to restore the original large structure. 実際,これらの部分を元に戻すと,元のオブジェクトに戻る.
code:lens7.hs
lensToId :: Lens a b -> (a -> a)
lensToId f = \a -> let (piece, hole) = f a in hole piece
その構造が何を「意味する」かについての詳細に立ち入ること無く,それらを説明しよう.はじめに,そのペアはしばしばストアと呼ばれる......
code: lens8.hs
data Store b a = Store b (b -> a)
関手
言うまでもないことだが,(b, b -> a)は(->) eがReaderモナドとするのと全く同じ方法でFunctorをなす.
code: lens9.hs
instance Functor (Store b) where
fmap f (Store piece hole) = Store piece (f . hole)
余モナド
何も手を加えなくても,ComonadはMonadの逆と考えることができる.Monadのmはjoin :: m (m a) -> m aとreturn :: a -> m aの操作から定義される.Comonad(しばしばwとして表記される as a visual pun)は,extract :: w a -> aとduplicate :: w a -> w (w a)の操作から定義される.あるいは,さらに対応を理解させるために下図を見てみよう.
code: lens10
| Monad a -> m a m (m a) -> m a
| Comonad w a -> a w a -> w (w a)
Store bはComonadを形成していることがわかる.
code: lens11.hs
instance Comonad (Store b) where
extract (Store piece hole) = hole piece -- this is the second part of lensToId!
duplicate (Store piece hole) =
Store piece (\newPiece -> Store newPiece hole)
余代数
最後の興味深い構造Coalgebraである.これは「種(シード値)」をもっと構造のあるものに変えるためのunfoldrの一般化である.例えば,整数からカウントダウンするリストを生成するためにunfoldrを使うことができる.
code: lens12
unfoldr (\n -> if (n == 0) then Nothing else Just (n, n-1)) 10
unfoldr goだけを見れば,それがa -> [a]のような型,「注入」関数を持っているのがわかる.unfoldr goのようなものは,種となる値を値のリストに変換するもので,まさにCoalgebraと同じものである.結果の大きな構造がFunctorである限り(そしてこれは実際にはa -> f aをCoalgebraたらしめる要件である),Coalgebraを繰り返し適用できるので,これらは再帰と密接に関係している.
code:lens13
fmap (unfoldr go) . unfoldr go :: a -> a -- this is like "duplicate"
fmap (fmap (unfoldr go)) . fmap (unfoldr go) . unfoldr go :: a -> a -- and duplicate again! このとおり,at this point Lens a b = a -> Store b aを呼び出していて,Store bはFunctorであるので,LensをCoalgebraと呼ぶことが許される.
code: lens14.hs
type Coalg f a = a -> f a
type Lens a b = Coalg (Store b) a -- (thanks to Austin Seipp for pointing this out)
これは,まとめて言えば,「Lensは余状態余モナド余代数である」という魅力的で斜め上の概念につながる[1]. 何をもたらしたのか?
さて,これで自明な"getterとsetterのペアという構造"から1つの引数だけを引き出すこのかなり小さなトリックが,lensの中に隠されていた構造を大量にさらけ出すことがわかったが,果たしてそれはlensをより強力にしてくれたり,直感をより明確にしてくれたりするのか?
さて, Store Comonadのことを,「全体」を2つの部分に分けた,「かけら」と「穴」を持っていると考えることは新たな洞察を与えてくれたのかもしれないが,わざわざこれほど専門用語を使う価値はあったのか?
(訳注:原文は"as given new insight" としているが,"has given new insight"のtypoだと判断した.)
多くの進歩が感じられる一つの例は合成演算子(>-)を書くときである.以前は書くのはそれほど難しくはなかったが,組み合わさった"setter"を書くには少しばかり頭の体操が要求された.それはStore Comonadを使うとどのようになるだろうか?
code: lens15.hs
(>-) :: Lens a b -> Lens b c -> Lens a c
(la >- lb) a = let Store partB holeBA = la a
Store partC holeCB = lb partB
holeCA = holeBA . holeCB
in Store partC holeCA
実際には,availableな型を考えると,この関数はほとんどそれ自身を書いている自明なことを書いているという意味か?.それはまた,型aを2つの基礎となるかけらとそれらの穴(2つのStoreの層)に分割し,それらを縫い合わせることで合成されたStoreを形成するという考え方をより明瞭に表している. 法則
1. 抽出したものを元に戻すものは何もしない
code:lens16
set s (get s) == s
2. setしたものを取り出すのは,setしたそのものがでてくる
code: lens17
get (set s v) == v
3. 繰り返すなんらかをsetした場合,最後にsetしたものが残る
code: lens18
get (set (set s v1) v2) == v2
Hopefully "getting"と"setting"がなにを意味するかについてのこれまでの直感が,これらの法則と完全に一致していることがわかる.これらの法則は,"getting"と"setting"の全体的な振る舞いを捉えるように慎重に設計されている.
O'Connorが発見したのは,これらの法則,特にCSにとって実用的な概念の本質であると考えられるものは,任意の"Comonad Coalgebra"で成り立つことが知られている遥かに一般的な法則の具体例として導くことができるということである.特に,あるl :: Lens b a = a -> Store b aを考えてみると,それらは完全に等価である.
code: lens19.hs
extract . l == id -- injecting with the coalgebra then extracting the comonad is id
-- (this is just breaking our whole into the "piece" and "hole"
-- then jamming them back together)
fmap l . l == duplicate l -- duplicate is the same as "repeated coalgebra injection"
-- (see the comments in the Coalgebra section)
明らかにこれらの法則は "Well Behaved Lens Laws" よりも直感的ではないが,Comonad Coalgebraは可能な限りboringであるというとても形式的なものよりもはるかに多くはない.それらはまさに期待するように振る舞う.
And "Costate" Comonad Coalgebras [1] behave as boringly as possible, exactly as getters and setters.
更に推し進められるか?
これはすでに一般的だが,今日のlensの表現にはまだ達していない.最後のステップがある.
今,誰かがこの "Comonad Coalgebra" Lensと使うとすれば,それらのStoreデータ型のインスタンスが必要になるだろう.それはlensのようなインターフェイスを提供するすべてのライブラリへの依存関係として,このlensライブラリの周辺すべてを引きずり込むことを意味している.最悪の結果ではないが,この依存関係に対して「最小限の」インターフェイスを提供できると良い.これまでのすべての力を保ちながら,Storeを排除するようなものである.
code: lens20.hs
experiment :: Functor f => Store b a -> (b -> f b) -> f a
experiment (Store part hole) inj = hole <$> inj part
Edwardが示唆したように,そして私がもっともっと深く探求しようとしたように,experimentはStoreをその「関数型」な形式に変換する.さらにこの変換は同型である.
code: lens21.hs
Store piece hole ~= experiment (Store piece hole)
Store b a ~= (b -> f b) -> f a
完全を期すために,私が以前にguessと読んでいた他の同型も書いておこう.
code: lens22.hs
guess :: ( forall f . Functor f => (b -> f b) -> f a ) -> Store b a
guess m = m $ \piece -> Store piece id
ここで,Store が Functorであるという事実を使っている.
それは同型なので,Store b aか(forall f. Functor f => (b -> f b) -> f a)のどちらを使っても何も変わらない意訳.Storeでは見た目がずっと単純な型になるが,2番目の型(Pretxetとも呼ばれる)ではStoreデータ型を持ち運ぶ必要はなくなる. Pretextを使ったときのLens a bがなんであるかを展開すると,以下のようになる.
code: lens23.hs
type Lens a b = Functor f => a -> (b -> f b) -> f a
ここで,とても混乱するが,fmapだけをつかってどんな型についても使えるようになる.
code: lens24.hs
_1 :: Lens (a, b) a
_1 (a, b) inj = (,b) <$> inj a
Pretextの合成
Lensの力を示す典型的な例をもう一度見てみよう.この形式では,2つのLensがどのように構成されているかを考えるのはやや難しいが,なんとかなる.
code:lens25.hs
(>-) :: Lens a b -> Lens b c -> Lens a c
(la >- lb) a = ...
待って!実際にはトリックがある.定義したPretext lensの定義を並べ替えると,
code: lens26.hs
type Lens a b = Functor f => (b -> f b) -> (a -> f a)
そして,おそらく別の型名を作ると,
code: lens27.hs
type Coalg f x = x -> f x
結果として,これはもっと単純な型として見ることができる.
code:lens28.hs
type Lens a b = Functor f => Coalg f b -> Coalg f a
そして実際に我々はすぐに基本的な関数合成を使った合成を持っている!
code: lens29.hs
(>-) :: Lens a b -> Lens b c -> Lens a c
la >- lb = la . lb
最後に,これはまさにlensライブラリで見ることができるLensの型である.この拡張された形式では,通常の関数合成(.)だけをつかってlensを合成することができ,あなたのコードの中の型にlensを書くための外部の依存化関係を必要としない.fmapだけがあればよいのである.
ちょっと待って,s-t-a-bって何?
lensを多用したことがあるなら,私が先程playしたちょっとしたトリックに気がついただろう.私はSimple Lensとして知られるLensをどのように定義するかに悩まされただけである.この記事全体では,2パラメータlensに焦点を絞ってきたが,ライブラリのlensは4パラメータlensである.この余計な複雑さはどこから来るのだろうか?
さて,これらのlensの1つを書いてみよう.私はずっと同じ例を選ぶ.
code: lens30.hs
_1 :: Lens (a,b) a
_1 inj (a, b) = (,b) <$> inj a
これは,2つのパラメータだけで意味があるように思えるかなり厳密な定義である.しかし,型シグネチャの行を忘れてGHCiにこれを推論させるとどうなるかを見てみよう.
code: lens31
:t \inj (a, b) -> (,b) <$> inj a
\inj (a, b) -> (,b) <$> inj a
:: Functor f => (a -> f b) -> (a, t) -> f (b, t)
We can "sort of" interpret that type as a Pretext lens, except that we need a ~ b and (a, t) ~ (b, t), each implying the other.
This possibility is, in fact, the exact thing we enountered way back at the beginning of this article, write before the first "Composition" section.
We can fix it, though, by generalizing the type of our Lens to its final form that we know and love.
code:lens32.hs
type Lens s t a b = Functor f => (a -> f b) -> (s -> f t)
Quite obvious now isn't it? ;)
If this was an interesting read, I highly recommend Russell O'Connor's Functor is to Lens as Applicative is to Biplate which carries out this argument with much more elegance and generality while also making many more connections to related topics. He also proves the important steps which I'm simply omitting. (Thanks to aseipp, drb226, alen_ribic, heisenbug, Jameshfisher, mutjida, and tailbalance for comments and corrections.)
[1] It's a common gag, as evidenced by PL Borat there, to call Store lenses "Costate Comonad Coalgebras". Above I walked through where "Coalgebra" and "Comonad" come from, but left "Costate" alone. It turns out there is a relationship between Store and State though it's not truly "Co-" relationship.
The "Co-" terminology comes from category theory where "Co-X" means "X with all of the arrows turned around". Category theory tends to encode all interesting properties of all things in the arrows, so this is a very important notion. Thus all the more reason to be precise in how State and Store are actually related.
Again in whirlwind fashion, one can think of all Monads as arising from the composition of two Functors which share a special relationship known as "adjunction". For the Store monad, they are as follows
code: lens33
(b, b -> a) == (b, _) . (b -> _) $ a
If we reverse the order of these functions, we end up with State directly.
code:lens34
(b, b -> a) == (b, _) . (b -> _) $ a
(b -> _) . (b , _) $ a == (b -> (b, a))
and obviously visa versa. I don't know of a good name for "adjunction flipped cousins", which perhaps explains the longevity of the pithy, suggestive, but ultimately incorrect term "Costate Comonad".