通过蕴涵削弱乙烯基的RecAll约束

Question

在乙烯基库中,有一个RecAll类型族,让我们要求对类型级别列表中的每个类型使用部分应用的约束.例如,我们可以这样写:

myShowFunc :: RecAll f rs Show => Rec f rs -> String

这一切都很可爱.现在,如果我们的约束RecAll f rs c在哪里c是未知的,并且我们知道c x需要d x(借用ekmett的contstraints包中的语言),我们怎么能得到RecAll f rs d？

我问的原因是我正在处理一些需要满足几个类型类约束的函数中的记录.要,我现在用的是做这个:&:组合子从Control.Constraints.Combine模块中存在的包.(注意:如果安装了其他东西,则不会构建软件包,因为它依赖于超级旧版本contravariant.您可以复制我提到的一个模块.)有了这个,我可以得到一些非常漂亮的约束,同时最小化类型类肉鸡.例如:

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

Answer 1

首先,让我们通过审查如何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 (a c) arising from a pattern":您已尝试进行模式匹配Sub Dict,但输入约束a c尚未在范围内.

当然,另一种类型错误是说你设法进入范围的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 (f r), RecAll f rs c1),因此也被纳入范围.它们在范围内的事实允许我们在两者上进行模式匹配Sub Dict,并且这两者Dict将它们各自的约束带入范围:c2 (f r)和RecAll f rs c2.这两个正是目标约束RecAll f (r ': rs) c2扩展到的,因此我们的Dict右侧是良好的类型.

为了完成我们的实现weakenAllRec,我们需要进行模式匹配,rs以确定是否将工作委托给weakenNil或weakenCons.但由于rs属于类型级别,我们无法直接对其进行模式匹配.该Hasochism本文介绍了如何以模式匹配的类型层次Nat,我们需要创建一个包装数据类型Natty.工作的方式Natty是每个构造函数都由相应的Nat构造函数索引,因此当我们Natty在值级别的构造函数上进行模式匹配时,相应的构造函数也隐含在类型级别.我们可以定义为类型级列表,如这样的包装rs,但它只是恰巧,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,不仅仅是c1 a :- c2 a因为我们不想声称这weakenRecAll将适用于任何a调用者的选择,而是,我们希望要求调用者证明每个都c1 a需要.c2 aa