-
Notifications
You must be signed in to change notification settings - Fork 29
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
The distributivity law for Alternative rules out effectful instances #63
Comments
I'd be fine with either solution, but I think dropping the law is perhaps slightly better. As you noted the class still has a sensible with just the annihilation law. I don't actually know why we made it distributive. Almost certainly I read it somewhere else and copied it without thinking of or understanding the implications carefully enough. |
I think the distributivity law does make sense - since Alternative brings together two different hierarchies, it makes sense to require that they interact in some particular way. I suppose we also could do what Haskell's
There is a fair bit of consideration in #6 (comment) and https://stackoverflow.com/questions/13080606/confused-by-the-meaning-of-the-alternative-type-class-and-its-relationship-to/13081604#13081604 (which is linked by that comment in #6) but it seems like the "left catch" issue was overlooked. |
Actually no, I think the "left catch" issue was considered in #6:
So it seems like the approach proposed there is to include the distribution law strictly, and declare that "left catch" instances should not be part of the hierarchy, and including instances for Maybe and Either was where we went wrong. |
Actually I think the Maybe instance is fine either way; it appears to satisfy both left catch and left distribution. https://try.purescript.org/?gist=2aeecbc58d3c8f686c3a02d7f9c83d24 |
My gut feeling is that “left catch” instances are more useful in practice. For example, we just merged #58 which talks about how Alt instances often behave in a left catch-y way. Also, I think |
MaybeT is another example of a "left catch" instance which doesn't obey distributivity but is useful in practice; see purescript/purescript-transformers#116 |
Doesn’t the distributivity law of MonadPlus implies the distributivity law of Alternative since Also would it make sense to have a class with Applicative and Alt superclasses for types satisfying the left catch law? That way we could have instances of Alternative (without the distributivity law) and this class for MaybeT and strenghten |
I think the MonadPlus distributivity law probably does imply the Alternative distributivity law, yes. The only problem with the Alternative distributivity law is that I’m still not aware of any examples where it’s useful in practice. The same goes for the MonadPlus distributivity law too. I’d rather not have classes with these laws at all if we can’t justify them, really. |
As for a hierarchy for “left catch” behaviours, I think that that’s what the existing Alternative hierarchy de facto is right now, which makes adding new classes less appealing to me: I would rather keep the hierarchy simpler than support every edge case people can concoct. If people need to refer back to the docs every time because there are too many separate classes to keep them all in their head, I think that’s a problem. On that note: having Alt basically just be higher-kinded Semigroup doesn’t really appeal to me very much either. I’m not aware of Alt being used for types which aren’t at least also Alternative (that is, which are also Applicative and satisfy either left catch or left distribution). Additionally, I think it’s a problem that there’s no class which brings <|> and Applicative together without requiring an identity element for <|>. I think a identity for <|> is an antipattern in most cases - for left catch instances, the identity element usually represents some kind of failure case, and when things fail you generally want a meaningful error message, but it is impossible for
with Alt having the associativity and left catch laws, and Alternative having the annihilation and identity laws. That brings up another example of law violations: |
Interesting points. I had always considered |
Did you mean Applicative here? Otherwise there’s an Alt instance for There’s also good theoretical reasons to not tie Alt and Plus to Applicative because then Plus can be to Either what Applicative is to Tuple: a lax monoidal functor from a category with Either as the monoidal structure to the same category but with Tuple as the monoidal structure (whereas Applicative has Tuple as the monoidal structure in both categories). I mention this because this theoretical framework helped me understand the relationships between Alt, Plus, Apply, Applicative, Alternative and their contravariant analogues but I can get we might want to focus on the most practical use cases to simplify the hierarchy. |
Just to be clear, See also purescript/purescript-parallel#23 which I closed, but probably shouldn't be closed. |
I did mean Alternative, yeah. I'm aware that those instances can exist, but I don't think they're very practically useful: in the vast majority of cases <|> is used, I expect people are depending on Alternative-like behaviour (consciously or not). Therefore I would prefer that <|> always indicate some kind of I've just remembered about a few more Alternative instances which satisfy distributivity and don't satisfy left catch: Array, List, and LogicT. It would definitely be a shame to lose functions like |
Wouldn’t this make reasoning harder? Why not refining the hierarchy instead and get rid of unlawful instances? Here’s what I’d like to do:
-- empty <|> a = a
-- f <$> empty = empty
class Alt f <= Plus f where
empty :: forall a. f a
-- a <|> empty = a
class Plus f <= ??? f This law holds for all the
-- empty <*> f = empty
class (Applicative f, Plus f) <= Alternative f
-- pure a <|> b = pure a
class Alternative f <= ??? f
-- (f <*> a) <|> (g <*> a) = (f <|> g) <*> a
class Alternative f <= ??? f Left catch is satisfied by Distributivity is satisfied by
-- empty >>= f = empty
class (Monad m, ??? m) <= MonadZero m
Then if we consider that the distributivity laws don’t pull their weight we can even drop |
I'd like to get rid of unlawful instances, but having an overly granular hierarchy is often just annoying in practice, and when you have too many laws-only classes in there I think that realistically most people will just ignore them and do what they need to to get things to compile (which often amounts to using inferred types). I think it adds ceremony, makes it harder to remember what all the classes are, and in practice doesn't provide very much additional safety or reasoning ability beyond what a simpler hierarchy would have given you. Just to expand on what I was saying earlier: I think it's a serious problem that you have to provide an On reflection, I think testCases :: Array { x :: Int, y :: Maybe Int }
testCases = ado
x <- [ 1, 2, 3 ]
y <- optional [ 10, 20, 30 ]
in { x, y } On the right identity law: I think an important example of a type which fails it is pretty much any parsing library. For example, On the |
Oh also, I'm pretty sure that |
How do you feel about Keeping That’s the only two practical reasons I can think of against restricting Also judging by the instances of I would still have separate subclasses witnessing the left catch law and the right identity though: -- (a <|> b) <|> c = a <|> (b <|> c)
class Applicative f <= Alt f where
alt :: forall a. f a -> f a -> f a
-- pure a <|> b = pure a
class Alt f <= ??? f
-- empty <|> a = a
-- empty <*> f = empty
class Alt f <= Alternative f where
empty :: forall a. f a
-- a <|> empty = a
class Alternative f <= ??? f ( Then
The equations documenting optional empty = pure Nothing
optional (pure x) = pure (Just x) We should perhaps add an equation for Array to illustrate the behaviour to expect for distributive types if you want to relax optional (pure x) = [Just x, Nothing]
Oh my bad, I naively assumed that parsers being a composition of |
The newtype Backwards f a = Backwards (f a)
instance Apply f => Apply (Backwards f) where
apply (Backwards f) (Backwards x) =
Backwards $
(\x’ f’ -> f’ x’) <$> x <*> f and with an instance like that, |
Oh right, that annihilation law should be witnessed by |
So, have we reached consensus on what should be done here? Or are we still discussing what to do? |
I don't think we have reached a consensus just yet. For example, I haven't yet looked into the question of Alt instances for monad transformers. Additionally, the question of whether we want
As it happens we did this already: purescript/purescript-maybe#45. I think the docs there probably do need a bit more thought now. I am now leaning towards only allowing
Note: I think a two-sided identiy for ParAff is possible if The reason I'm not particularly keen on subclasses witnessing left catch versus distributivity is that all of the functions which work with an arbitrary Alt/Alternative can behave sensibly without needing to know whether we have a left catch instance or a distributivity instance, and therefore I don't see these subclasses ever being used:
|
On second thoughts this makes zero sense; if |
Regarding comonad transformers: turns out they actually can have The more I think of this, the more I agree with you, I feel like I initially missed the point. Thank you for taking the time to explain the matter and give so much good examples 🙇 So, to summarize, the proposal is to get away with the left catch and distributivity laws and this would leave us with the following (basically what you suggested in #63 (comment), minus the left catch law): -- (a <|> b) <|> c = a <|> (b <|> c)
class Applicative f <= Alt f where
alt :: f a -> f a -> f a
-- empty <|> a = a
-- a <|> empty = a
-- empty <*> f = empty
class Alt f <= Alternative f where
empty :: forall a. f a Edit: I opened purescript/purescript-maybe#51 to discuss the documentation of |
My take on this—as the person that suggested the distributivity law—is that the underlying issue here is overly constraining values. As @hdgarrood pointed out many times, requiring at least forall f a.
Control.Alt.Alt f =>
Control.Applicative.Applicative f =>
Control.Lazy.Lazy (f (Array a)) =>
f a ->
f (Array a) There's nothing about these values that requires the extra type classes nor the laws those extra type classes provide. Loosening the constraints on values addresses the actual issue better than shuffling the hierarchy or changing the laws. Those two things can be an improvement, but neither addresses the underlying issue of overly constraining values. Knowing which data types satisfy which laws is the useful part for us humans. Knowing that Overly constraining values and functions is not useful to us humans. It is exactly what leads to discussions like this, or any of the other issues linked in this one. It comes from good intentions, but almost every time we do it, it has bad consequences (like giving All that to say, the fault isn't with the type class and its laws; the fault is with overly constraining things. As far as shuffling the hierarchy goes, making I get the explanations so far, and I understand how the discussion got to this point, but @kl0tl brought up an important point about the With the current formulation, it does tend toward that because most times that a That seems to come from thinking about
The reason class (Data.Functor.Functor f) <= Choose f where
choose ::
forall a b.
(Data.Either.Either a b -> c)
f a ->
f b ->
f c
alt ::
forall a f.
Choose f =>
f a ->
f a ->
f a
alt left right = choose go left right
where
go ::
Data.Either.Either a a ->
a
go either = case either of
Data.Either.Left a -> a
Data.Either.Right a -> a We made the product and sum sides explicit in the contravariant hierarchy. The main issue with the contravariant hierarchy is also overconstraining. We decided to make An example of the problems that causes is the What I'm suggesting here is that changing the hierarchy to have the sum-side be dependent on the product-side doesn't help us nearly as much as it seems like it should. But it does rule out valid instances, may require extra constraints for instances that already exist, and will break someone's code that cannot deal with the product-side. As far as changing the law, I'd suggest we dump the whole type class. That would address the original concern, mitigate the underlying issue that keeps making these issues pop up, and not require a reshuffle in the hierarchy. Empty type classes require a lot of diligence to use correctly. Because they're only about laws–not methods–they are only practical to define, not to constrain. It seems like there's two useful purposes to empty type classes: reasoning about the behavior of a specific data type as a human, rewriting code of any data types as a computer. It's very nice to know that a specific data type behaves a certain way when you mix and match different type classes. It means we can more easily manually rewrite things when we need to. There's surely another way to communicate that concept without resorting to empty type classes. On the code rewriting front, I don't really know of any tool that does something like that right now. It seems wishful to keep these empty classes for that regard. If the compiler ever gets support for that sort of thing, it would be the time to revisit the idea. Empty type classes are sometimes used as a convenience for grouping constraints together. The issue is when we ascribe laws to the empty type class and then use that type class later as a convenience (like But, it doesn't even address the issue pointed out by @hdgarrood up above. Trying to use an empty type class to talk about multiple type classes at once means we either leave out useful combinations, or have an explosion of empty type classes for all combinations. Neither is a good situation to be in. Neither is actually necessary if we explicitly list out the actual required constraints and don't have to deal with empty type classes. Given how much pain these empty type classes cause, it seems better overall if we don't use that pattern so much. |
Keeping There’s also good theoretical reasons to have |
As previously discussed, if we're in a monad, this guarantee is already provided by the monad laws (you get Am I wrong—does someone have a use case for wanting to guarantee annihilation in a functor that is Apply and Plus but not Monad? (For example, the |
So the annihilation law enables us to talk about those applicative functors which can collect stuff along the path a branching computation actually took, without over extending to the whole taken branches. I don’t know how useful this actually is but the difference in behaviour seems enough for me to suggest that we should keep the law. |
Should we change
|
Alternative has this distributivity law:
(f <|> g) <*> x == (f <*> x) <|> (g <*> x)
However, this law rules out a few instances, most notably "effectful" ones like Effect or Aff. For example:
for which
(f <|> g) <*> x
will log "hi" once, whereas(f <*> x) <|> (g <*> x)
will log "hi" twice.Note that Effect has no Alt instance right now (and therefore no Plus or Alternative either), whereas Aff does have all of those instances.
I think it would be good to decide whether we want to keep this law and say that the problem lies with Aff's instance, or condone the Aff instance by dropping the distributivity law from the Alternative class.
It would be useful to see a concrete example of a case where the distributivity law is useful for ensuring that something behaves sensibly, because I'm not aware of any (and I think Aff's instance is used quite widely in practice, and I'm not aware of this having had any real consequences).
If we did drop the Alternative distributivity law, we'd be left with just the annihilation law,
empty <*> f = empty
. I think this makes sense as a class: I'd argue it gives you exactly what you need to write a sensible version ofguard
, since the annihilation law ensures that subsequent effects after a failedguard
are nullified, and you needpure
from Applicative andempty
from Plus (see also #62).The text was updated successfully, but these errors were encountered: