generated at
【WIP】ゼロから作るLens(和訳)

Lens は狂った型シグネチャを持つという多くの欠点がある.これは,基礎からこのトチ狂ったシグネチャを目まぐるしく導出する文書である.さらなる lens のコードの探求と洗練された型を「通して」理解するための出発点として有用であるかもしれない.

GettingとSetting

最も簡単に言うと, Lens はオブジェクト指向言語のgetterとsetterによく似たgetterとsetterである.これまでにこれらを見たことがない人は,純粋な言語における"get"と"set"が何を意味するのか疑問に思うかもしれない.

Haskellでは,getとsetとは,「大きい」構造とそれのいくつか「小さい」部分との関係を指す.例えば,タプルが与えられた場合,その左側をgetやsetしたいだろう.

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"が合わさったものである.最も理解しやすい実装はそれらをタプルにすることである.

lens2.hs
data Lens a b = Lens { get :: a -> b , set :: b -> a -> a }

そして,確かにこれは,後に出てくるより賢い派生と共通の性質を大体持っている,申し分なく妥当な Lens である.いくつかの「より大きい」ものの中の「より小さい」部分に焦点を絞って,前述と同じようにフィールドセレクタの get l set l を使ってlens l を作成する.

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を合わせて作ることもできる.

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の合成の魔法の一部は,この面倒なボイラープレートのすべてを完全に葬り去ってしまうということである.

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"はどちらも大きい部分を引数として取る.例えば,それらの関数適用を組み合わせて「タプルから引数を抽出する」ということができる.

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. 実際,これらの部分を元に戻すと,元のオブジェクトに戻る.

lens7.hs
lensToId :: Lens a b -> (a -> a) lensToId f = \a -> let (piece, hole) = f a in hole piece

今後も繰り返し表れる,構造をかけらとそれらの部分が収まる穴に分割するという考え方はもう早速重要である.しかし,その分割を行うプロセス a -> (b, b -> a) とその結果 (b, b -> a) 自体は,どちらも驚くほど豊かな構造を持つ.

その構造が何を「意味する」かについての詳細に立ち入ること無く,それらを説明しよう.はじめに,そのペアはしばしばストアと呼ばれる......

lens8.hs
data Store b a = Store b (b -> a)

関手
言うまでもないことだが, (b, b -> a) (->) e がReaderモナドとするのと全く同じ方法で Functor をなす.

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) の操作から定義される.あるいは,さらに対応を理解させるために下図を見てみよう.

lens10
| Monad a -> m a m (m a) -> m a | Comonad w a -> a w a -> w (w a)
Store b Comonad を形成していることがわかる.

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 を使うことができる.

lens12
> unfoldr (\n -> if (n == 0) then Nothing else Just (n, n-1)) 10 [10,9,8,7,6,5,4,3,2,1]

unfoldr go だけを見れば,それが a -> [a] のような型,「注入」関数を持っているのがわかる. unfoldr go のようなものは,種となる値を値のリストに変換するもので,まさに Coalgebra と同じものである.結果の大きな構造が Functor である限り(そしてこれは実際には a -> f a Coalgebra たらしめる要件である), Coalgebra を繰り返し適用できるので,これらは再帰と密接に関係している.

lens13
> unfoldr go :: a -> [a] > 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 と呼ぶことが許される.

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 を使うとどのようになるだろうか?

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 を形成するという考え方をより明瞭に表している.

加えて,前にリンクしたRussell O'Connorのブログ記事を読むと,ここで本当に美しいことが起こっていることに気がつくだろう.

法則
我々のこれまでの直感は,Lensがどのように振る舞う「べき」かに対する確信に基づいているが,これをより具体的にすることができる.Lensの概念はCSの研究者によって長い間研究され,この直感を概説する一連の形式的な法則が確立された.それらはPierce's Laws of a "Very Well Behaved Lens"にある以下のものである:

1. 抽出したものを元に戻すものは何もしない
lens16
set s (get s) == s

2. setしたものを取り出すのは,setしたそのものがでてくる
lens17
get (set s v) == v

3. 繰り返すなんらかをsetした場合,最後にsetしたものが残る
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 を考えてみると,それらは完全に等価である.

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 を排除するようなものである.

Edward Kmett's discussion of Store Comonadic Cellular Automatamy followup exploration を読んでいるなら, experiment とよばれる Store 上の非常に興味深い演算を見たことがあるだろう.

lens20.hs
experiment :: Functor f => Store b a -> (b -> f b) -> f a experiment (Store part hole) inj = hole <$> inj part

Edwardが示唆したように,そして私がもっともっと深く探求しようとしたように, experiment Store をその「関数型」な形式に変換する.さらにこの変換は同型である.

lens21.hs
Store piece hole ~= experiment (Store piece hole) Store b a ~= (b -> f b) -> f a

完全を期すために,私が以前に guess と読んでいた他の同型も書いておこう.

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 がなんであるかを展開すると,以下のようになる.

lens23.hs
type Lens a b = Functor f => a -> (b -> f b) -> f a

ここで,とても混乱するが, fmap だけをつかってどんな型についても使えるようになる.

lens24.hs
_1 :: Lens (a, b) a _1 (a, b) inj = (,b) <$> inj a

Pretextの合成

Lensの力を示す典型的な例をもう一度見てみよう.この形式では,2つのLensがどのように構成されているかを考えるのはやや難しいが,なんとかなる.

lens25.hs
(>-) :: Lens a b -> Lens b c -> Lens a c (la >- lb) a = ...

待って!実際にはトリックがある.定義した Pretext lensの定義を並べ替えると,

lens26.hs
type Lens a b = Functor f => (b -> f b) -> (a -> f a)

そして,おそらく別の型名を作ると,

lens27.hs
type Coalg f x = x -> f x

結果として,これはもっと単純な型として見ることができる.

lens28.hs
type Lens a b = Functor f => Coalg f b -> Coalg f a

そして実際に我々はすぐに基本的な関数合成を使った合成を持っている!

lens29.hs
(>-) :: Lens a b -> Lens b c -> Lens a c la >- lb = la . lb

最後に,これはまさに lens ライブラリで見ることができる Lens の型である.この拡張された形式では,通常の関数合成 (.) だけをつかってlensを合成することができ,あなたのコードの中の型にlensを書くための外部の依存化関係を必要としない. fmap だけがあればよいのである.

この形式化はやや異なる方向から生まれたものであるが, Twan van Laarhoven によって"CPS Functional Reference" という名前で最初に発見されたことは注目に値する.

ちょっと待って,s-t-a-bって何?

lens を多用したことがあるなら,私が先程playしたちょっとしたトリックに気がついただろう.私は Simple Lens として知られる Lens をどのように定義するかに悩まされただけである.この記事全体では,2パラメータlensに焦点を絞ってきたが,ライブラリのlensは4パラメータlensである.この余計な複雑さはどこから来るのだろうか?

さて,これらのlensの1つを書いてみよう.私はずっと同じ例を選ぶ.

lens30.hs
_1 :: Lens (a,b) a _1 inj (a, b) = (,b) <$> inj a

これは,2つのパラメータだけで意味があるように思えるかなり厳密な定義である.しかし,型シグネチャの行を忘れてGHCiにこれを推論させるとどうなるかを見てみよう.

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.
この余分な自由は,getterとsetterに関する非常に強力ななにかを示唆している.settingは全体の型を変える能力を持っているのだ!常にそうでないということも,全くそうでないというこもあるが,先に定義した Lens の型はその可能性を考慮から消してしまう.

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.

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 Monad s as arising from the composition of two Functor s which share a special relationship known as "adjunction". For the Store monad, they are as follows
lens33
(b, b -> a) == (b, _) . (b -> _) $ a
If we reverse the order of these functions, we end up with State directly.
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".