haskell - 约束包是如何工作的？

Question

据我了解， Data.Constraint.Forall背后的想法是在实现中使用强制，但使用类型系统确保安全。关于后者，我有两个问题。

1. 为什么我们需要两个 skolem 变量——A 和 B？我想如果一个“未知”类型满足一个约束，那么它就是多态的。第二种类型如何提供更多安全性？
2. 为什么这些类型被称为 skolem 变量？我认为skolemnization是用来去除存在量化的，这里我们看到了全称量化。我错过了某个地方的标志翻转吗？

Answer 1

当 Skolem 是单个变量时，可以使用 MPTC 和函数依赖来识别 Skolem，方法是使用在约束上参数化的约束。当有两个时，我曾经这样做的技巧不起作用。

从在此模块之外编写的代码的角度来看，变量是Skolemized。它们实际上是一个“新鲜”类型的构造函数。

但是鉴于您不能在模块之外明确引用这些类型，因为它们没有被导出，任何涵盖这些 Skolems 的实例都必须被普遍量化。

这就是我从存在主义升级到普遍主义的方式。“标志翻转”来自他们未出口的性质，而不是技术上他们作为 Skolems 的角色。