Sneak Peek: Bolt Math
I guess I’m not entirely convinced by your argument that you need a heterogeneous foundation? Many of the mathematical structures we work with are homogenous, with a few exceptions. And we usually describe non-homoegeonous operations as actions! I think numhask does it quite nicely: Additive is homogeneous, and for the non-homogeneous case you have AdditiveAction.
To give an example, we work a lot with typed unit values using the units package, which are ultimately newtypes over Double. A typed quantity like Length is additive, but has a MultiplicativeAction with Double, so you can do mm 2 *. 4 and so on. And in the same way we can use linear and give vectors actions over Double and so on. It works pretty well in practice.
I’d be interested to see an example of where you need non-homogeneousness that isn’t cleanly describable as an action?
Discussion in the ATmosphere