Coq：类型类与依赖记录(Coq: typeclasses vs dependent records)

 我无法理解Coq中类型类和依赖记录之间的区别。 参考手册给出了类型类的语法，但没有说明它们到底是什么以及如何使用它们。 一些思考和搜索揭示了类型类本质上是具有一些语法糖的依赖记录，允许Coq自动推断一些隐式实例和参数。 似乎类型数组的算法在任何给定的上下文中只有一个或多或少一个可能的实例时效果更好，但这不是一个大问题，因为我们总是可以将类型类的所有字段移动到它的参数，消除歧义。 此外， Instance声明会自动添加到Hints数据库中，这通常可以简化证明，但如果实例过于笼统并导致证明搜索循环或爆炸，有时也会破坏它们。 还有其他我应该注意的问题吗？ 在两者之间进行选择的启发式是什么？ 例如，如果我只使用记录并尽可能将其实例设置为隐式参数，我会失去任何东西吗？ 

I can't understand the difference between typeclasses and dependent records in Coq. The reference manual gives the syntax of typeclasses, but says nothing about what they really are and how should you use them. A bit of thinking and searching reveals that typeclasses essentially are dependent records with a bit of syntactic sugar that allows Coq to automatically infer some implicit instances and parameters. It seems that the algorithm for typeclasses works better when there is more or a less only one possible instance of it in any given context, but that's not a big issue since we can always move all fields of typeclass to its parameters, removing ambiguity. Also the Instance declaration is automatically added to the Hints database which can often ease the proofs but will also sometimes break them, if the instances were too general and caused proof search loops or explosions. Are there any other issues I should be aware of? What is the heuristic for choosing between the two? E.g. would I lose anything if I use only records and set their instances as implicit parameters whenever possible?

原文：https://stackoverflow.com/questions/29872260