约束包如何工作？ [英] How does the constraints package work?

问题描述

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

1. 为什么我们需要两个skolem变量 - A和B？我会想象，如果一个约束满足未知类型，那么它是多态的。第二种类型如何提高安全性？


2. 为什么这些类型称为skolem变量？我认为使用搜索是为了消除存在量化，在这里我们看到了普遍量化。是否有一个符号翻转的地方，我错过了？

解决方案

和函数依赖关系，通过使用约束上的参数化约束来确定Skolem是否为单个变量。我曾经这样做的技巧在有两种情况时不起作用。

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

但是，由于不能导出，所以不能在模块外明确引用这些类型，涵盖这些Skolems必须被普遍量化。

这就是我从存在到现实的升级。 '标志翻转'来自他们的未报告性质，而不是技术上来自他们作为Skolems的角色。

The idea behind Data.Constraint.Forall, as I understand it, is to use coercion in the implementation, but ensure safety using the type system. I have two questions regarding the latter.

1. Why do we need two skolem variables — A and B? I would imagine that if a constraint is satisfied by an «unknown» type, then it is polymorphic. How does the second type give more safety?
2. Why are these types called skolem variables? I thought that skolemnization is used to remove existential quantification, and here we see universal quantification. Is there a sign-flipping somewhere which I missed?

解决方案

It is possible with an MPTC and functional dependency to identify the Skolem when it is a single variable, by using a constraint parameterized on a constraint. The trick I used to do that doesn't work when there are two.

From the perspective of code written outside of this module, the variables are Skolemized. They are effectively a 'fresh' type constructor.

But given that you can't refer explicitly to these types outside of the module since they aren't exported, any instance that covers these Skolems has to be universally quantified.

This is how I upgrade from an existential to a universal. The 'sign flip' comes from their unexported nature, not technically from their role as Skolems.

这篇关于约束包如何工作？的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！