On Tue, May 28, 2013 at 11:22:22PM +0200, Johannes Gerer wrote:
I have to ask, why was plausability and looking at the actual definition (not just the types) not important for the other examples.
It would also be important to check the definitions in the other examples too, but it's hard enough to get the types to match!
But I think my problem lies somewhere else. Maybe all would become evident, if I knew the rigorous definition of "A is more general than B" in this context. Especially when A is a class of type, that takes two arguments (i.e. Unit and Arrow) and B for ones, that takes only one (like Monad, Pure,..)
I'm not sure what the right definition is. You are right that it is far from obvious (at least to you and me!). For a definition of equivalence, I feel it should go something like this: To every instance a of A I can assign an instance b of B, and to every instance b of B I can assign an instance a' of A. Moreover there should be a function polymorphic in all parameters between a and a', which has a polymorphic inverse. (And likewise for A and B swapped). These functions might need to be required to commute with all member functions of A. Perhaps this is perfectly obvious and well known, but I haven't managed to work it out on my own. Tom