Use types from linear package for vectorspaces
Issue #1
new
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.
Comments (1)

 Log in to comment
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 byFunctor
s 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 hadSmooth
andRiem
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 thevectorspaces
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 oflinear
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 ofdiffgeom
, 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 bothlinear
andvectorspaces
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 vectorspaces 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 vectorspaces one).