Is there One version Finsupp

Stream: Is there code for X?

[hilbert]

docs#Finsupp and docs#DFinsupp define for type class Zero. Is there a One version Finsupp?

[Weiyi Wang]

I literally had the exact same question just now. It seems there is none. There is even Finsupp.prod that still uses 0 as indicator even though it is a multiplicative concept

[Yaël Dillies]

No there isn't but there have been talks about generalising finsupps to an arbitrary element, eg @Sky Wilshaw needed this at some point

[Yaël Dillies]

IMO it's currently difficult to refactor things satisfactorily because DFinsupp isn't currently a special case, meaning that either you align the new FinsuppI/DFinsuppI on Finsupp/DFinsupp and duplicate yet again a huge amount of API, or you define FinsuppI in terms of DFinsuppI and now you need to decide whether to stick to the Finsupp or DFinsupp design

[Yaël Dillies]

I've been putting off making a decision here, so instead I've worked on making sure that the files that could become files about FinsuppI do not contain any arithmetic. See most recently #25002

[Yaël Dillies]

cc @Eric Wieser since you're probably tied with me for the prize of "most bothered by the current statu quo"

[Jz Pan]

Does Finsupp α (Additive M) help? It is cumbersome, though.

[hilbert]

Jz Pan said:

Does Finsupp α (Additive M) help? It is cumbersome, though.

It's very inconvinient since I actually want a Multiplication version of docs#DirectSum .

[Eric Wieser]

How bad would it be to do everything with addition instead?