Ordered additive torsors

Stream: Is there code for X?

[Scott Carnahan]

Let V be an R-module, for some commutative ring R. I'd like to consider some power series spaces of the form (z ^ α)V((z)), for some α in a group containing the integers, such as the complex numbers. That is, exponents lie in some coset, and I'd like to impose an order on the coset compatible with translation by integers, so that elements are defined by the condition that support is bounded below. This would allow me to use existing Hahn series API to express the R((z))-module structure. Do we have typeclass language for expressing this combination of order and AddTorsor structure?

[Scott Carnahan]

It seems like CovariantClass works pretty well.

[Edward van de Meent]

You might possibly need ContravariantClass as well

[Scott Carnahan]

Thank you. It looks like I also need an AddAction version of Finest.addAntidiagonal, and a WithTop version of HahnSeries.order.