Cli*_*ton 5 haskell equality type-families
如何编写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).