约束包是如何工作的？

Posted 2023-05-08

【中文标题】约束包是如何工作的？

【英文标题】：How does the constraints package work?

【发布时间】：2012-09-25 13:00:19

【问题描述】：

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

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

【参考方案1】：

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

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

但鉴于您无法在模块外部明确引用这些类型，因为它们没有被导出，因此必须对涵盖这些 Skolem 的任何实例进行普遍量化。

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

【讨论】：

谢谢。你能展示一下你所说的技巧吗？另外，您是否有证据（或令人信服的论点）证明两个变量就足够了？

我看看能不能把它挖出来。这只是我在编写相关代码时猛烈抨击的一个简单示例。 “令人信服的论点”只是我想出的 hack 不起作用，而且我能想出的任何草图都可能看穿它，这将是太多的工作来测试。使用足够的 Oleggery 来解决这两个变量的解决方案很可能是可能的，但您几乎可以肯定需要一些非常重型的机器来完成它。 ;)

即兴发挥，最简单的例子归结为使用类和fundep。请记住，您可以拥有class Foo a b | a -> b, b -> a，那么如果您对Foo a a 的第二个参数进行“量化”，则其第二个参数不是参数化的，即使您可以使用Skolem A 实例化第二个参数。但是当你使用两种类型时，fundep 技巧不再起作用，因为现在对两者的要求 (Foo A A, Foo A B) 打败了fundep。

所以两个变量足以击败这个相当明显的攻击途径。不过，我没有证据证明这是唯一的攻击媒介。很可能构建一个将约束作为参数和另一个参数的类，并在它们之间有一些复杂的fundep链，以某种方式公开足够的信息以允许您区分Skolem。但是，这样的构造可能至少需要重叠/不连贯的实例。