Make Data.Map a vector space.

[jyp]

I tried to make Data.Map a vector space, but I found that the Left/RightModule Natural/Integer v superclass constraint of Monoidal/Group meant that I had to declare several incoherent instances.

Hence I have removed these constraints, as well as the LeftModule () a instance, which is also incoherent.

[ekmett]

Data.Map as a vector space has been a rather persistent source of headaches in the linear library as it isn't quite true. Every vector space is a free vector space, and a Map is a representation of a sparse vector space really only if you can compare the scalars for equality with 0. We compromised and added it to linear in exchange for a rather huge increase in the complexity and loss of principles.

Losing the left/right module for Integer over all groups is actually quite a severe problem, so I'm loathe to take this patch as given. I'll leave the issue open to remind that there is an issue, however.

That said, the unit module can probably die.

[jyp]

I don't think that I understand your point about Map.

However, modules for Natural (Integer) cause overlapping instances for every polymorphic Monoidal (Group) instance needed for a vector space. Say you want to define:

instance (Monoidal v) => Monoidal (v,v)

then you need:

instance LeftModule Natural (v,v)

but I would also like

instance LeftModule c v => LeftModule c (v,v)

And so we get incoherent instances.

Furthermore, as I see it the left module for group is already captured by the "times" method. So I am not sure what is gained by having both. Besides, the usual mathematical definition of Monoidal/Group certainly are not formulated in terms of module. So it felt like a quirk to me.

[ekmett]

There are certain traps we find ourselves in because of the uniqueness of instances in Haskell. In mathematics it is unambiguous to state that every group forms a module over the integers, and every monoid forms a module over the naturals in a canonical way. It can be quite useful to require such an instance as part of the definition of a group or monoid because it can then allow it to work more efficiently, e.g. by exploiting idempotence or peasant multiplication, but more importantly, it can let me avoid having to make up new vocabulary (e.g. times) for exactly the same thing. Such vocabulary requires me to know which special case I'm concerning myself about, and generally renders code messy.

The times method is one way to capture the functionality, but it comes at the cost of a consistency in that sense, (that we can say this fact uniformly for all groups / monoids) using the same vocabulary as any other module / vector space structure.

On the other hand, the current mess gets in the way of parametrically specifying a vector space, and I, like you, am not terribly happy with that.

I understand that you want to resolve this ambiguity in one direction. It is a reasonable stance to take. However, I'm not entirely happy with having to do so.

Alternatives are available. For example, we could allow overlap but disallow incoherence, etc. This would require more instances but would in theory allow us to proceed without losing the constraint. I'm leaving this open until I can spend more time on trying to resolve that style of approach.

Other approaches I've made good use of elsewhere are to require some constraints-package style explicit dictionary opening to supply such meta-constraints that are hard to teach the typeclass system to enforce.

Until I've exhausted those approaches I'm rather unhappy with the idea of giving up on these superclasses. If I do give up on them, I'll be stating something much weaker than the object I want to really talk about.

[jyp]

I'll just add for the record that dropping the superclass constraint does not preclude writing the module instances when they are unambiguous.

Here is an idea for a resolution though: relax the superclass to talk about any type which can be embed Naturals (resp. Integers):

class IsNatural n where
  fromNatural :: Natural -> n

class (IsNatural n, LeftModule n m, RightModule n m) => Monoidal m where
   ...

[ekmett]

It doesn't preclude writing the module instances, but it prevents you from knowing they are canonically available.