Use types from linear package for vectorspaces

[Jacob Hinkle]

As suggested by Anthony Cowley I've started this conversion, and it's nice so far. The main feature is that we define a vector space as a Functor over its field. Then you get certain things like scalar multiplication for free. Unfortunately, I never set it up this way originally, instead just hardcoding Double as the field.

The main motivation for this is to be able to reuse vector spaces found in other packages and to benefit from the labor of the linear developers. I'll also probably look at making some of the other classes a bit more polymorphic, where possible.

[Jacob Hinkle]

Just putting this note here for myself.

I gave this a good shot, trying to match the polymorphism found in linear. For instance, vector spaces are defined by Functors over their field, which is a little bit restricting with respect to the representation we might use for a given vector space. Trying to match that sort of polymorphism for vector bundles lead me to trying to have everything polymorphic all the way up. So I had Smooth and Riem polymorphic in some sort of "coordinate type". That's pretty cumbersome and makes it hard to remember what types you need for each function. Instead, I think I'd rather go the vector-spaces route and just have the field type as a type family in the vector space class, and possibly in the manifold classes. I might switch to having that as a dependency instead of linear in order to use existing instances.

This has been a fun little weekend investigation because I got to learn a bit more about the linear package. However, vector spaces are a pretty small part of diffgeom, and work fundamentally different than vector bundles, so I don't think I can actually get too far with them.

I would love to have a type that captured only the scalar multiplication aspect of modules/vector spaces and extend that by adding the ^+^? and ^-^? operators which check basepoint before doing vector bundle addition. But both linear and vector-spaces start by implementing the additive group aspect. What I'd like is to define "field actions" then generalize that to different additive modes for vector spaces and vector bundles.

So right now it comes down to whether I'll just look at linear and vector-spaces a bit more to get inspiration for my own classes, foregoing all the existing instances I could inherit, or just give up some of the granularity in my typeclass hierarchy and use one of those (probably the monomorphic vector-spaces one).