As the topics says, I wish to understand the conceptual similarities and differences of lenses and bi-directional patterns. Similarities I can think of:
both give access to a part of the data
patterns let you bind part of the data to variables, which can be pattern-matched again, while van Laarhoven lenses provide that via function composition.
both concepts let you construct and de-construct data
lawful lenses have no pairing constructor Lens s a -> Lens s b -> Lens s (a,b) because the type does not guarantee that two lenses donāt overlap. Likewise, the bound variables in a pattern must be unique.
The obvious difference is that a lens is like a pattern that always matches, while general pattern matches can fail.
Quite concretely, constructors are bi-directional patterns and Control.Lens.TH can turn these into actual lenses. So can we say
āAll lenses are (possibly nested) bi-directional pattern matchesā?
Are you aware of prisms, which are a direct generalization of constructors in the lens world?
Since you mentioned complement lenses last time, while a lens is an isomorphism source <-> c āØÆ view, a prism is an isomorphism source <-> c + view.
Lenses and prisms are part of a larger hierarchy of ābidirectional stuffā called optics (see also Glassery). Lenses and prisms are both subsets of affine traversals, thatās another way to make sense of their similarities.
Thatās nice to know, but I am not after an over-arching optics concept, even if it can fit any pattern. Like last time, I wonder: what are the actual ways to define a lens, given the structure of a data type? In other words, given an algebra of type constructions (e.g. products, coproducts) is there an algebra of lens constructions that can describe any lens? For example:
{-# LANGUAGE GADTs #-}
data Lens s a where
IdLens :: Lens s s
-- ^ complement: ()
Assoc :: Lens s a -> Lens a b -> Lens s b
-- ^ complement: product of the complements
-- ((b,c),c') ~ (b,(c,c'))
Fst :: Lens s a -> Lens (s,c) a
Snd :: Lens s a -> Lens (c,s) a
Distr :: Lens s a -> Lens t a -> Lens (Either s t) a
-- ^ (a,c) + (a,c') ~ (a,c+c')
Null :: Lens Void a
We can therefore make an analogy: Lens s a is like the assertion a divides s for numbers. Each of the above constructors corresponds to a theorem about divisibility.
I have a hard time imagining[1] how this would represent reverse, which is an Iso and therefore also a Lens. You could add an ad-hoc algebra element for it, of course, but I think youād end up doing that for a lot of lenses.
Good point. Isos on recursive types are indeed very rich. The only way I can imagine is via a very general algebra element for fixed points, which can produce, among other things, unFix :: Fix f -> f (Fix f). Although I am entirely unfamiliar with it, Control.Lens.Plated.plate appears to be relevant.
Welp, I really got nerd-sniped here. But yes, thereās a data encoding of Isos that lets relationships like reverse be represented without ad-hoc support, and itās probably powerful enough to do most other provable isomorphisms. And once you have Iso, Lens is easy.
This journey started by looking at the definition of reverse:
We happen to know that reverse is its own inverse, but the goal here is to encode it as an Iso without that knowledge, by composing a finite set of elemental Isos, each of which are, by definition, mechanically invertible. At first glance, rev doesnāt look like a relationship that can be mechanically run in reverse. Its RHS expressions are not patterns that one could use to do an inverse matchāa is a match-everything pattern, and itās not clear what matching on rev would mean. Plus, thereās the recursion. It turns out, these two problems solve each other!
Letās abstract out the recursion. One way to do this is via a function like loop, which has type (a -> Either a b) -> a -> b. If the provided function returns a Left, loop iterates on that value; if it returns a Right, loop uses that as the result. We can rewrite rev with this like so:
reverse l = loop rev (l, [])
where
rev ([], a) = Right a
rev (x:xs, a) = Left (xs, x:a)
That is already starting to look more invertible, isnāt it! But now the problem is imagining how to invert loop. Running loop in reverse would look like accepting a b, wrapping it in Right, sending it backwards through the provided function, and getting an a out. Are we done? Or should we wrap that a in a Left and send it through again? Thereās not enough information to know.
No worries; just do the same Either trick again, but on the other side of the function. We can write an invertible loop like this:
loop :: (Either a b -> Either a c) -> b -> c
loop f = go . Right
where
go x = case f x of
Left a -> go (Left a)
Right c -> c
An intuition driver for the visually-minded: Imagine a segment of ribbon with non-uniform width. One end of the ribbon is divided between segments of length a and b, and the other end is divided between segments of length c and a. If this ribbon represents an invertible function, loop represents the action of curling the ribbon up and gluing the a segments together, resulting in a shape with an open b end and an open c end, representing an invertible function from b to c.
The idea here is that b (in the forward direction) or c (in the reverse direction) start out wrapped in Right, and then passed to the inner function. If the result of the inner function is Left, loop sends it back through in the same direction. If itās Right, loop unwraps and returns it. The logic is the same in either direction, so the inverse of loop f is simply loop of the inverse of f.
We can rewrite reverse again to use this loop, and the result is quite clean:
reverse :: [a] -> [a]
reverse = loop $ \case
Right a -> Left (a, [])
Left (x:xs, a) -> Left (xs, x:a)
Left ([], a) -> Right a
Now this looks like something we could make from Isos! Itās basically an exercise in sum/product gymnastics, with some appropriate encoding of lists, and with an Iso corresponding to loop (which is a nicely generic piece of equipment, plausibly powerful enough to represent any recursive function that can be proven to be invertible using the isomorphism axioms Iāll be laying out shortly).
Iām going to switch to writing ārealā code now. Letās start with an interface class for isomorphisms. This isnāt strictly necessary as an abstraction for this post, but it would make it easier to experiment with alternate representations, and perhaps more importantly, it lets me write a bunch of helper methods in a uniform way so that they look the same as the constructors of the Iso type.
-- Isomorphisms form a category: they have an identity
-- and associative composition.
class Category iso => Isomorphism iso where
-- They are, perhaps most importantly, invertible.
symm :: b `iso` a -> a `iso` b
-- They can be executed forwards and backwards.
fwd :: a `iso` b -> a -> b
rev :: a `iso` b -> b -> a
rev i = fwd (symm i)
-- Up to isomorphism, sums and products form an
-- abelian semiring.
-- Abelian monoid axioms for sums:
swapS :: Either b a `iso` Either a b
assocS :: Either a (Either b c) `iso` Either (Either a b) c
nullL :: a `iso` Either Void a
nullR :: a `iso` Either a Void
nullR = nullL >>> swapS
-- Abelian monoid axioms for products:
swapP :: (b, a) `iso` (a, b)
assocP :: (a, (b, c)) `iso` ((a, b), c)
unitL :: a `iso` ((), a)
unitR :: a `iso` (a, ())
unitR = unitL >>> swapP
-- Rounding out the semiring with distributivity...
factorL :: Either (a, b) (a, c) `iso` (a, Either b c)
factorR :: Either (a, c) (b, c) `iso` (Either a b, c)
factorR = biS swapP swapP >>> factorL >>> swapP
-- ...and absorption.
absorbL :: (Void, a) `iso` Void
absorbR :: (a, Void) `iso` Void
absorbR = swapP >>> absorbL
-- We also want strength with respect to sums...
left' :: a `iso` b -> Either a c `iso` Either b c
right' :: b `iso` c -> Either a b `iso` Either a c
right' i = swapS >>> left' i >>> swapS
biS :: a `iso` c -> b `iso` d -> Either a b `iso` Either c d
biS i j = left' i >>> right' j
-- ... and products.
first' :: a `iso` b -> (a, c) `iso` (b, c)
second' :: b `iso` c -> (a, b) `iso` (a, c)
second' i = swapP >>> first' i >>> swapP
biP :: a `iso` c -> b `iso` d -> (a, b) `iso` (c, d)
biP i j = first' i >>> second' j
-- Finally, two special guests. `loop'` encodes iterative
-- isomorphisms, using the logic discussed above.
loop' :: Either c a `iso` Either c b -> a `iso` b
-- And `inspect` uses generics to convert arbitrary data
-- types into sums of products. The implementation of
-- the `Encode` class is largely a distraction; I'll include
-- it in the appendix, but just consider this to be an
-- element that papers over the distinction between
-- `[a]` and `Either () (a, [a])`.
inspect :: Encode a b => a `iso` b
This is not 100% completeāI know I omitted anything involving exponentials, and possibly there are a few other axioms it would be important to have, but I donāt expect that the omissions will change the flavor of the thing much.
We could define a type that implements this class, but letās skip ahead to the good stuff and define reverse as an isomorphism.
The process of bashing out an isomorphism using this interface reminds me of nothing so much as writing a proof in Agda, but weāre not doing anything fancy with types. Itās essentially just an especially fussy point-free translation of our last definition of reverse, which I will repeat as needed for reference:
reverse :: [a] -> [a]
reverse = loop $ \case
Right a -> Left (a, [])
Left (x:xs, a) -> Left (xs, x:a)
Left ([], a) -> Right a
The obvious place to start the translation is with a loop':
We know from reverse that c0, the intermediate state of the iterative function, is ([a], [a]). Spelling out the type that we want to use to fill this hole will save us some effort later:
reverseI :: forall iso a. Isomorphism iso => [a] `iso` [a]
reverseI = loop' inner
where
inner :: Either ([a], [a]) [a] `iso` Either ([a], [a]) [a]
inner = _
Now, the only way for us to do āpattern matchingā with these isomorphism combinators is to turn everything we want to match into Either and throw axioms at it to move the Eithers around. Using the isomorphism [a] ā Either () (a, [a]), letās convert the patterns inside reverse:
Right a -> Left (a, Left ())
Left (Right (x, xs), a) -> Left (xs, Right (x, a))
Left (Left (), a) -> Right a
This is a close match for an assocS. The forward implementation of assocS will necessarily look like this:
Left a -> Left (Left a)
Right (Left b) -> Left (Right b)
Right (Right c) -> Right c
If we swapS both the outer and the inner sums in the LHS of the reverse clauses, we can get roughly this form. (There are some products that will need to be factored through, but ignore that for the moment.)
Using inspect to represent turning lists into sums, what weāve worked out so far is this:
reverseI :: forall iso a. Isomorphism iso => [a] `iso` [a]
reverseI = loop' inner
where
inner :: Either ([a], [a]) [a] `iso` Either ([a], [a]) [a]
inner =
left' (first' (inspect >>> swapS)) >>> swapS
>>> _
>>> left' (second' (symm inspect))
Now the hole needs to represent this:
Left a -> Left (a, Left ())
Right (Left (x, xs), a) -> Left (xs, Right (x, a))
Right (Right (), a) -> Right a
We can bring the LHS closer to assocS by distributing the second tuple element inside the Right patterns. Likewise, we can bring the RHS closer by distributing the first tuple element inside the Left patterns.
reverseI :: forall iso a. Isomorphism iso => [a] `iso` [a]
reverseI = loop' inner
where
inner :: Either ([a], [a]) [a] `iso` Either ([a], [a]) [a]
inner =
left' (first' (inspect >>> swapS)) >>> swapS
>>> right' (symm factorR)
>>> _
>>> left' (factorL >>> second' (symm inspect))
This can be simplified by pulling the symm factorR back through the swapS and merging it with the left' that precedes it.
reverseI :: forall iso a. Isomorphism iso => [a] `iso` [a]
reverseI = loop' inner
where
inner :: Either ([a], [a]) [a] `iso` Either ([a], [a]) [a]
inner =
left' (first' (inspect >>> swapS) >>> symm factorR) >>> swapS
>>> _
>>> left' (factorL >>> second' (symm inspect))
There are a few superfluous units to squash:
reverseI :: forall iso a. Isomorphism iso => [a] `iso` [a]
reverseI = loop' inner
where
inner :: Either ([a], [a]) [a] `iso` Either ([a], [a]) [a]
inner =
left' (first' (inspect >>> swapS) >>> symm factorR >>> right' (symm unitL)) >>> swapS
>>> _
>>> left' (left' unitR >>> factorL >>> second' (symm inspect))
This hole now needs to represent this:
Left a -> Left (Left a)
Right (Left ((x, xs), a)) -> Left (Right (xs, (x, a)))
Right (Right a) -> Right a
This is almost a perfect match for assocS, except for the rearrangement of ((x, xs), a) to (xs, (x, a)). Thatās just first' swapP >>> symm assocP, and so we can complete the definition with:
This is not code Iād want to meet at night in a dark alley without a type checker. I wrote out this long, boring explanation because I canāt expect a lot of people to follow even a heavily commented version of this definition if it appeared as a fait accompliāI doubt I could if I hadnāt worked through it myself. But it does demonstrate that our isomorphism vocabulary is sufficient to define this operation. Letās concretize and run a demo:
data Iso a b where
IsoId :: Iso a a
IsoComp :: Iso b c -> Iso a b -> Iso a c
IsoSymm :: Iso a b -> Iso b a
IsoSwapS :: Iso (Either a b) (Either b a)
IsoAssocS :: Iso (Either a (Either b c)) (Either (Either a b) c)
IsoNullL :: Iso a (Either Void a)
IsoSwapP :: Iso (a, b) (b, a)
IsoAssocP :: Iso (a, (b, c)) ((a, b), c)
IsoUnitL :: Iso a ((), a)
IsoFactorL :: Iso (Either (a, b) (a, c)) (a, Either b c)
IsoAbsorbL :: Iso (Void, a) Void
IsoLeft :: Iso a b -> Iso (Either a c) (Either b c)
IsoFirst :: Iso a b -> Iso (a, c) (b, c)
IsoLoop :: Iso (Either a b) (Either a c) -> Iso b c
IsoInspect :: Encode a b => Iso a b
instance Category Iso where
id = IsoId
(.) = IsoComp
instance Isomorphism Iso where
symm = IsoSymm
swapS = IsoSwapS
assocS = IsoAssocS
nullL = IsoNullL
swapP = IsoSwapP
assocP = IsoAssocP
unitL = IsoUnitL
factorL = IsoFactorL
absorbL = IsoAbsorbL
left' = IsoLeft
first' = IsoFirst
loop' = IsoLoop
inspect = IsoInspect
fwd = \case
IsoId -> id
IsoComp i j -> fwd i . fwd j
IsoSymm i -> rev i
IsoSwapS -> swapEither
IsoAssocS -> \case
Left a -> Left (Left a)
Right (Left b) -> Left (Right b)
Right (Right c) -> Right c
IsoNullL -> Right
IsoSwapP -> swap
IsoAssocP -> \(a, (b, c)) -> ((a, b), c)
IsoUnitL -> ((), )
IsoFactorL -> \case
Left (a, b) -> (a, Left b)
Right (a, c) -> (a, Right c)
IsoAbsorbL -> fst
IsoLeft i -> first (fwd i)
IsoFirst i -> first (fwd i)
IsoLoop i -> loop (fwd i)
IsoInspect -> encode
rev = \case
IsoId -> id
IsoComp i j -> rev j . rev i
IsoSymm i -> fwd i
IsoSwapS -> swapEither
IsoAssocS -> \case
Left (Left a) -> Left a
Left (Right b) -> Right (Left b)
Right c -> Right (Right c)
IsoNullL -> either absurd id
IsoSwapP -> swap
IsoAssocP -> \((a, b), c) -> (a, (b, c))
IsoUnitL -> snd
IsoFactorL -> \case
(a, Left b) -> Left (a, b)
(a, Right c) -> Right (a, c)
IsoAbsorbL -> absurd
IsoLeft i -> first (rev i)
IsoFirst i -> first (rev i)
IsoLoop i -> loop (rev i)
IsoInspect -> decode
reverseIso :: Iso [a] [a]
reverseIso = reverseI
main :: IO ()
main = do
print $ fwd reverseIso [1..4]
print $ rev reverseIso [1..4]
So much for Isos. Of course, every Iso is a Lens. But one may wonder if we have to do even more vocabulary building to construct a Lens algebra. Good news: we donāt, because up to isomorphism, there is only one lens. Here it is:
data Lens s a = forall c. MkLens (Iso s (a, c))
Yes, our Iso algebra gives us a Lens algebra basically for free!
instance Category Lens where
id = MkLens unitR
MkLens i . MkLens j = MkLens (symm assocP . first' i . j)
get :: Lens s a -> s -> a
get (MkLens i) s = fst (fwd i s)
put :: Lens s a -> s -> a -> s
put (MkLens i) s a = rev i (a, snd (fwd i s))
lensVL :: Functor f => Lens s a -> (a -> f a) -> s -> f s
lensVL (MkLens i) f s = let (a, c) = fwd i s in rev i . (, c) <$> f a
lensFst :: Lens s a -> Lens (s, c) a
lensFst (MkLens i) = MkLens (first' i >>> symm assocP)
lensSnd :: Lens s a -> Lens (c, s) a
lensSnd (MkLens i) = MkLens (swapP >>> first' i >>> symm assocP)
lensDistr :: Lens s a -> Lens t a -> Lens (Either s t) a
lensDistr (MkLens i) (MkLens j) = MkLens (biS i j >>> factorL)
lensUnit :: Lens s ()
lensUnit = MkLens unitL
lensNull :: Lens Void a
lensNull = MkLens (symm absorbR)
It is easy to see that the one Lens satisfies all the lens laws as long as it contains a lawful Iso. Itās a little harder to seeāthough your previous exploration does a good job establishing thisāthat any Lens you could want is an isomorphism from the outer type to an (inner type, complement) pair. Helper functions like the above can put a nice interface on the Iso manipulation for Lens users (an interface that can expand indefinitely without adding any elements to the underlying algebra), but regardless of what happens under the hood, this shows that a complete Iso algebra is both necessary and sufficient for a complete Lens algebra.
Appendix: distracting helper code used by the above:
class Encode a b | a -> b where
encode :: a -> b
decode :: b -> a
instance (Generic a, GenericEncode (Rep a) b) => Encode a b where
encode = gencode . from
decode = to . gdecode
class GenericEncode a b | a -> b where
gencode :: a x -> b
gdecode :: b -> a x
instance GenericEncode content a => GenericEncode (M1 i c content) a where
gencode (M1 x) = gencode x
gdecode = M1 . gdecode
instance (GenericEncode l a, GenericEncode r b) => GenericEncode (l :+: r) (Either a b) where
gencode (L1 a) = Left (gencode a)
gencode (R1 b) = Right (gencode b)
gdecode = either (L1 . gdecode) (R1 . gdecode)
instance (GenericEncode l a, GenericEncode r b) => GenericEncode (l :*: r) (a, b) where
gencode (a :*: b) = (gencode a, gencode b)
gdecode (a, b) = gdecode a :*: gdecode b
instance GenericEncode (K1 c a) a where
gencode (K1 a) = a
gdecode = K1
instance GenericEncode U1 () where
gencode _ = ()
gdecode _ = U1
instance GenericEncode V1 Void where
gencode = \case {}
gdecode = absurd
This is so beautiful! I never imagined that casting the āis isomorphic toā into code would solve the problem.
Just for the record: The c is an existential type, right?
data Lens s a where
MkLens :: Iso s (a,c) -> Lens s a
This quite directly encodes the theorem: There is a lens from s to a if and only if there exists some type c and an isomorphism between s and (a,c).
Since my goal is to do all this on Generic representations, I would replace the IsoEncode with a constructor
IsoRep :: (Generic c, Rep c ~ f) => Iso c (f ())
So generic isomorphisms might look like this:
data GIso :: (Type -> Type) -> (Type -> Type) -> Type where
GIsoId :: GIso a a
GIsoComp :: GIso b c -> GIso a b -> GIso a c
GIsoSymm :: GIso a b -> GIso b a
GIsoSwapS :: GIso (a :+: b) (b :+: a)
GIsoAssocS :: GIso (a :+: (b :+: c)) ((a :+: b) :+: c)
GIsoNullL :: GIso a (V1 :+: a)
GIsoSwapP :: GIso (a :*: b) (b :*: a)
GIsoAssocP :: GIso (a :*: (b :*: c)) ((a :*: b) :*: c)
GIsoUnitL :: GIso a (U1 :*: a)
GIsoFactorL :: GIso ((a :*: b) :+: (a :*: c)) (a :*: (b :+: c))
GIsoAbsorbL :: GIso (V1 :*: a) V1
GIsoLeft :: GIso a b -> GIso (a :+: c) (b :+: c)
GIsoFirst :: GIso a b -> GIso (a :*: c) (b :*: c)
GIsoLoop :: GIso (a :+: b) (a :+: c) -> GIso b c
GIsoRec0 :: (Generic c, Rep c ~ f) => GIso (K1 R c) f
data GLens :: (Type -> Type) -> (Type -> Type) -> Type where
GLens :: GIso s (a :*: c) -> GLens s a
This is tremendously useful for me as a starting point for further explorations. Thanks!
You seem more interested in lenses than in other optics, but for posterity (and to make this post long enough for Discourse), Iāll note that we can also say, up to isomorphism, that there is only one prism and only one affine traversal.
data Prism s a where
MkPrism :: Iso s (Either a c) -> Prism s a
data AffineTraversal s a where
MkAffineTraversal :: Iso s (Either (a, c0) c1) -> AffineTraversal s a
I think optics outside of this diamond are harder to present in this format, which is one advantage of the profunctor/VL presentations over this one.
With your permission the GIso type will be incorporated into the refined-subtype project. Further I think one could factor out cartesian and co-cartesian category structure, which will help in implementing some of the Iso primitives.
I enjoy seeing nerding out like this.