Applicative is Functor

[liyishuai]

Help needed:

• Instance "PApplicative is PFunctor"

[gmalecha]

I don't know how useful people find the P-versions of things. Does it make sense to just remove them? What we do with them can be accomplished via dependent types at some computation cost.

[liyishuai]

I haven't used them yet. We can remove them if that doesn't break any dependant (CI can tell that).

[gmalecha]

I think this is a good way to go.

I also wonder if there would be interest from the community to pull out Monad, Functor, Applicative as a separate library. There are a lot of libraries with exactly the same definitions and it is kind of annoying to have the same code in multiple dependencies because they don't interoperate. Specifically, I am thinking about stdpp, extlib, and meta-coq, but I wouldn't be surprised if there are others.

[vzaliva]

I support the idea of pulling monads into a separate package. It should be lean and minimalistic so it could be easily combined with other libraries.

[liyishuai]

Should we start another repo for that monad package?

[gmalecha]

I think so. I think it deserves a bit of thought though as we would like a light weight solution that is still sufficient to do almost everything that people already do.

I think it is also important to find who has existing implementations of this functionality and what would get them to switch to a dependency.

[liyishuai]

Discussions are continued in #79