约束包如何工作？

Question

根据我的理解,Data.Constraint.Forall背后的想法是在实现中使用强制,但使用类型系统确保安全性.我对后者有两个问题.

1. 为什么我们需要两个skolem变量--A和B？我想如果一个约束被一个"未知"类型满足,那么它就是多态的.第二种类型如何提高安全性？
2. 为什么这些类型称为skolem变量？我认为石油化用于去除存在量化,在这里我们看到普遍量化.我错过了哪个标志翻转？

Answer 1

通过使用在约束上参数化的约束,使用MPTC和函数依赖可以在Skolem是单个变量时识别Skolem.我曾经这样做的技巧在有两个时不起作用.

从在该模块外部编写的代码的角度来看,变量是 Skolemized.它们实际上是一种"新鲜"类型的构造函数.

但鉴于您不能在模块外部明确引用这些类型,因为它们不会被导出,因此任何涵盖这些Skolems的实例都必须进行普遍量化.

这就是我从存在主义升级到普遍主义的方式."标志翻转"来自于他们未被移植的本质,而不是技术上来自他们作为Skolems的角色.