in vinyl library, there recall type family, let's ask partially applied constraint true every type in type level list. example, can write this:
myshowfunc :: recall f rs show => rec f rs -> string and that's lovely. now, if have constraint recall f rs c c unknown, , know c x entails d x (to borrow language ekmett's contstraints package), how can recall f rs d?
the reason ask i'm working records in functions require satisfying several typeclass constraints. this, using :&: combinator control.constraints.combine module in exists package. (note: package won't build if have other things installed because depends on super-old version of contravariant. can copy 1 module mentioned though.) this, can beautiful constraints while minimizing typeclass broilerplate. example:
recall f rs (typeablekey :&: fromjson :&: typeableval) => rec f rs -> value but, inside body of function, call function demands weaker constraint. might this:
recall f rs (typeablekey :&: typeableval) => rec f rs -> value ghc can't see second statement follows first. assumed case. can't see how prove reify , ghc out. far, i've got this:
import data.constraint weakenand1 :: ((a :&: b) c) :- c weakenand1 = sub dict -- not dict vinyl. ekmett's dict. weakenand2 :: ((a :&: b) c) :- b c weakenand2 = sub dict these work fine. stuck:
-- 2 proxy args stop ghc complaining ambiguoustypes weakenrecall :: proxy f -> proxy rs -> (a c :- b c) -> (recall f rs :- recall f rs b) weakenrecall _ _ (sub dict) = sub dict this not compile. aware of way effect looking for. here errors if helpful. also, have dict qualified import in actual code, that's why mentions constraint.dict:
table.hs:76:23: not deduce (a c) arising pattern relevant bindings include weakenrecall :: proxy f -> proxy rs -> (a c :- b c) -> recall f rs :- recall f rs b (bound @ table.hs:76:1) in pattern: constraint.dict in pattern: sub constraint.dict in equation ‘weakenrecall’: weakenrecall _ _ (sub constraint.dict) = sub constraint.dict table.hs:76:46: not deduce (recall f rs b) arising use of ‘constraint.dict’ context (b c) bound pattern constructor constraint.dict :: forall (a :: constraint). (a) => constraint.dict a, in equation ‘weakenrecall’ @ table.hs:76:23-37 or (recall f rs a) bound type expected context: (recall f rs a) => constraint.dict (recall f rs b) @ table.hs:76:42-60 relevant bindings include weakenrecall :: proxy f -> proxy rs -> (a c :- b c) -> recall f rs :- recall f rs b (bound @ table.hs:76:1) in first argument of ‘sub’, namely ‘constraint.dict’ in expression: sub constraint.dict in equation ‘weakenrecall’: weakenrecall _ _ (sub constraint.dict) = sub constraint.dict
let's begin reviewing how dict , (:-) meant used.
ordtoeq :: dict (ord a) -> dict (eq a) ordtoeq dict = dict pattern matching on value dict of type dict (ord a) brings constraint ord a scope, eq a can deduced (because eq superclass of ord), dict :: dict (eq a) well-typed.
ordentailseq :: ord :- eq ordentailseq = sub dict similarly, sub brings input constraint scope duration of argument, allowing dict :: dict (eq a) well-typed well.
however, whereas pattern-matching on dict brings constraint scope, pattern-matching on sub dict not bring scope new constraint conversion rule. in fact, unless input constraint in scope, can't pattern-match on sub dict @ all.
-- not deduce (ord a) arising pattern constzero :: ord :- eq -> int constzero (sub dict) = 0 -- okay constzero' :: ord => ord :- eq -> int constzero' (sub dict) = 0 so explains first type error, "could not deduce (a c) arising pattern": have tried pattern-match on sub dict, input constraint a c not in scope.
the other type error, of course, saying constraints did manage scope not sufficient satisfy recall f rs b constraint. so, pieces needed, , ones missing? let's @ definition of recall.
type family recall f rs c :: constraint recall f [] c = () recall f (r : rs) c = (c (f r), recall f rs c) aha! recall type family, unevaluated is, abstract rs, constraint recall f rs c black box not satisfied set of smaller pieces. once specialize rs [] or (r : rs), becomes clear pieces 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 had rec f rs, instance use proxy p ~ rec f.
next, let's implement version of above (:-) 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 input constraint recall f (r ': rs) c1 scope duration of argument, we've arranged include rest of function's body. equation type family recall f (r ': rs) c1 expands (c1 (f r), recall f rs c1), both brought scope well. fact in scope allows pattern-match on 2 sub dict, , 2 dict bring respective constraints scope: c2 (f r), , recall f rs c2. 2 precisely target constraint recall f (r ': rs) c2 expands to, our dict right-hand side well-typed.
to complete our implementation of weakenallrec, need pattern-match on rs in order determine whether delegate work weakennil or weakencons. since rs @ type level, cannot pattern-match on directly. hasochism paper explains how in order pattern-match on type-level nat, need create wrapper datatype natty. way in natty works each of constructors indexed corresponding nat constructor, when pattern-match on natty constructor @ value level, corresponding constructor implied @ type level well. define such wrapper type-level lists such rs, happens rec f rs has constructors corresponding [] , (:), , callers of weakenallrec have 1 lying around anyway.
weakenrecall :: rec f rs -> (forall a. c1 :- 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 type of entails must forall a. c1 :- c2 a, not merely c1 :- c2 a, because don't want claim weakenrecall work a of caller's choosing, rather, want require caller prove c1 a entails c2 a every a.
