Простая линза Haskell из учебника нарушает закон линз

Я читаю этот учебник:

http://blog.jakubarnold.cz/2014/08/06/lens-tutorial-stab-traversal-part-2.html

и мой код выглядит так:

import Control.Applicative
import Data.Traversable
import Control.Lens

data User = User String [Post] deriving Show
data Post = Post String deriving Show

posts :: Lens' User [Post]
posts f (User n p) = fmap (User n) (f p)

users :: [User]
users = [User "john" [Post "hello", Post "world"], User "bob" [Post "foobar"]]

tp :: (Traversable t, Applicative f) => ([Post] -> f [Post]) -> t User -> f (t User)
tp = traverse . posts

Теперь, следуя сообщению в блоге, вот некоторые распространенные вычисления линз:

*Main> view tp users
[Post "hello",Post "world",Post "foobar"]

*Main> set tp [Post "x",Post "y"] users
[User "john" [Post "x",Post "y"],User "bob" [Post "x",Post "y"]]

*Main> view tp (set tp [Post "x",Post "y"] users)
[Post "x",Post "y",Post "x",Post "y"]

Последняя оценка привела меня в замешательство. Разве не должен выполняться следующий закон линз?

view l (set l v s) = v

(Закон взят с сайта http://artyom.me/lens-over-tea-2.)


person danpomaro    schedule 25.12.2015    source источник


Ответы (1)


Это закон линзы, а tp — это обход, поэтому он не обязан подчиняться этому закону.

Строго говоря, view вообще не должен работать с обходами (он и так работает, но делает это путем моноидального объединения собранных результатов).

person Artyom    schedule 25.12.2015
comment
Итак, если я понимаю, о чем вы говорите, если a и b линзы, то и a . b тоже. Но traverse . a уже не линза, а обход. Есть ли какой-либо другой способ создания обходов композицией? Если c и d обходы, то c . d тоже обход? - person danpomaro; 25.12.2015
comment
@danpomaro Ага. lens + lens = объектив; lens + traversal = traversal + lens = traversal + traversal = обход. - person Artyom; 25.12.2015
comment
@danpomaro документация по линзам включает диаграмму с подробностями; составлять вещи из двух синих ящиков, и вы получаете что-то из любого синего ящика, к которому они оба имеют путь. - person Daniel Wagner; 26.12.2015