Alternative reform

[garyb]

@paf31 What would this look like then, the way it is in semigroupoids?

[paf31]

I don't think that's a bad option :)

[garyb]

So:

  class (Functor f) <= Alt f where
    (<|>) :: forall a. f a -> f a -> f a

  class (Alt f) <= Plus f where
    zero :: forall a. f a -> f a -> f a

  class (Applicative f, Plus f) <= Alternative f

Would we want to go with zero or empty for the identity?

One thing I'm not sure about now is what happens with MonadPlus and MonadOr. Semigroupoids doesn't have the distinction, and just has Alternative as a superclass of MonadPlus, so we'd have something like this:

But it seems MonadOr is probably redundant (as morelse is <|>, and mzero is zero). In fact the definition would be a bit weird, because if the class is class (MonadZero m, Alternative m) <= MonadOr m then we have to define both mzero and zero, but if we have the class as class (Monad m, Alternative m) <= MonadOr m then it also seems weird that there's no mzero?

If there isn't a good reason for Plus to exist, one option would be to have something like:

Basically, renaming Plus to Zero and making Applicative the superclass rather than Alt, and then having MonadZero as a class with no members but rolling Zero and Monad together... but I suspect there's good reasons why that's not the right thing to do, although I don't know of anything that is Plus but not Applicative myself.

[garyb]

Also pinging @joneshf / @puffnfresh / @jdegoes, any input would be appreciated again.

[jdegoes]

Will review tomorrow if that's not too late.

Sent from my iPhone

On May 20, 2014, at 7:51 AM, Gary Burgess notifications@github.com wrote:

Also pinging @joneshf / @puffnfresh / @jdegoes, any input would be appreciated again.

—
Reply to this email directly or view it on GitHub.

[paf31]

Do we have a use case in mind for breaking stuff up this way? Either perhaps?

[garyb]

Alright, here's another idea, excluding MonadOr as I don't think it needs to exist, however, if it does, all it would be is an empty class with Monad (or MonadZero, it doesn't matter now as there's only one zero in this hierarchy) and Alternative as superclasses:

In fact, do we need to even make it MonadZero and MonadPlus, wouldn't AlternativePlus/z do instead?

Perhaps with this mplus should be called <+>, although that would conflict with the ArrowPlus operator elsewhere.

[garyb]

Or <<>>/<++> maybe, to better match the usual Monoid.

[joneshf]

I kind of want to turn this into a blog post, so it's going to get a bit wordy. Also, there wasn't a real good explanation for this in one specific place.

As mentioned, I didn't really understand this whole thing before (and still feel a bit like I'm missing something), but I think the whole point of this branch in the hierarchy is to give monoidal semantics to functorial structures.

We can't just use a fully qualified instance of Monoid and Semigroup because they would be dependent on the inner type, and the semantics wouldn't be the same. We want to combine the functorial structures, not the data within the structures.

This is what the Maybe instance of Monoid does in Haskell. Because of this, it doesn't agree with the Alternative instance.

So, to get the monoidal structure, we define similar classes.

Alt needs to obey the standard Semigroup law of associativity:

• x <|> (y <|> z) = (x <|> y) <|> z

As well, it should interact with the Functor instance for left distributativity:

• f <$> (x <|> y) = (f <$> x) <|> (f <$> y)

Plus needs to obey the standard Monoid law of identity:

• empty <|> x = x
• x <|> empty = x

And also interact with the Functor instance for right annihilation:

• f <$> empty = empty

Alternative is the point where we say that we want our monoidal semantics to interact with the applicative functorial strucures. Alternative being a superclass of both Applicative (and therefore Apply) and Plus, it needs to express the interaction between these.

The interaction is <*> right distributing over <|> and left annihilation for the Apply instance:

• (f <|> g) <*> x = (f <*> x) <|> (g <*> x)
• empty <*> x = empty

Interestingly, I'm not sure that we can say anything about left distributativity or left annihilation. See this answer for more details. Though, the conclusions reached may have only been in order to keep compatibility with what is already defined.

Now, if we want to show that our monoidal semantics interact with the monadal structures, we need another type class for that. It would seem that we should have MonadPlus be a superclass of MonadZero. This fits more in line with the Semigroup -> Monoid hierarchy. However, we didn't get this granular with applicative functors when we created Alternative. We just said, "This is how you interact between monoidal semantics and applicative functorial strucures," without mentioning that you could only have an Alt that you wanted to interact with Applicative.

I feel that this is mostly a design decision. We have to say enough is enough, because otherwise we end up with an exponential explosion of typeclasses. So, maybe we don't really need to have both MonadPlus and MonadZero. The functions they would provide should already be provided from Alt, and Plus (confusing names btw). We just have to pick one hierarchy that works best in the general case. This is not to say that someone couldn't make a new hierarchy. In fact, many others exist, but for our purposes, I'm not sure we should be so granular.

In any case, the laws that need to be held are >>= right distributing over <|> and left annihilation for the Bind instance:

• (x <|> y) >>= f = (x >>= f) <|> (y >>= f)
• empty >>= f = empty

What I'm suggesting is that, if you have a MonadPlus, you can derive an Alternative, Monad, and friends. But not the other way around. We need MonadPlus because Alternative by itself cannot ensure left annihilation or right distribution for the Bind instance.

This makes one ask, where does MonadOr fit into the picture? Well, I don't think it belongs in this part of the hierarchy. It seems like it has a purpose, but it's not for combining monoidal semantics with functorial strucures.

And that last part makes me ask, where is Group in all of this? Have we as a community looked at combining groupal semantics with functorial strucures?

Thoughts?

Most of this information was gathered from:

http://stackoverflow.com/a/10168111/1549047
http://stackoverflow.com/q/13122489/1549047
http://stackoverflow.com/q/13122489/1549047
http://stackoverflow.com/a/13081604/1549047
http://stackoverflow.com/a/13115196/1549047
http://stackoverflow.com/a/13174738/1549047
http://cstheory.stackexchange.com/q/14143
http://cstheory.stackexchange.com/a/14146/23058
http://cstheory.stackexchange.com/a/14144/23058

[garyb]

I'll check out those links and do some reading, but your reasoning seems pretty solid to me.

I probably wasn't really approaching it from the right angle, one of the reasons I had Alternative separate from MonadPlus is I wasn't sure you could always have both, or sometimes you don't care about <|> but do need mzero/mplus, so I was trying to avoid having to provide instances for both, but if you can derive Alternative from MonadPlus then that's awesome.

Nice work. 👍

[joneshf]

Well, it would be an empty definition for both classes, like how Monad is now. It's just to express the interaction between the two sides of the hierarchy.

Also, your other formulations were good, don't discount them. Sometimes we need to take a second to think about how else we can express ideas, rather than just going with what has already been done. There's nothing suggesting that the Haskell way is the one right way. It's just the convention we have for most things, but we could've reformulated some of the types/classes and still gotten equivalent expressive power.

I'd really like for there to be someway for us to specify at compile time the laws these are supposed to uphold, but without getting into full on proofs (which might be out of scope for the language), I'm not sure there's a way. I'd love to be wrong though.

@jdegoes didn't you mention some kind of idea about verifying laws or something in #purescript like 3-4 months ago?

[paf31]

I like @joneshf's proposal. I like the ones @garyb wrote down too, but I'm also in favour of removing as many intermediate classes as possible that we aren't likely to ever use (like Zero?) and I think the last graph is nice and simple.

I would be interested to try and find an example of a Plus which is not an Alternative.

[jdegoes]

Type classes are only useful to the extent they have laws which permit formal reasoning. Zero has no laws and is therefore a type class anti-pattern.

@joneshf This is far beyond the scope of this ticket, but in answer to your question, I would love it if type classes had a formal representation of their laws. In Idris, this is actually quite easy, although it becomes correspondingly harder to define instances.

For a language like Purescript without dependent types, this would probably require special syntax / compiler support. I'm about 60% done with a blog post on type classes that explores some of the possibilities (unfortunately I started it months ago and haven't made any progress due to work!).

[paf31]

There was an interesting Reddit post about how to use Template Haskell with QuickCheck to test laws as part of a type signature. I'd like to try something like that after ps-in-ps is working, as a library, as opposed to specific compiler support.

[joneshf]

I think we need Zero/Plus as much as we need Monoid. They are equally important I feel.

I would be interested to try and find an example of a Plus which is not an Alternative.

Our good friend Map comes to spoil the party:

...
import qualified Data.Map as M

instance altMap :: (Ord k) => Alt (Map k) where
  (<|>) m  m' = m `M.union` m'

instance plusMap  :: Plus (Map k) where
  empty = M.empty
...

But since you can't define an Applicative for Map, you can't have an Alternative. Really it's just anything that is parameterized over more than one type variable for which there is no sensible default for all but the last type variable.

Then you might ask, do we need to be even more granular and have some interaction between Apply and Alt/Zero? I'm not sure. We don't have to be the only solution to this hierarchy. Anyone can build up their own and distribute it. Or we could offer multiple hierarchies as well (that reminds me of an idea i had with bower the other day). At the same time, I feel we should try to provide the least broken solution, so we don't end up like haskell where the hierarchy still hasn't been fixed.

I'm about 60% done with a blog post on type classes that explores some of the possibilities

Looking forward to it!