Why doesn't a prism set function return an Option/Maybe
Asked Answered
B

2

8

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).

Buhrstone answered 23/9, 2017 at 20:51 Comment(0)
F
11

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.

Federative answered 23/9, 2017 at 22:10 Comment(5)
Is that Just actually a Right?Photina
Thank you, I believe I understand now. Perhaps I will write my own version of a set operation. F# (which lacks higher kinded types - for now), wouldn't allow me to express the general form of a traversal, so the fact that a prism is a special case of a traversal is really of no particular benefit that I'm aware of.Buhrstone
@NathanWilson, I suspect type-changing prisms may still be useful even in that restricted context, and those really need the extra flexibility of Either.Righteousness
@dfeuer, I had honestly never heard of type-changing prisms until reading your answer. Certainly something I will have to do some research on - thanks for pointing that out to me.Buhrstone
@NathanWilson, the basic idea is that if the value is found not to be built from the specified constructor, then any parameters mentioned only under the specified constructor are irrelevant and can be changed to anything whatsoever. [] :: forall a. [a], Nothing :: forall a. Maybe a, Left (x :: a) :: forall b. Either a b, Right (x :: b) :: forall a. Either a b, etc.Righteousness
R
12

I doubt there's one definitive answer, so I'll give you two here.

Origin

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.

Nice hierarchy

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.

Righteousness answered 23/9, 2017 at 21:23 Comment(0)
F
11

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.

Federative answered 23/9, 2017 at 22:10 Comment(5)
Is that Just actually a Right?Photina
Thank you, I believe I understand now. Perhaps I will write my own version of a set operation. F# (which lacks higher kinded types - for now), wouldn't allow me to express the general form of a traversal, so the fact that a prism is a special case of a traversal is really of no particular benefit that I'm aware of.Buhrstone
@NathanWilson, I suspect type-changing prisms may still be useful even in that restricted context, and those really need the extra flexibility of Either.Righteousness
@dfeuer, I had honestly never heard of type-changing prisms until reading your answer. Certainly something I will have to do some research on - thanks for pointing that out to me.Buhrstone
@NathanWilson, the basic idea is that if the value is found not to be built from the specified constructor, then any parameters mentioned only under the specified constructor are irrelevant and can be changed to anything whatsoever. [] :: forall a. [a], Nothing :: forall a. Maybe a, Left (x :: a) :: forall b. Either a b, Right (x :: b) :: forall a. Either a b, etc.Righteousness

© 2022 - 2024 — McMap. All rights reserved.