alex404
commented
6 months ago Hi Reuben, thanks for your interest.
So actually once upon a time I had an interest in simulating classical mechanics (for robotics) and indeed I developed goal-geometry with that in mind. I think that code is too old to really dig up, but the structure of goal-geometry is still well suited to supporting it.
In goal I generally use the charts (the c in c # x) to capture isomorphisms between points on some underlying manifold, and in particular dual spaces. You might have noticed that that there's a Dual class in Goal.Geometry.Vector. My intuition there is that one Chart indicates the Primal space (e.g. the 'Tangent' for the tangent space) and the other the Dual space (e.g. 'Cotangent').
For physics in particular, if you have some base manifold m (e.g. Pendulum) in a coordinate space (e.g. 'Euclidean'), you could define a 'Bundle m' manifold that has twice the dimension of 'm', so that 'Bundle Pendulum' would be 2d. You can then create two more charts 'Tangent' and 'Cotangent', and instantiate the 'Dual' class, so that 'Tangent # Bundle Pendulum' and 'Cotangent # Bundle Pendulum' represent the tangent and cotangent bundles, respectively. Notice that there's a 'Riemannian' class as well that develops more of the differential geometry structure.
Of course, you might rather like to think of the tangent and cotangent bundles as their own manifolds, rather then just coordinate systems on the 'Bundle', and you could construct things in this way. In goal though I've always tried to strike a balance between accurately reflecting the math, and practical utility, and I've found that the chart is a good way to capture isomorphisms like this.
When I was working with physics models (which were very simple, e.g. double pendulums) I didn't need sophisticated dependent types. I just used the structures I defined above. These days with my probabilistic models everything is very compositional, so I still don't need things like e.g. singletons, I just built up my complex models out of simpler components. Of course, your mileage may vary.
Anyway, for now I'd prefer not to include the structures directly into my code, because they wouldn't interact at all with the rest of my codebase. Still, I would be quite happy to see someone revive a 'goal-physics' package, and if became reasonably stable I could rebase some of it back into geometry.
I'm happy to answer any more questions if you'd like to pursue this more.
reubenharry
Apologies if this is a naive question, but I was curious if you'd thought about adding tangent bundles to goal-geometry. In particular, I wanted to implement some physics models on manifolds using goal-geometry, but the natural way to do that would be with a tangent or cotangent bundle. I'm assuming the issue is that this would require dependent types (or in Haskell's case, maybe a clever use of singletons?), since the tangent space depends on the point on the manifold.