Théo Zimmermann (May 22 2020 at 07:38): Théo Zimmermann (May 22 2020 at 07:38):What do you think of Hierachy Builder (https://github.com/math-comp/hierarchy-builder). Is this something that you could use in your own projects? Is it something that we could recommend blindly to mathematician newcomers?
Ralf Jung (May 22 2020 at 07:41):I dont know much about it. From what @Robbert Krebbers says, it is basically a generalization of what math-comp/ssreflect are doing?
Ralf Jung (May 22 2020 at 07:42):unfortunately their approach doesn't work for us because we need the hierarchy to interact well with typeclasses, and the unification algorithm that typeclasses use is incompatible with ssreflect heirarchies. that's okay for them as they use their own apply: tactic everywhere which uses the new(er) unification, and they dont use type classes at all. but we are mixing canonical structures and typeclasses (for various reasons, one of them being entirely out of our control: Proper instances so we can rewrite -- ssreflect uses normal = everywhere but we really need setoids), and so we have no choice, things have to work with old unification.
Ralf Jung (May 22 2020 at 07:42):so we had to heavily tweak their approach to make it work "most of the time", and even then about once a month we discover a situation where one of our instances doesnt fire and using apply: instead makes it work. it is quite painful.
Ralf Jung (May 22 2020 at 07:45):so based on that @Théo Zimmermann I would answer your question about recommending it blindly with "no". there are some major caveats.
Théo Zimmermann (May 22 2020 at 07:47):OK, thanks! Indeed, the incompatibility with setoid rewrite is quite a bummer given how important the latter is (especially to mathematicians who are used to work with quotients).
Ralf Jung (May 22 2020 at 07:51):correspondingly, https://github.com/coq/coq/issues/6294 is easily #1 on the list of coq bugs that we'd really like to see fixed.^^ (but yes I know it's a really hard problem.)
Enrico Tassi (May 22 2020 at 08:33):@Cyril Cohen @Kazuhiko Sakaguchi you may be interested in the points made by Ralf. Can we do something to make HB more setoid friendly? (apart from reimplementing setoids...)
Enrico Tassi (May 22 2020 at 08:37):@Ralf Jung is setoids the only issue you have? I imagine it is because of binders in Iris, am I correct? ("newcomer mathematician" -> "needs setoids" seems a quite strong assumption to me, this is why I'm asking for more details)
Janno (May 22 2020 at 08:38):BTW: I tried porting the iris hierarchy to the hierarchy builder to see what whould happen but a) it really doesn't do type class resolution (so the field types are basically the Set Printing All output of the original version) and b) after some fields it just started reporting internal errors to me. I might still have the branch somewhere.. I should probably report bugs?
Ralf Jung (May 22 2020 at 08:41):Enrico Tassi said:
Ralf Jung is setoids the only issue you have? I imagine it is because of binders in Iris, am I correct? ("newcomer mathematician" -> "needs setoids" seems a quite strong assumption to me, this is why I'm asking for more details)
we use typeclasses for a lot of things, not just setoids. setoids is just the thing we control least.^^
not sure what you mean by binders here. iris has tons of objects where Coq's = is just not the right notion of equality, we need something more extensional. on top of that we use step-indexing which gives rise to a family dist: nat -> T -> T -> Prop of equivalence relations, and we also need good support for rewriting with dist n.
Enrico Tassi (May 22 2020 at 08:42):@Janno Please open an issue about your porting experience, it can be interesting to us developing it. HB does nothing about type classes, nothing at all, so it is not clear to me what you expect.
Enrico Tassi (May 22 2020 at 08:42):(maybe we should move these messages in the HB stream)
Janno (May 22 2020 at 08:43):(Is there such a stream?)
Théo Zimmermann (May 22 2020 at 10:56):There is!
Notification Bot (May 22 2020 at 10:58):This topic was moved here from #Coq users > Hierarchy builders and type classes by Théo Zimmermann
Cyril Cohen (May 23 2020 at 01:00):Enrico Tassi said:
Cyril Cohen Kazuhiko Sakaguchi you may be interested in the points made by Ralf. Can we do something to make HB more setoid friendly? (apart from reimplementing setoids...)
I am not sure there would be an issue with setoid. HB only handles hierarchies themselves, fields can be anything, in particular a setoid equality that you can base instances of Proper on, I think.
Interaction issues between canonical structures and typeclasses appear mainly when you rely on both of them at the same time to infer one object. If it happens with HB, I am curious to see how exactly...
Ralf Jung (May 29 2020 at 11:58):@Cyril Cohen
I am not sure there would be an issue with setoid. HB only handles hierarchies themselves, fields can be anything, in particular a setoid equality that you can base instances of Proper on, I think.
as mentioned before, the issue with this is that TC search is unable to apply many lemmas whose statement involves canonical structures, including in some cases the projections of the structures themselves.
Ralf Jung (May 29 2020 at 11:59):the only reason ssreflect works at all is that they use apply: instead of apply
Ralf Jung (May 29 2020 at 11:59):this is a long-standing problem in Coq's unification algorithm (https://github.com/coq/coq/issues/6294)
Bas Spitters (Dec 08 2021 at 12:54):What is the status of the hierarchy builder and type classes? Did anyone experiment? Is there a detailed proposal on what to do?
Bas Spitters (Dec 08 2021 at 12:58):@Janno Did you ever write down your experience?
@Enrico Tassi @Cyril Cohen @Kazuhiko Sakaguchi you write:
We believe it would take a minor coding effort to retarget HB to another bundling approach.
https://hal.inria.fr/hal-02478907v5/document
Is more information available?
Enrico Tassi (Dec 08 2021 at 13:06):We did not try. I still think it would not be too hard, but my priority is to have math-comp be ported to HB. We are getting close, but we are not there yet. For example we managed to compile the odd order theorem on top of MC+HB, but we still have some performance issues to solve before declaring victory.
If you really want TC support in HB, we happily accept contributions ;-)
Bas Spitters (Dec 08 2021 at 14:59):We could try to have a look at it, but it would be good to have some guidance on the "minor coding effort".
Last updated: Jan 29 2023 at 16:02 UTC