Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Intuition for rigidity #57

Open
kozross opened this issue Jul 7, 2022 · 5 comments
Open

Intuition for rigidity #57

kozross opened this issue Jul 7, 2022 · 5 comments

Comments

@kozross
Copy link

kozross commented Jul 7, 2022

I'm aware of the technical definition of what it means for a Selective to be rigid. What I'm missing is the significance of being (or indeed, not being) rigid: in short, why is ridigity, or lack thereof, a useful property?

@turion
Copy link
Collaborator

turion commented Jul 7, 2022

Just for the benefit of not having to switch tabs, the definition is:

f <*> x = select (Left <$> f) ((&) <$> x)

To me this always sounded like a sensible thing that might be asked of all selectives, but apparently there are some that don't satisfy it. The article says that:

the Validation instance is not a rigid selective functor because select occasionally
discards effects in the second argument

I don't understand this completely.

instance Semigroup e => Applicative (Validation e) where
  pure = Success
  Failure e1 <*> Failure e2 = Failure (e1 <> e2) -- Accumulate errors
  Failure e1 <*> Success _ = Failure e1
  Success _ <*> Failure e2 = Failure e2
  Success f <*> Success a = Success (f a)

instance Semigroup e => Selective (Validation e) where
  select (Success (Left a)) f = ($a) <$> f
  select (Success (Right b)) _ = Success b -- Skip after false conditions
  select (Failure e) _ = Failure e -- Skip after failed conditions

Let's try and see in which cases Validation e is not rigid.

Failure e1 <*> Failure e2 =!= select (Left <$> Failure e1) ((&) <$> x)
-- Applicative definition ||| Validation functor
Failure (e1 <> e2)        =!= select (Failure e1) ((&) <$> x)
--                        ||| Selective definition
Failure (e1 <> e2)        =!= Failure e1

I skimmed over the other 3 cases and I think for those, the rigidity law holds. What I don't really understand is why we're not defining:

select (Failure e1) (Failure e2) = Failure $ e1 <> e2
select (Failure e) (Success _) = Failure e

I can't see any Selective laws broken, and this would make Validation e rigid. While keeping its secret superpower, which is detecting Failures ahead. If someone would want to skip a later action, one could simply convert Validation to Either and select on that.

So my very uninformed feeling is that the rigid law is quite natural, and says that actions in Applicative are chained the same way as in Selective.

@turion
Copy link
Collaborator

turion commented Jul 7, 2022

Here is a further way to think about this. You can think about an expression Left <$> f like "all inner values are Left". For example, if f = [a, b, c], then Left <$> f = [Left a, Left b, Left c].

Rigidity then looks at something of the form select x y and says that if all the inner values x are Left, then y may not be skipped. Given that the slogan about select is:

you must apply the function of type a -> b when given a value of type Left a, but you may skip the function and associated effects, and simply return b when given Right b.

You might think that rigidity should be a required law for every Selective! I'm certainly starting to think this now.

Usefulness

Rigidity is a useful property because it validates the following law:

x *> (y <*? z) = (x *> y) <*? z

This is called the "interchange law". I find it more akin to an associative law, actually. I believe it is a very useful law, because otherwise reasoning in hypothetical Selective Do notation gets hard. Consider:

main = do
  foo
  x <- bar
  case x of
    Left a -> (($ a) <$> z)
    Right b -> pure b

Should this get desugared to x *> (y <*? z) or (x *> y) <*? z? There is an arbitrary choice, but with rigidity you don't have to worry!

Comment

We could also cook up a related law, let's call it "op-rigidity":

select (Right <$> x) y == x

This would say that "you must skip the function and associated effects when given Right b". Obviously many Selectives will not satisfy this, foremost all that are defined via selectA.

It is wise that we don't require selectives to be both rigid and op-rigid at the same time. Consider a functor that has a constant summand, for example:

data MyEither e a = Oops e | Fine a
  deriving Functor

Now Right <$> Oops e == Oops e == Left <$> Oops e. But this puts us in a tight spot because this now means that select (Oops e) ((&) <$> y) has to be both Oops e and Oops e <*> y! With other words we've constrained <*> to match the Applicative instance of Either, and we can never implement something like Validation. Unless we don't require both laws, and to me it seems sensible not to require op-rigidity.

@kozross
Copy link
Author

kozross commented Jul 7, 2022

Does op-rigidity enable any capabilities or methods that regular rigidity wouldn't? Would it perhaps make sense to have Selective, which is rigid, but not op-rigid, and OpSelective which is both?

@turion
Copy link
Collaborator

turion commented Jul 8, 2022

I'm not aware of any yet. But note that rigidity is a law that Andrey Mokhov et al have researched in a peer-reviewed article, and op-rigidity is a thing I just came up on a whim and posted in a github comment ;)

@snowleopard
Copy link
Owner

Thanks for the interesting discussion! :) Let me add a few thoughts:

  • I don't have a good "intuition for rigidity" to offer. I do have a plain practical motivation. Quoting the paper:

    As we remarked in §2.3, rigid selective functors have a particularly simple normal form thanks to the additional law (<*>) = apS, which tells us that the apply operator <*> is redundant and can be implemented via the selective interface.

    So, I simply take advantage of the fact that rigid selective functors have a simple normal form and hence give us a simple free construction. Perhaps, the "intuition for rigidity" is that rigidity takes the Applicative interface out of the picture.

  • I think it's more instructive to look at Under as an example of a non-rigid selective functor: it's much more basic and simpler than Validation. (In some sense that can be made precise, Validation is a lifted version of Under.)

  • The "op-rigidity" law is featured in the paper under the name "pure Right property" (I believe they are not exactly the same but the differences aren't particularly interesting for this discussion). I suggest taking another look at §2.3 in the paper: it discusses the pure Left and Right properties and how they relate to the Under and Over selective functors. I've just re-read it and... I think it's pretty good? :)

Happy to continue the discussion! If there are any questions that I might have missed that need answering, please let me know.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

No branches or pull requests

3 participants