我无法理解Coq中类型类和依赖记录之间的区别.参考手册给出了类型类的语法,但没有说明它们到底是什么以及如何使用它们.一些思考和搜索揭示了类型类本质上是具有一些语法糖的依赖记录,允许Coq自动推断一些隐式实例和参数.当在任何给定的上下文中只有一个或多或少的一个可能的实例时,似乎类型类的算法工作得更好,但这不是一个大问题,因为我们总是可以将类型类的所有字段移动到它的参数,消除歧义.此Instance声明也会自动添加到Hints数据库中,这通常可以简化证明,但如果实例过于笼统并导致证据搜索循环或爆炸,有时也会破坏它们.还有其他我应该注意的问题吗？在两者之间进行选择的启发式是什么？例如,如果我只使用记录并尽可能将其实例设置为隐式参数,我会失去任何东西吗？
假设我有一组函数,每个函数都可以依赖于一个或两个隐式变量A B: Type.我怎么指定这个？即将这些变量添加到它们的变量列表中并将它们设置为隐式变量.
最明显的方法是添加{A B: Type}到他们的定义中.然而,在现实生活和中等复杂的发展中,这些共享的隐含列表很容易就是6-10个条目,并且包括复杂的类型,因此使得函数定义难以阅读,甚至更难理解它们的相似性或对所提到的类型进行更改.因此,该解决方案不适用.
我可以在一个部分或模块中包含所有函数并Variables (A B: Type) etc在开头写入,但这不会使变量隐含,我将不得不在部分末尾手动设置所有函数的参数.更糟糕的是,这将使所有变量共享.即如果我宣布
Section sect.
Variable A B: Type.
Definition f (t: A -> Type) := (..).
Definition g (t: A -> Type) (s: B -> Type) := G (f t) (f s).
End sect.
(G是一些双变量函数)然后g不会被接受,因为s不存在A -> Type,即使基本上f只需要一个任意类型的族.
我可以制作一个部分并宣布Context {A B: Type}.这将使这些变量隐含在所有函数中,但是像以前一样的共享问题仍将存在.因此,我必须随意将我的函数分成几个部分,以便我可以使用隐式参数的不同值来调用Sect.1中的函数.这很有效,但很难看,而且我可以很容易地想象出每个部分都必须有2-3个函数才能正常调用它们的情况.
有更好的解决方案吗？