Stream: math-comp users

Topic: Two versions of the same data structure


view this post on Zulip Ricardo (Feb 22 2023 at 15:39):

Hi everyone. Hope you're all well. I have a data structure for graph homomorphisms like

Record hom (S N : choiceType) : Type :=
  Hom { dom : graph S N
      ; cod : graph S N
      ; f_sites : {fmap S -> S}
      ; f_nodes : {fmap N -> N}
      ; property1 : ...
    }.

Then all the homomorphims that share the codomain are the objects of a comma category. That's why I'd like to parameterise some homomorphisms over their codomain like

Record cHom (S N : choiceType) (cod : graph S N) : Type :=
  CHom { dom : graph S N
       ; f_sites : {fmap S -> S}
       ; f_nodes : {fmap N -> N}
       ; property1 : ...
     }.

so that I can write functions like

Definition cmatch S N (C : graph S N) (a b : cHom S N C) := ...

I could also write cHom like

Record cHom (S N : choiceType) (C : graph S N) : Type :=
  CHom { h :> hom S N
       ; codEcod : cod h = C
     }.

But I'm not sure what would be the advantages or disadvantages of each approach. What do you think would be a good way to share the theory for hom and cHom?

view this post on Zulip Paolo Giarrusso (Feb 22 2023 at 17:18):

Can you define hom in terms of cHom rather than the opposite?

view this post on Zulip Paolo Giarrusso (Feb 22 2023 at 17:19):

very roughly sth like

Record Hom S N := {
  dom : graph S N
  cod : graph S N
  graph : cHom S N dom cod
}.

view this post on Zulip Paolo Giarrusso (Feb 22 2023 at 17:20):

the upside is that instead of codEcod, you just never introduce two codomains that must be equal — which is the best way to replace propositional equalities by definitional ones

view this post on Zulip Paolo Giarrusso (Feb 22 2023 at 17:21):

I did this for both cod and dom not because it's necessary but because it seems more natural, might come up later, and this is of course somewhat invasive on the existing theory

view this post on Zulip Ricardo (Feb 22 2023 at 17:36):

Paolo Giarrusso said:

the upside is that instead of codEcod, you just never introduce two codomains that must be equal — which is the best way to replace propositional equalities by definitional ones

Yes, that's why I stopped. I knew that propositional equality would be a pain later on and there had to be a better way. Thank you @Paolo Giarrusso for the suggestion.

view this post on Zulip Ricardo (Feb 23 2023 at 02:08):

Your idea @Paolo Giarrusso of having both dom and cod as parameters has been increadibly useful. Together with having finfuns instead of finmaps for f_sites and f_nodes have made the proofs much shorter and clearer. Thank you.

view this post on Zulip Paolo Giarrusso (Feb 23 2023 at 02:18):

I haven't done so much but I'm happy it helped! For some context: "Bundling" and "unbundling" components are relatively common and general refactorings: bundling turns indexes/parameters into record members, and unbundling does the opposite. I've learned the idea from https://arxiv.org/abs/1102.1323 (even if their application to overloading, or algebraic hierarchies like math-comp, has significant performance problems at scale)

view this post on Zulip Ricardo (Feb 23 2023 at 03:11):

Yes. I read their paper when I started this project and even though their proposal seemed very compelling, their performance issues and the fact that I didn't find much documentation nor supporting libraries for that type of programming made me backtrack and search for other alternatives. Another paper I found interesting was the one by @Jason Gross https://arxiv.org/abs/1401.7694 but using HoTT scared me because I don't understand it yet.

view this post on Zulip Ali Caglayan (Feb 26 2023 at 19:15):

You may be interested in https://github.com/jwiegley/category-theory which uses similar ideas to Jason's library (such as uni polymorphism and avoidance of prop etc). That is compatible with regular Coq developments.

view this post on Zulip Ali Caglayan (Feb 26 2023 at 19:16):

The use of HoTT in Jason's library isn't particularly important for most things, but it does let you derive extensionality principles like isos ~ equalities. In practice however, this does not matter much in my experience.

view this post on Zulip Ricardo (Feb 26 2023 at 22:47):

Thank you @Ali Caglayan. Question: why would one want to avoid prop? Question 2: Uni polymorphism is universe polymorphism?

view this post on Zulip Ali Caglayan (Feb 26 2023 at 22:53):

HoTT has it's own reasons for avoiding prop (incompabibility with univalence) but the main reason it is avoided here is that it generalizes nicely. You could develop a whole theory about prop valued relations, but then you need to repeat a lot for homs (since they might be type valued). Then it is typically better to do type valued stuff from the begining. Same for Coq Ensembles vs presheaves.

See the reasons for the category-theory library here: https://github.com/jwiegley/category-theory/#design-decisions

view this post on Zulip Ricardo (Feb 27 2023 at 02:28):

I see. Thank you :smile:


Last updated: Jul 25 2024 at 15:02 UTC