Weakening vinyl's RecAll constraint through entailment
In the vinyl library, there is a RecAll type family, which let's us ask that a partially applied constraint is true for every type in a type level list. For example, we can write this:
myShowFunc :: RecAll f rs Show => Rec f rs -> String
And that's all lovely. Now, if we have the constraint RecAll f rs c where c is unknown, and we know the cx entails dx (to borrow language from ekmett's contstraints package), how can we get RecAll f rs d ?
The reason I ask is that I'm working with records in some functions that require satisfying several typeclass constraints. To do this, I am using the :&: combinator from the Control.Constraints.Combine module in the exists package. (Note: the package won't build if you have other things installed because it depends on a super-old version of contravariant . You can just copy the one module I mentioned though.) With this, I can get some really beautiful constraints while minimizing typeclass broilerplate. For example:
RecAll f rs (TypeableKey :&: FromJSON :&: TypeableVal) => Rec f rs -> Value
But, inside the body of this function, I call another function that demands a weaker constraint. It might look like this:
RecAll f rs (TypeableKey :&: TypeableVal) => Rec f rs -> Value
GHC can't see that the second statement follows from the first. I assumed that would be the case. What I can't see is how to prove it for reify it and help GHC out. So far, I've got this:
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
These work fine. But this is where I am stuck:
-- 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
This does not compile. Is anyone aware of a way to get the effect I am looking for. Here are the errors if they are helpful. Also, I have Dict as a qualified import in my actual code, so that's why it mentions 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
Let's begin by reviewing how Dict and (:-) are meant to be used.
ordToEq :: Dict (Ord a) -> Dict (Eq a)
ordToEq Dict = Dict
Pattern matching on a value Dict of type Dict (Ord a) brings the constraint Ord a into scope, from which Eq a can be deduced (because Eq is a superclass of Ord ), so Dict :: Dict (Eq a) is well-typed.
ordEntailsEq :: Ord a :- Eq a
ordEntailsEq = Sub Dict
Similarly, Sub brings its input constraint into scope for the duration of its argument, allowing this Dict :: Dict (Eq a) to be well-typed as well.
However, whereas pattern-matching on Dict brings a constraint into scope, pattern-matching on Sub Dict does not bring into scope some new constraint conversion rule. In fact, unless the input constraint is already in scope, you can't pattern-match on Sub Dict at all.
-- 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
So that explains your first type error, "Could not deduce (ac) arising from a pattern" : you have tried to pattern-match on Sub Dict , but the input constraint ac was not already in scope.
The other type error, of course, is saying that the constraints you did manage to get into scope were not sufficient to satisfy the RecAll f rs b constraint. So, which pieces are needed, and which ones are missing? Let's look at the definition of RecAll .
type family RecAll f rs c :: Constraint where
RecAll f [] c = ()
RecAll f (r : rs) c = (c (f r), RecAll f rs c)
Aha! RecAll is a type family, so unevaluated as it is, with a completely abstract rs , the constraint RecAll f rs c is a black box which could not be satisfied from any set of smaller pieces. Once we specialize rs to [] or (r : rs) , it becomes clear which pieces we need:
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
I'm using p rs instead of Proxy rs because it's more flexible: if I had a Rec f rs , for instance I could use that as my proxy with p ~ Rec f .
Next, let's implement a version of the above with (:-) instead of 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 brings its input constraint RecAll f (r ': rs) c1 into scope for the duration of its argument, which we've arranged to include the rest of the function's body. The equation for the type family RecAll f (r ': rs) c1 expands to (c1 (fr), RecAll f rs c1) , which are thus both brought into scope as well. The fact that they are in scope allows us to pattern-match on the two Sub Dict , and those two Dict bring their respective constraints into scope: c2 (fr) , and RecAll f rs c2 . Those two are precisely what the target constraint RecAll f (r ': rs) c2 expands to, so our Dict right-hand side is well-typed.
To complete our implementation of weakenAllRec , we will need to pattern-match on rs in order to determine whether to delegate the work to weakenNil or weakenCons . But since rs is at the type level, we cannot pattern-match on it directly. The Hasochism paper explains how in order to pattern-match on a type-level Nat , we need to create a wrapper datatype Natty . The way in which Natty works is that each of its constructors is indexed by a corresponding Nat constructor, so when we pattern-match on a Natty constructor at the value level, the corresponding constructor is implied at the type level as well. We could define such a wrapper for type-level lists such as rs , but it just so happens that Rec f rs already has constructors corresponding to [] and (:) , and the callers of weakenAllRec are likely to have one lying around anyway.
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
Note that the type of entails must be forall a. c1 a :- c2 a forall a. c1 a :- c2 a , not merely c1 a :- c2 a , because we don't want to claim that weakenRecAll will work for any a of the caller's choosing, but rather, we want to require the caller to prove that c1 a entails c2 a for every a .
下一篇: 通过包容来减弱乙烯基的RecAll约束