通过包容来减弱乙烯基的RecAll约束
在乙烯基库中，有一个RecAll类型的家族，让我们要求对于类型级别列表中的每个类型，部分应用的约束条件是真实的。 例如，我们可以这样写：
myShowFunc :: RecAll f rs Show => Rec f rs -> String
这一切都很可爱。 现在，如果我们有约束RecAll f rs c ，其中c未知，并且我们知道cx需要dx （从ekmett的contstraints包中借用语言），那么我们如何才能获得RecAll f rs d ？
我问的原因是我正在处理一些需要满足几个类型类约束的函数中的记录。 为此，我使用存在包中Control.Constraints.Combine模块的:&: combinator。 （注意：如果你安装了其他东西，那么这个包就不会生成，因为它依赖于一个超旧版本的contravariant ，你可以复制我提到过的一个模块。）这样，我可以得到一些非常漂亮的约束条件尽量减少typeclass烤盘。 例如：
RecAll f rs (TypeableKey :&: FromJSON :&: TypeableVal) => Rec f rs -> Value
但是，在这个函数体内，我调用另一个需要较弱约束的函数。 它可能看起来像这样：
RecAll f rs (TypeableKey :&: TypeableVal) => Rec f rs -> Value
GHC看不到第一条第二条声明。 我认为情况会是这样。 我无法看到的是如何证明它的意义，并帮助GHC出来。 到目前为止，我有这样的：
import Data.Constraint
weakenAnd1 :: ((a :&: b) c) :- a c
weakenAnd1 = Sub Dict -- not the Dict from vinyl. ekmett's Dict.
weakenAnd2 :: ((a :&: b) c) :- b c
weakenAnd2 = Sub Dict
这些工作正常。 但是，这是我卡住的地方：
-- The two Proxy args are to stop GHC from complaining about AmbiguousTypes
weakenRecAll :: Proxy f -> Proxy rs -> (a c :- b c) -> (RecAll f rs a :- RecAll f rs b)
weakenRecAll _ _ (Sub Dict) = Sub Dict
这不会编译。 有谁知道一种方法来获得我期待的效果。 如果他们有帮助，这里是错误。 此外，我有Dict作为我的实际代码中的限定导入，所以这就是为什么它提到Constraint.Dict ：
Table.hs:76:23:
Could not deduce (a c) arising from a pattern
Relevant bindings include
weakenRecAll :: Proxy f
-> Proxy rs -> (a c :- b c) -> RecAll f rs a :- RecAll f rs b
(bound at Table.hs:76:1)
In the pattern: Constraint.Dict
In the pattern: Sub Constraint.Dict
In an equation for ‘weakenRecAll’:
weakenRecAll _ _ (Sub Constraint.Dict) = Sub Constraint.Dict
Table.hs:76:46:
Could not deduce (RecAll f rs b)
arising from a use of ‘Constraint.Dict’
from the context (b c)
bound by a pattern with constructor
Constraint.Dict :: forall (a :: Constraint).
(a) =>
Constraint.Dict a,
in an equation for ‘weakenRecAll’
at Table.hs:76:23-37
or from (RecAll f rs a)
bound by a type expected by the context:
(RecAll f rs a) => Constraint.Dict (RecAll f rs b)
at Table.hs:76:42-60
Relevant bindings include
weakenRecAll :: Proxy f
-> Proxy rs -> (a c :- b c) -> RecAll f rs a :- RecAll f rs b
(bound at Table.hs:76:1)
In the first argument of ‘Sub’, namely ‘Constraint.Dict’
In the expression: Sub Constraint.Dict
In an equation for ‘weakenRecAll’:
weakenRecAll _ _ (Sub Constraint.Dict) = Sub Constraint.Dict
首先回顾一下Dict和(:-)是如何使用的。
ordToEq :: Dict (Ord a) -> Dict (Eq a)
ordToEq Dict = Dict
模式匹配的值Dict类型的Dict (Ord a)将约束Ord a带入了范围，从中可以推导出Eq a （因为Eq是Ord的超类），所以Dict :: Dict (Eq a)类型。
ordEntailsEq :: Ord a :- Eq a
ordEntailsEq = Sub Dict
类似地， Sub在其参数的持续时间内将其输入约束纳入范围，从而允许此Dict :: Dict (Eq a)也很好地类型化。
然而，虽然Dict上的模式匹配带来了一个约束到范围，但在Sub Dict上的模式匹配没有引入一些新的约束转换规则。 事实上，除非输入约束已经在范围内，否则根本无法在Sub Dict上进行模式匹配。
-- Could not deduce (Ord a) arising from a pattern
constZero :: Ord a :- Eq a -> Int
constZero (Sub Dict) = 0
-- okay
constZero' :: Ord a => Ord a :- Eq a -> Int
constZero' (Sub Dict) = 0
因此，这解释了您的第一个类型错误， "Could not deduce (ac) arising from a pattern" ：您试图在Sub Dict上进行模式匹配，但输入约束ac尚未处于范围之内。
另一种类型的错误当然是说你设定的限制条件不足以满足RecAll f rs b约束条件。 那么，哪些是需要的，哪些缺失？ 我们来看一下RecAll的定义。
type family RecAll f rs c :: Constraint where
RecAll f [] c = ()
RecAll f (r : rs) c = (c (f r), RecAll f rs c)
啊哈！ RecAll是一个类型族，因此没有进行评估，它具有完全抽象的rs ，约束RecAll f rs c是一个黑盒子，不能满足任何一组小块。 一旦我们专门rs到[]或(r : rs)很明显，我们需要这件：
recAllNil :: Dict (RecAll f '[] c)
recAllNil = Dict
recAllCons :: p rs
-> Dict (c (f r))
-> Dict (RecAll f rs c)
-> Dict (RecAll f (r ': rs) c)
recAllCons _ Dict Dict = Dict
我使用p rs而不是Proxy rs因为它更灵活：如果我有Rec f rs ，例如我可以使用它作为p ~ Rec f代理。
接下来，让我们使用(:-)而不是Dict实现上述版本：
weakenNil :: RecAll f '[] c1 :- RecAll f '[] c2
weakenNil = Sub Dict
weakenCons :: p rs
-> c1 (f r) :- c2 (f r)
-> RecAll f rs c1 :- RecAll f rs c2
-> RecAll f (r ': rs) c1 :- RecAll f (r ': rs) c2
weakenCons _ entailsF entailsR = Sub $ case (entailsF, entailsR) of
(Sub Dict, Sub Dict) -> Dict
Sub将其输入约束RecAll f (r ': rs) c1纳入其参数持续时间的作用域中，我们已经安排将该参数包含在函数的其余部分中。 对于类型族RecAll f (r ': rs) c1的等式扩展为(c1 (fr), RecAll f rs c1) ，因此这两者都被引入范围。 它们在范围内的事实允许我们在两个Sub Dict上进行模式匹配，并且这两个Dict将它们各自的约束条件带入范围： c2 (fr)和RecAll f rs c2 。 这两个正是目标约束RecAll f (r ': rs) c2扩展到的内容，所以我们的Dict右边是很好的类型。
为了完成weakenAllRec的实现，我们需要在rs上进行模式匹配，以确定是否将工作委托给weakenNil或weakenCons 。 但是由于rs处于类型级别，我们不能直接对它进行模式匹配。 Hasochism文件解释了为了在类型级Nat上进行模式匹配，我们需要创建一个包装数据类型Natty 。 Natty工作方式是它的每个构造函数都由一个相应的Nat构造函数索引，所以当我们在一个Natty构造函数的值级别进行模式匹配时，相应的构造函数也在类型级别上隐含。 我们可以为类型级别列表（如rs定义这样一个包装器，但恰恰相反， weakenAllRec Rec f rs已经具有对应于[]和(:)构造函数，并且weakenAllRec的调用者可能有一个位于其周围的构造函数。
weakenRecAll :: Rec f rs
-> (forall a. c1 a :- c2 a)
-> RecAll f rs c1 :- RecAll f rs c2
weakenRecAll RNil entails = weakenNil
weakenRecAll (fx :& rs) entails = weakenCons rs entails
$ weakenRecAll rs entails
请注意， entails类型必须是全部forall a. c1 a :- c2 a forall a. c1 a :- c2 a ，不仅仅是c1 a :- c2 a ，因为我们不想声称weakenRecAll将任何工作a来电者的选择的，而是，我们希望能够要求调用者证明c1 a每个a需要c2 a a 。
上一篇: Weakening vinyl's RecAll constraint through entailment
下一篇: Is there a way to make GHC provide the type class constraints of typed holes?