haskell - 全面的约束

如何编写forall约束，例如对于某些类型族F和G:

forall x y. G (F x y) ~ (x, y)

是否可以使用Edward A. Kmett的 Constraints 软件包？如果可以的话，可以提供一个小例子吗？我想我需要使用Forall。

最佳答案

是的，可以使用constraints来实现。但是要小心!如果类型族不是平凡的，那么您声称的等式不太可能拥有足够的constraints通用性。尤其要考虑当x和y被卡住的类型族时，类型族是否成功减少

type family X where {}
type family Y where {}

另外，我看到您特别想要的约束没有任何自由变量。希望这只是一个例子。像这样的实际封闭约束不太可能有用。
Data.Constraint.Forall中的基本类型族是Forall。使用ForallT可以更方便地处理这个特定示例，但是了解如何使用Forall最为重要。

通常，Forall p表示forall x . p x。听起来不太一般，但实际上是这样，如果您逐步构建p的话。你追求

forall x y. G (F x y) ~ (x, y)

首先定义一个表示您所寻求的关系的类。

class G (F x y) ~ (x, y) => C x y
instance G (F x y) ~ (x, y) => C x y

现在，您可以逐步进行操作，定义

class Forall (C x) => D x
instance Forall (C x) => D x

(您可以将其读取为D x = forall y . C x y)

然后使用Forall D(即forall x . D x)来表达您的约束。您将需要使用inst来获取Dict (D x)，并再次使用来获得Dict (C x y)。

关于haskell - 全面的约束，我们在Stack Overflow上找到一个类似的问题：https://stackoverflow.com/questions/38945644/