In functional optics, a well-behaved prism (called a partial lens in scala, I believe) is supposed to have a set function of type 'subpart -> 'parent -> 'parent
, where if the prism "succeeds" and is structurally compatible with the 'parent
argument given, then it returns the 'parent
given with the appropriate subpart modified to have the 'subpart
value given. If the prism "fails" and is structurally incompatible with the 'parent
argument, then it returns the 'parent
given unmodified.
I'm wondering why the prism doesn't return a 'parent option
(Maybe
for Haskellers) to represent the pass/fail nature of the set function? Shouldn't the programmer be able to tell from the return type whether the set was "successful" or not?
I know there's been a lot of research and thought put into the realm of functional optics, so I'm sure there must be a definitive answer that I just can't seem to find.
(I'm from an F# background, so I apologize if the syntax I've used is a bit opaque for Haskell or Scala programmers).
I doubt there's one definitive answer, so I'll give you two here.
I believe prisms were first imagined (by Dan Doel, if my vague recollection is correct) as "co-lenses". Whereas a lens from s
to a
offers
get :: s -> a
set :: (s, a) -> s
a prism from s
to a
offers
coget :: a -> s
coset :: s -> Either s a
All the arrows are reversed, and the product, (,)
, is replaced by a coproduct, Either
. So a prism in the category of types and functions is a lens in the dual category.
For simple prisms, that s -> Either s a
seems a bit weird. Why would you want the original value back? But the lens
package also offers type-changing optics. So we end up with
get :: s -> a
set :: (s, b) -> t
coget :: a -> s
coset :: t -> Either s b
Suddenly what we're getting back in the non-matching case may actually be a bit different! What's that about? Here's an example:
cogetLeft :: a -> Either a x
cogetLeft = Left
cosetLeft :: Either b x -> Either (Either a x) b
cosetLeft (Left b) = Right b
cosetLeft (Right x) = Left (Right x)
In the second (non-matching) case, the value we get back is the same, but its type has been changed.
For both Van Laarhoven (as in lens
) and profunctor style frameworks, both lenses and prisms can also stand in for traversals. To do that, they need to have similar forms, and this design accomplishes that. leftaroundabout's answer gives more detail on this aspect.
To answer the “why” – lenses etc. are pretty rigidly derived from category theory, so this is actually quite clear-cut – the behaviour you describe just drops out of the maths, it's not something anybody defined for any purpose but follows from far more general ideas.
Ok, that's not really satisfying.
Not sure if other languages' type systems are powerful enough to express this, but in principle and in Haskell, a prism is a special case of a traversal. A traversal is a way to “visit” all occurences of “elements” within some “container”. The classical example is
mapM :: Monad m => (a -> m b) -> [a] -> m [b]
This is typically used like
Prelude> mapM print [1..4]
1
2
3
4
[(),(),(),()]
The focus here is on: sequencing the actions/side-effects, and gathering back the result in a container with the same structure as the one we started with.
What's special about a prism is simply that the containers are restricted to contain either one or zero elements† (whereas a general traversal can go over any number of elements). But the set
operator doesn't know about that because it's strictly more general. The nice thing is that you can therefore use this on a lens, or a prism, or on mapM
, and always get a sensible behaviour. But it's not the behaviour of “insert exactly once into the structure or else tell me if it failed”.
Not that this isn't a sensible operation, just it's not what lens libraries call “setting”. You can do it by explicitly matching and re-building:
set₁ :: Prism s a -> a -> s -> Maybe s
set₁ p x = case matching p x of
Left _ -> Nothing
Right a -> Just $ a ^. re p
†More precisely: a prism seperates the cases: a container may either contain one element, and nothing else apart from that, or it may have no element but possibly something unrelated.
If you love us? You can donate to us via Paypal or buy me a coffee so we can maintain and grow! Thank you!
Donate Us With