snowleopard / selective

Selective Applicative Functors: Declare Your Effects Statically, Select Which to Execute Dynamically
MIT License
202 stars 21 forks source link

Intuition for rigidity #57

Open kozross opened 2 years ago

kozross commented 2 years ago

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 commented 2 years ago

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 commented 2 years ago

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 commented 2 years ago

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 commented 2 years ago

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 commented 2 years ago

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

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