haskell - 全部约束

Question

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

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

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

Answer 1

是的，这可以使用 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) .