Osłabienie wiązania RecAll winylu przez wymuszenie

Question

W bibliotece vinyl znajduje się rodzina typów RecAll, która pozwala nam zapytać, czy ograniczenie stosowane częściowo jest prawdziwe dla każdego typu na liście poziomu typów. Na przykład, możemy napisać to:

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

To wszystko jest piękne. Teraz, jeśli mamy ograniczenie RecAll f rs c, gdzie c jest nieznany i wiemy, że c x zawiera d x (aby wypożyczyć język z pakietu ekmett's contstraints), jak możemy uzyskać RecAll f rs d?

Powodem, dla którego pytam, jest to, że pracuję z rekordami w niektórych funkcjach, które wymagają spełnienia kilku ograniczeń typeclass. Aby to zrobić, używam kombinatora :&: z modułu Control.Constraints.Combine w pakiecie exists. (Uwaga: pakiet nie zostanie skompilowany, jeśli masz zainstalowane inne rzeczy, ponieważ zależy to od bardzo starej wersji contravariant. Możesz po prostu skopiować jeden moduł, o którym wspomniałem.) Dzięki temu mogę uzyskać naprawdę piękne ograniczenia, podczas gdy zminimalizowanie brojlerki typeclass. Na przykład:

RecAll f rs (TypeableKey :&: FromJSON :&: TypeableVal) => Rec f rs -> Value 

Ale w ciele tej funkcji wzywam inną funkcję, która wymaga słabszego ograniczenia. Może to wyglądać następująco:

RecAll f rs (TypeableKey :&: TypeableVal) => Rec f rs -> Value 

GHC nie widzi, że drugie zdanie wynika z pierwszego. Zakładałem, że tak będzie. Nie mogę zobaczyć, jak to udowodnić, aby to potwierdzić i pomóc GHC. Do tej pory mam to:

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 

Te działają dobrze. Ale tutaj utknąłem:

-- 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 

To nie kompiluje. Czy ktoś jest świadomy sposobu uzyskania efektu, którego szukam? Tutaj są błędy, jeśli są pomocne. Również mam Dict jako wykwalifikowany importu w moim rzeczywisty kod, więc dlatego wspomina 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

Zacznijmy od przeglądu jak Dict i (:-) mają być użyte.

ordToEq :: Dict (Ord a) -> Dict (Eq a) 
ordToEq Dict = Dict 

dopasowanie wzorca o wartość Dict typu Dict (Ord a) przynosi ograniczenie Ord a do zakresu, z której można wywnioskować Eq a (ponieważ Eq to nadrzędna Ord) tak Dict :: Dict (Eq a) dobrze wpisany.

ordEntailsEq :: Ord a :- Eq a 
ordEntailsEq = Sub Dict 

Podobnie Sub powoduje jego wejścia do ograniczenia zakresu dla okresu jej argumentów, co pozwala to Dict :: Dict (Eq a) być również wpisany również.

Jednak podczas dopasowywania do wzoru na Dict wprowadza ograniczenie w zakresie, dopasowanie do wzorca na Sub Dict nie wprowadza w zakres jakiejś nowej reguły konwersji wiązań. W rzeczywistości, chyba że ograniczenie wejściowe jest już w zakresie, nie można w ogóle dopasować do wzorca na 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 

Więc to wyjaśnia swój pierwszy błąd typu, "Could not deduce (a c) arising from a pattern": wypróbowaniu do wzorca-meczu na Sub Dict, ale ograniczenie wejścia a c nie był już w zasięgu.

Innym błędem typu jest oczywiście twierdzenie, że ograniczenia, którym udało się wejść w zakres, nie były wystarczające do spełnienia ograniczenia RecAll f rs b. Które części są potrzebne, a których brakuje? Spójrzmy na definicję 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 to rodzina typów, tak bezcenna, z całkowicie abstrakcyjnym rs, ograniczenie RecAll f rs c jest czarną skrzynką, której nie można zadowolić z żadnego zestawu mniejszych elementów. Po specjalizujemy rs do [] lub (r : rs), staje się jasne, jakie elementy musimy:

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 

Używam p rs zamiast Proxy rs ponieważ jest bardziej elastyczny: gdybym miał Rec f rs, na przykład mogę użyć jej jako mój serwer proxy z p ~ Rec f.

Następnie niech wdrożyć wersję powyższego z (:-) zamiast 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 przynosi swoje ograniczenia wejściowego RecAll f (r ': rs) c1 w zakresie w czasie trwania swojego argumentu, który mamy ułożone zawierać resztę ciała funkcji. Równanie dla rodziny typów RecAll f (r ': rs) c1 rozszerza się do (c1 (f r), RecAll f rs c1), które również wchodzą w zakres. Fakt, że są one w zakresie pozwala nam dopasować wzorce na dwóch Sub Dict, a te dwa Dict wprowadzają swoje ograniczenia do zakresu: c2 (f r) i RecAll f rs c2. Te dwa są dokładnie tym, do czego rozszerza się docelowe ograniczenie RecAll f (r ': rs) c2, więc nasza prawa strona Dict jest dobrze wpisana.

Aby zakończyć naszą realizację od weakenAllRec, musimy wzorzec-meczu na rs w celu ustalenia, czy delegować pracę do weakenNil lub weakenCons. Ale ponieważ rs jest na poziomie typu, nie możemy bezpośrednio dopasować do niego wzorca. W dokumencie Hasochism wyjaśniono, w jaki sposób, aby dopasować do wzoru na poziomie typu Nat, musimy utworzyć opakowujący typ danych: Natty. Sposób, w jaki działa Natty, polega na tym, że każdy z jego konstruktorów jest indeksowany przez odpowiadający konstruktor Nat, więc gdy dopasowujemy wzorce do konstruktora Natty na poziomie wartości, odpowiedni konstruktor jest również implikowany na poziomie typu. Możemy zdefiniować takie otoki dla list na poziomie typu, takich jak rs, ale tak się składa, że ​​Rec f rs ma już konstruktory odpowiadające [] i (:), a wywołujący z weakenAllRec prawdopodobnie będą mieć takie, które leżą w pobliżu.

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 

Należy pamiętać, że rodzaj entails musi być forall a. c1 a :- c2 a, nie tylko c1 a :- c2 a, ponieważ nie chcemy, aby twierdzić, że weakenRecAll będzie działać na każdym a wybranym przez dzwoniącego, ale raczej chcemy wymagać rozmówcę aby udowodnić, że zawiera c2 a dla każdego .