-
Notifications
You must be signed in to change notification settings - Fork 21
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
Comments
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:
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 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 So my very uninformed feeling is that the rigid law is quite natural, and says that actions in |
Here is a further way to think about this. You can think about an expression Rigidity then looks at something of the form
You might think that rigidity should be a required law for every UsefulnessRigidity 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 CommentWe 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 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 |
Does op-rigidity enable any capabilities or methods that regular rigidity wouldn't? Would it perhaps make sense to have |
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 ;) |
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. |
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?The text was updated successfully, but these errors were encountered: