class for Finsupp like structures

Stream: mathlib4

[Alfredo Moreira-Rosa]

At the moment we have one implementation for Finsupp, but i know that other ones are implemented outside mathlib with different required properties :

• i heard about one from @Kim Morrison that's computable, efficient, require Hashable and using HashMap
• i'm implementing one (also computable) that require LinearOrder and using TreeMap
• i saw one in CsLib

So, to guide all these implementations and have some common lemmas for free, would it be interresting to have a class to bind them all ? like this ?

class FinsuppLike (F : Type w) (α : Type u) (M : Type v) [FunLike F α M] [Zero M] [Zero F] where
  support : F → Finset α
  mem_supp : ∀ (f : F) (a : α), a ∈ support f ↔ f a ≠ 0
  not_mem_supp : ∀ (f : F) (a : α), a ∉ support f ↔ f a = 0
  single  : α → M → F
  ... other common operations
  ... other common laws

[Edward van de Meent]

My first thought upon reading was: making a class for these surely defies the purpose of having multiple implementations, namely to have different performance specs?

For the purpose of proving things, sure, this would work, but if you care about performance you need to consider the performance of the underlying implementations, and choose the one that best suits your purpose. In that case, figuring out which function is implemented in which way for which instance seems like more of a nuisance than anything... (compared to just plainly specifying the function you want)

For proving stuff it could be beneficial, maybe as a way to turn operations in other implementations into a "canonical" choice of implementation which is suited for proving things about?

[Alfredo Moreira-Rosa]

I don't understand your thoughts about performance. A class would not impose any performance requirements.
Example, in my implementation, the real support is using TreeMap, but i defined an exposed support that is using Finset for the mathematical properties. The TreeMap is hidden from the user, the only thing that is exposed is that you need to provide a LinearOrder on α. But is not exposed at the class level.

Can you expand a lithle more about your concerns about performance?

[Edward van de Meent]

as for the specific design, i suspect that rather than using FunLike F α M, we'd want to use something like GetElem (or just inline the whole operation) (particularly since (afaik) HashMaps don't implement FunLike?)

[Alfredo Moreira-Rosa]

The F here is not the HashMap, it's your Finsupp impl. And for sure your Finsupp impl should implement FunLike

[Alfredo Moreira-Rosa]

I give you a MVW of my implementation as an example :

structure OrdFinsupp.{u, v} (α : Type u) [LinearOrder α] (M : Type v) [Zero M] [DecidableEq M] where
  _support : Std.ExtTreeMap α M
  _ne_zero: ∀ a, a ∈ _support ↔ ∃ m, _support.get? a = some m ∧ m ≠ 0

infixr:25 " ↦₀ " => OrdFinsupp

def apply (f : α ↦₀ M) (a : α) : M :=
  match f._support.get? a with
  | some m => m
  | none   => 0

instance : FunLike (α ↦₀ M) α M where
  coe f := f.apply
  coe_injective' := by ...

[Alfredo Moreira-Rosa]

You would then just have to link your implementation like this :

instance : FinsuppLike (α ↦₀ M) α M where
  ....

[Edward van de Meent]

Alfredo Moreira-Rosa said:

The F here is not the HashMap, it's your Finsupp impl. And for sure your Finsupp impl should implement FunLike

for programming purposes, i'd say HashMap is very much like Finsupp, i.e. a way of storing some amount of data of some type indexed by some other type. There is an effective equivalence between HashMap A B (or ExtHashMap A B if you want to be pedantic) and Finsupp A (WithZero B).

As for my previous point, the issue i see is with ergonomics. If you want to write a performant program, it very possible that you need to use a certain implementation, where things like "getting the value at the smallest index" are efficient rather than "reading out all values of the structure" or "reading out a single value of the structure". It's easy for an abstraction like this to miss these kinds of highly specialized functions, which then are built up out of the basic operations which are stored in the class, at the cost of possible performance. However, because of the abstraction, it's not at all obvious that your implementation is not as performant as it could be, which seems like a tally against using the class to me.

(a specific case i was considering is explained in detail in this excellent video on fibonacci heaps, which in my opinion are finsupp-like)

[Alfredo Moreira-Rosa]

I still don't understand your point. I'm pretty sure exposing only math properties on FinsuppLike the way i did don't improse anything on the underlying implementation.
It's pretty much the same as CommGroup don't impose anything on your Nat implementation.
This is just saying, that a Finsupp should have a support and how it behaves when an element is in (is is not in) the support.
Anyway, thank you for the feedback.

[Aaron Liu]

Alfredo Moreira-Rosa said:

This is just saying, that a Finsupp should have a support and how it behaves when an element is in (is is not in) the support.

But docs#DFinsupp doesn't have a support in the way you describe (you can get one out when the domain has decidable equality and the codomain has decidable nezero)

[Alfredo Moreira-Rosa]

Thanks Aaron, I did not dive into DFinsupp.
But my question still remains. Could we define a class to bind all implementations? That's the core of my question.
I think it would solve some difficulties we have to change these implementations, and allow more experimenting on them.
But maybe that's not desirable.

[Alfredo Moreira-Rosa]

---

I just checked DFinsupp on my toy class and it don't pose any issue (you don't need to leak DecidableEq into the class):
here my impl working just as with Finsupp and DFinsupp :

-- my impl
instance instFinsuppLikeOrdFinsupp : FinsuppLike (α ↦₀ M) α M where
  support := OrdFinsupp.support
  single := OrdFinsupp.single
  mem_support := OrdFinsupp.mem_support_iff
  zero_support := OrdFinsupp.support_zero

-- Finsupp impl
noncomputable instance instFinsuppLikeFinsupp : FinsuppLike (α →₀ M) α M where
  support := Finsupp.support
  single := Finsupp.single
  mem_support := Finsupp.mem_support_iff
  zero_support := Finsupp.support_zero

-- DFinsupp
instance instFinsuppLikeDFinsupp :
    FinsuppLike (DFinsupp (fun _ : α => M)) α M where
  support := DFinsupp.support
  single := DFinsupp.single
  mem_support := DFinsupp.mem_support_iff
  zero_support := DFinsupp.support_zero

using the following class :

class FinsuppLike (F : Type w) (α : Type u) (M : Type v) [FunLike F α M] [Zero M] [Zero F] where
  support {M} : F → Finset α
  single : α → M → F
  mem_support : ∀ {f : F} {a : α}, a ∈ support f ↔ f a ≠ 0
  zero_support : support (0 : F) = ∅

And with those you can prove already a lot of the basic lemmas that could be shared with different implementations.

[Yaël Dillies]

Why are you trying to make an efficient type, rather than efficient operations?

[Alfredo Moreira-Rosa]

What do you have in mind ? Using efficient data structure gives efficient operations. So maybe i don't understand the question. Can you elaborate ?

[Yaël Dillies]

An inefficient representation forces inefficient operations, but I don't think an efficient representation will make you write efficient operations automagically. In this case, DFinsupp is an okay representation, and you can write rather efficient operations on it. I am not yet convinced you need a new, more efficient, representation.

[Eric Wieser]

Can you make the above code a #mwe? I think you're still in trouble, because you'll conclude things like "DFinsupp is only finsupp-like when the domain and codomain satisfy certain conditions".

[Alfredo Moreira-Rosa]

Yes, my toy exemple was not made to adapt to DFinsupp. But rather to ask if having a class is something that is desirable or not.

Don't focus too much on why i'm doing my own impl. I suspect Kim impl is much better than mine but i did not want to require Hashable, and LinearOrder seemed like a good tradeoff for me.

[Alfredo Moreira-Rosa]

So to clarify, i don't want to merge my impl on Mathlib, just asking if we want to have a class for this in Mathlib.
If so i'm willing to work on it and discuss it here

[Eric Wieser]

I think the point here is that the difficult bit is not choosing the right implementation for Finsupp given its API, but choosing an API that permits a performant implementation. By choosing the API in your typeclass you've already done this hard step, and you may as well just pick an efficient implementation of it and write DFinsupp.toMyFinsupp etc

[Alfredo Moreira-Rosa]

@Eric Wieser is this enough of a #mwe ?

section
universe u v w

class FinsuppLike (F : Type w) (α : Type u) (M : Type v) [FunLike F α M] [Zero M] [Zero F] where
  support {M} : F → Finset α
  single : α → M → F
  mem_support : ∀ {f : F} {a : α}, a ∈ support f ↔ f a ≠ 0
  zero_support : support (0 : F) = ∅

namespace FinsuppLike
variable {α : Type u}
variable {M : Type v} [Zero M]
variable {F : Type w} [Zero F] [FunLike F α M]

theorem ext [FinsuppLike F α M] {f g : F} (h : ∀ a, f a = g a) : f = g :=
  DFunLike.ext _ _ h

lemma ne_iff [FinsuppLike F α M] {f g : F} : f ≠ g ↔ ∃ a, f a ≠ g a := DFunLike.ne_iff

lemma not_mem_support [inst : FinsuppLike F α M] {f : F} {a : α} :
  a ∉ inst.support f ↔ f a = 0 := by
  rw [FinsuppLike.mem_support]
  exact not_ne_iff

theorem zero_apply [FinsuppLike F α M] : ∀ (a : α), (0 : F) a = 0 := by
  intro a
  apply FinsuppLike.not_mem_support.mp
  intro h
  rw [FinsuppLike.zero_support] at h
  exact Finset.notMem_empty a h

end FinsuppLike

[Eric Wieser]

I meant one including your instance instFinsuppLikeDFinsupp

[Alfredo Moreira-Rosa]

wasn't my code above enough, repeating it here :

import Mathlib.Data.DFinsupp.Defs

section
universe u v w

class FinsuppLike (F : Type w) (α : Type u) (M : Type v) [FunLike F α M] [Zero M] [Zero F] where
  support {M} : F → Finset α
  single : α → M → F
  mem_support : ∀ {f : F} {a : α}, a ∈ support f ↔ f a ≠ 0
  zero_support : support (0 : F) = ∅
end

section
universe u v w

variable {α : Type u} [DecidableEq α]
variable {M : Type v} [Zero M] [DecidableEq M]

instance instFinsuppLikeDFinsupp :
    FinsuppLike (DFinsupp (fun _ : α => M)) α M where
  support := DFinsupp.support
  single := DFinsupp.single
  mem_support := DFinsupp.mem_support_iff
  zero_support := DFinsupp.support_zero
end

[Alfredo Moreira-Rosa]

DecidableEq is only needed for the instance, not the FinsuppLike declaration

[Alfredo Moreira-Rosa]

Edited #mwe to separate FinSuppLike and instance requirements

[Eric Wieser]

Right, so for your specification, DFinsupp (fun _ : Nat => M') for an arbirary type with zero M' is not Finsupp-like

[Eric Wieser]

And I can't use FinsuppLike.single in that case, even though DFinsupp.single would work

[Alfredo Moreira-Rosa]

In this case, since only the impl is impacted, just changing it to makes it work for M':

variable {M : Type v} [Zero M] [(x : M) → Decidable (x ≠ 0)]

For single issue, do you think it can be fixed ? any idea ? not worth it ?

[Eric Wieser]

One fix would be to split FinsuppLike into a separate class for single and support