Bas Spitters (May 10 2024 at 11:49): Bas Spitters (May 10 2024 at 11:49):Lean mathlib has a deep type class hierarchy. I understand they only use (tabled) type classes.
Why does one need HB, canonical structures and type classes in Coq?
I could not find this in the papers by @Cyril Cohen @Assia Mahboubi @Enrico Tassi and the other experts here.
Reynald Affeldt (May 10 2024 at 12:13):I am not an expert but I think that the conclusion of the HB paper (https://drops.dagstuhl.de/storage/00lipics/lipics-vol167-fscd2020/LIPIcs.FSCD.2020.34/LIPIcs.FSCD.2020.34.pdf) contains some hints
Enrico Tassi (May 10 2024 at 12:15):HB is a language, it currently target CS, although Cyril did some experiments to target TC. Together with @Davide F we are rewriting a TC engine based on Elpi, and hopefully add memoization (tabling) to Elpi. This is somewhat a plan to make the question TC vs CS mooth.
The advantage of having a language dedicated to library structuring is That you can do a bit more. You can static check for ambiguous inference, write specific tools such as HB.howto, HB.about, HB.export or HB.graph, and finally define the contact surface of clients: HB.factory and HB.builders let one change the hierarchy without breaking user code.
HB is just sugar, of course you can do the same without, but the cost is higher....
Reynald Affeldt (May 10 2024 at 12:18):I was about to mention the detection of competing inheritance paths by HB that is an issue that is independent of whether it is implemented using CS and TC (https://link.springer.com/chapter/10.1007/978-3-030-51054-1_1).
Reynald Affeldt (May 10 2024 at 12:19):About differences between CS and TC there is also Sakaguchi-san's paper: https://arxiv.org/pdf/2002.00620
Pierre Roux (May 10 2024 at 13:12):And if you want to learn about the difficulties faced by mathlib, not having something like HB, you can read https://arxiv.org/pdf/2202.01629
Bas Spitters (May 10 2024 at 13:25):@Pierre Roux Thanks for reminding me about that paper. Do you know whether anything changed in the move to lean4?
Pierre Roux (May 10 2024 at 13:30):I'm not aware of any dramatic change.
Last updated: Oct 13 2024 at 01:02 UTC