约束包如何工作？

背后Data.Constraint.Forall的想法，我的理解，就是用强制的执行，但要确保使用类型系统的安全。关于后者我有两个问题。约束包如何工作？

为什么我们需要两个skolem变量 - A和B？我会想象，如果一个约束满足“未知”类型，那么它是多态的。第二种类型如何提高安全性？
为什么这些类型称为斯科伦变量？我认为使用搜索是为了消除存在量化，在这里我们看到了普遍量化。有什么迹象表明我错过了什么地方？

来源

2012-10-04 Roman Cheplyaka

通过使用在约束上参数化的约束，使用MPTC和函数依赖性可以确定Skolem是单个变量的情况。我曾经这样做的伎俩在有两个时不起作用。

从本模块外编写代码的角度来看，变量为 Skolemized。他们实际上是一个'新鲜'类型的构造函数。

但考虑到你不能明确提及这些类型的模块之外，因为他们没有出口，覆盖这些Skolems任何实例必须是普遍的量化。

这是我从生存升级到通用。 '标志翻转'来自它们的未报告性质，而不是技术上来自其作为Skolems的角色。

来源

2012-10-04 15:19:05

感谢。你可以展示你在谈论的技巧吗？另外，你是否有证据（或有说服力的论点）有两个变量就足够了？ –

我会看看我是否可以挖掘它。这只是我写代码时遇到的一个简单例子。 “令人信服的论点”就是我所提出的黑客行为并不奏效，而我所能想到的任何素描都可能通过它进行测试，这将是太多的工作来测试。如果有足够的Oleggery来解决这两个可变的解决方案，那么很可能会有这种可能性，但是您几乎可以肯定需要一些相当重的机器来完成这项工作。 ;） –

关闭袖口，最简单的例子归结为使用类和fundep。记住你可以有'Foo a b'类A - > B，B - >了'，然后如果你“量化”过富的'的第二个参数中了'在它的第二个参数不是参数化的，尽管你可以实例与斯科伦'A'是第二个参数。但是当你使用两种类型时，fundep技巧不再有效，因为现在对'（Foo A A，Foo A B）'的要求击败了fundep。 –

约束包如何工作？

回答

相关问题