#TypeTheory: why does unbundling seem to never come up when discussing #Agda typeclasses? It seems to me the problem would apply in Agda as well as in Coq eelis.net/research/math-.
Tagging because he must have informed opinions on this...
Conversation
Note that typeclasses are used very little in Agda. And the problem, shifted to encoding theories as records, still occurs. There's just a sweet-spot obtained by making the carrier and functions parameters to the bundle of properties that works pretty well.
2
2
It seems to occur more in Coq because of trying to get the system to infer a lot for you. There is a style difference that seems to really push on this problem hard. It might be a scale thing too: Coq's math-comp is way larger than the Algebra library in Agda.
1
2
IIRC it comes up in Lean's mathlib, which is quite large. I thought I heard it mentioned by one of the students in their presentation on it, but I could be misremembering.
Tom Hales complains about it, cogently. We quote & cite him as motivation in our paper. I think Lean's mathlib has chosen a different point in the design space of bundling/unbundling, which I think is farther from a sweat spot.
1
1
Of course, it's easily fixed by some meta-programming. Lean's is only on proofs right now, but if it gained a "declaration monad" (instead of just a tactic one), that problem is easily solved.
1
2
Show replies