FinFun vs Finsupp

Stream: computer science

[Tristan Figueroa-Reid]

Is there a particular use case for wanting FinFun over Finsupp?

[Fabrizio Montesi]

Thanks for bringing this up.
Once upon a time, in the project FinFun comes from (https://chords.dev), it was not so similar to Finsupp. It's a coincidence that it evolved this way, and now I'm in doubt myself about it. That's why I put an explicit 'API unstable'/not cooked comment at the beginning of FinFun.

But yeah, we should remove it if Finsupp does the same thing, probably. We might need to extend it with computable functions though, like for going back and forth from/to List. In compilers we expect functions with finite support to have finite representations. Is that possible already? I see Finsupp uses noncomputable in its whole file.

@x.y. what do you think? You're the main user of FinFun together with me, that I know of.

[Tristan Figueroa-Reid]

Right - I forgot about that. I noticed this only because I was looking at Finsupp earlier from another thread.

FinFun seems fine, though it doesn't respect extensionality the same way that Finsupp does.

[Fabrizio Montesi]

Side question: Would it be called Finfun in mathlib style?

[Fabrizio Montesi]

Thanks for the pointer to the thread. That suggests we should keep and improve FinFun for now, I guess.

[x.y.]

Fabrizio Montesi said:

Thanks for bringing this up.
Once upon a time, in the project FinFun comes from (https://chords.dev), it was not so similar to Finsupp. It's a coincidence that it evolved this way, and now I'm in doubt myself about it. That's why I put an explicit 'API unstable'/not cooked comment at the beginning of FinFun.

But yeah, we should remove it if Finsupp does the same thing, probably. We might need to extend it with computable functions though, like for going back and forth from/to List. In compilers we expect functions with finite support to have finite representations. Is that possible already? I see Finsupp uses noncomputable in its whole file.

x.y. what do you think? You're the main user of FinFun together with me, that I know of.

I do need something computable so I guess to me FinFun is a quite useful data type that is not exactly replaceable by Finsupp… tho I agree that we do not have enough important properties encoded for it.

[Tristan Figueroa-Reid]

(To clarify, Finsupp's underlying structure is computable - the theory around it isn't.)

[Fabrizio Montesi]

Let's see where we can go with FinFun then. A few initial questions:

• I guess it should be renamed to Finfun, right? (I'd like to be consistent with mathlib's style here.)
• We're currently a bit inconsistent in assuming that the codomain type has a Zero. I think we should switch to assuming it early-on, as in Finsupp (and coincidentially my textbook on choreographic languages, which is the original reason for FinFun anyway). Agreed? This will make a lot of stuff easier and more useful.
• Given the above, should we rename it to something that signals the Zero assumption?
• What notation should we use? I dislike the current ⇀, and like the one Finsupp uses, but alas that means the latter is already taken.

[Tristan Figueroa-Reid]

If you do want to reuse DFinsupp's theory, perhaps you can define this structure as the non-dependently typed version of DFinsupp (def FinFun (α : Type*) (M : Type*) [Zero M] := Π₀ (_ : α), M)?

(I think it's FinFun? Lean does use PascalCase for structures, which makes me surprised by Finsupp's name)

[Fabrizio Montesi]

Maybe. In principle that'd be fine, but DFinsupp looks pretty complex (certainly for good reasons) to know at a glance.

[x.y.]

Fabrizio Montesi said:

Let's see where we can go with FinFun then. A few initial questions:

• I guess it should be renamed to Finfun, right? (I'd like to be consistent with mathlib's style here.)
• We're currently a bit inconsistent in assuming that the codomain type has a Zero. I think we should switch to assuming it early-on, as in Finsupp (and coincidentially my textbook on choreographic languages, which is the original reason for FinFun anyway). Agreed? This will make a lot of stuff easier and more useful.
• Given the above, should we rename it to something that signals the Zero assumption?
• What notation should we use? I dislike the current ⇀, and like the one Finsupp uses, but alas that means the latter is already taken.

Re 0. Agree with Finfun
Re 1. Yes I think so
Re 2. I’m not sure, I kind of like it means a function with finite domain…
Re 3. One option would be \to_f?

[Fabrizio Montesi]

Unfortunately I couldn't find subscript f in unicode :(

[Kim Morrison]

I have an alternative computation focused implementation for finitely supported functions (based on HashMap, actually ExtHashMap, plus a wrapper layer that ensures there are no default values stored in the map). It should be completely computable and as performant as the underlying HashMap... I'm busy with other things, but hoping to ship it as a demo of how to build APIs using grind.

[Fabrizio Montesi]

Kim Morrison said:

I have an alternative computation focused implementation for finitely supported functions (based on HashMap, actually ExtHashMap, plus a wrapper layer that ensures there are no default values stored in the map). It should be completely computable and as performant as the underlying HashMap... I'm busy with other things, but hoping to ship it as a demo of how to build APIs using grind.

Yes please!! :)

Where do you plan on having that? Is it gonna be compatible with Finset?

[x.y.]

Fabrizio Montesi said:

Unfortunately I couldn't find subscript f in unicode :(

What about \to^f, iirc there is a superscript f?

[Fabrizio Montesi]

Mmh, actually, there's a relevant difference between FinFun and Finsupp: in FinFun, we don't take the support as parameter, but rather the domain of definition. So it's perfectly fine to have f x = 0 even if x is in dom. We're just interested in f x necessarily being 0 if x is not in dom.

[Eric Wieser]

Isn't that still docs#DFinsupp ?

[Eric Wieser]

Could you share a link to where FinFun is defined?

[Fabrizio Montesi]

ah, yet another difference between Finsupp and DFinsupp :-)

[Fabrizio Montesi]

https://github.com/cs-lean/cslib/blob/main/Cslib/Data/FinFun.lean

[Eric Wieser]

Ah, FinFun does not have good extensionality

[Eric Wieser]

I guess FinFun is to DFinsupp as HashMap is to ExtHashMap

[Fabrizio Montesi]

I think my current edits might fix that, it's currently a bit messy.

[Fabrizio Montesi]

In particular I'm making a new branch based on this for discussing it:

/-- A finite function is a function `f` equipped with a domain of definition `dom`. -/
structure FinFun (α : Type u) (β : Type v) [Zero β] where
  f : α → β
  dom : Finset α
  dom_complete : ∀ x, x ∉ dom → f x = 0

[Eric Wieser]

That's better, but the function {f := 0, dom:=empty} is still not equal to {f := 0, dom:=univ}

[Eric Wieser]

And so you can't say "two FinFun's are equal if they agree everywhere"

[Fabrizio Montesi]

Ah, extensional equality! Of course, I agree.

[Eric Wieser]

Once you fix that, you've either reinvented Finsupp (by changing the implies to an Iff) or DFinsupp (by quotienting out the dom)

[Eric Wieser]

(strictly speaking DFinsupp uses Multiset not Finset, which in practice often avoids needing [DecidableEq α])

[Fabrizio Montesi]

Eric Wieser said:

(strictly speaking DFinsupp uses Multiset not Finset, which in practice often avoids needing [DecidableEq α])

! I was actually wondering why Multiset.

[Fabrizio Montesi]

Eric Wieser said:

Once you fix that, you've either reinvented Finsupp (by changing the implies to an Iff) or DFinsupp (by quotienting out the dom)

The former.

mathematical mumbling sounds ensue

[Eric Wieser]

The problem with using an Iff is that you quickly end up needing decidability of (x : β) = 0 to know whether to remove things from dom

[Eric Wieser]

Whereas for DFinsupp you can happily keep growing your dom/support, as the quotient makes it irrelevant

[Fabrizio Montesi]

Exactly, which now makes me understand your comment about FinFun, HashMap and ExtHashMap. I'm not familiar with ExtHashMap but the names are telling enough, from your comments. (And I agree with you.)

[Eric Wieser]

In particular I'm making a new branch based on this for discussing it:

The version you have in this message is a little more faithful to the HashMap : ExtHashMap comparison

[Fabrizio Montesi]

(deleted)

[Fabrizio Montesi]

(deleted)

[Fabrizio Montesi]

A few 'uh, oh!' later (my deleted mesgs above), I'm starting to see how we could make it work with the iff in our project. That'd mean that we basically want Finsupp without all these noncomputable, I guess, getting back to my first messages.

[Eric Wieser]

I would wager that DFinsupp would work just as well for you, and you'd save yourself the effort of having to rewrite bits of Finsupp locally

[Fabrizio Montesi]

Oh, I definitely agree. As I mentioned before, I'm just worried about exposing the user to the complexity of DFinsupp by defining FinFun as a DFinSupp as @Tristan Figueroa-Reid suggested before:

def FinFun (α : Type*) (M : Type*) [Zero M] := Π₀ (_ : α), M

[Fabrizio Montesi]

but I'll play a bit with this idea, maybe the ergonomics will actually work out

[Fabrizio Montesi]

I can get very motivated by avoiding duplications. ;-)

[Fabrizio Montesi]

Re that Trunc: will I be able to compute 'intersections' and 'unions' as I can do with Finset as support?

[Eric Wieser]

Ultimately you'll want to use docs#Quotient.map₂, or if you're lucky the Trunc version already exists

[Eric Wieser]

docs#DFinsupp.zipWith is the union

[Eric Wieser]

Arguably you don't need the intersection, since under the quotient they're the same anyway

[Fabrizio Montesi]

Just to make sure we're on the same page: what I meant is that I wanna construct f from g and h (all DFinsupp) such that the support of f is the intersection of the supports of g and h (all the stuff not in the intersection of the supports gets mapped to 0).

[Fabrizio Montesi]

maybe there's ⊓ for that somewhere?

[Eric Wieser]

What do you want the function to be in that case?

[Eric Wieser]

You can of course implement that as

DFinsupp.zipWith f g fun i fi gi => if fi = 0 then 0 else if gi = 0 then 0 else sorry

but if your sorry is fi * gi then of course you can just drop the if

[Fabrizio Montesi]

I guess point-wise application of ⊓? I.e., f x = g x ⊓ h x for all x in g.support \cap h.support and 0 otherwise.

[Eric Wieser]

That's f ⊓ g I think

[Eric Wieser]

Are you sure you want the 0 otherwise bit, rather than just having f x = g x ⊓ h x everywhere?

[Eric Wieser]

If you have 0 ⊓ f x = 0 etc then those are the same thing anyway

[Eric Wieser]

docs#DFinsupp.support_inf is relevant

[Fabrizio Montesi]

Eric Wieser said:

docs#DFinsupp.support_inf is relevant

It is, thanks! Isn't that basically what I wrote?

Re what I want: I'm not 100% sure yet, lots of stuff to double check. I apologise in advance for changing my mind. :grinning_face_with_smiling_eyes:

[Matt Diamond]

is this supposed to capture the notion of partial functions? it seems similar to docs#PFun, conceptually speaking (though that type does not require that the domain is finite)

[Fabrizio Montesi]

Yes, with finite domain of definition. I'd be just happy with a Finsupp implemented in the style of DFinsupp. :⁠-⁠)

[Matt Diamond]

just to be clear, DFinsupp also requires that values in the support are nonzero (it seemed like there was some confusion on that point above)

[Fabrizio Montesi]

Yes, but I think that's fine (after re-checking my pen-and-paper proofs for the 3rd time..)

[Eric Wieser]

I would guess that just making arrow notation for Π₀ (_ : α), M would be sufficient for your use-case

[Eric Wieser]

Using def FinFun just forces you to reinvent all the same wheels

[Fabrizio Montesi]

Eric Wieser said:

I would guess that just making arrow notation for Π₀ (_ : α), M would be sufficient for your use-case

Yes, that's what I'm playing with now. The def FinFun approach turned out to be cumbersome, as you say.

[Fabrizio Montesi]

I've done an intermediate step towards that (cslib#118), as switching directly to DFinsupp broke way too much downstream code. But at least this will make downstream code go more in line with the APIs of Finsupp/DFinsupp. We'll keep working in that direction. :)

[Fabrizio Montesi]

I didn't expect grind to be able to prove this, nice work annotating stuff everyone. :-)

@[scoped grind =]
theorem fromFun_inter [Zero β] [DecidableEq α]
    [∀ y : β, Decidable (y = 0)] {f : α → β} {support1 support2 : Finset α} :
    (f ↾ support1) ↾ support2 = f ↾ (support1 ∩ support2) := by grind