Ograniczona rodzina zamkniętych typów

Question

Czy mogę przekonać kompilator, że ograniczenie jest zawsze spełnione przez typ synonimów w rodzinie typu zamkniętego? Rodzina jest indeksowana przez skończony zestaw promowanych wartości.

Coś wzdłuż linii

data NoShow = NoShow 
data LiftedType = V1 | V2 | V3 

type family (Show (Synonym (a :: LiftedType)) => Synonym (a :: LiftedType)) where 
    Synonym V1 = Int 
    Synonym V2 = NoShow -- no Show instance => compilation error 
    Synonym V3 =() 

mogę wymusić ograniczenie na otwartych rodzin typu:

class (Show (Synonym a)) => SynonymClass (a :: LiftedType) where 
    type Synonym a 
    type Synonym a =() 

instance SynonymClass Int where 
    type Synonym V1 = Int 

-- the compiler complains here 
instance SynonymClass V2 where 
    type Synonym V2 = NoShow 

instance SynonymClass V3 

ale kompilator będzie wtedy musiał być w stanie rozumować o tym, że istnieje wystąpienie SynonymClass a dla każdego z V1, i V3? Ale w każdym razie wolałbym nie używać rodziny typu otwartego.

Moja motywacja do tego jest taka, że ​​chcę przekonać kompilator, że wszystkie wystąpienia zamkniętej rodziny w moim kodzie mają wystąpienia Show/Read. Uproszczony przykład to:

parseLTandSynonym :: LiftedType -> String -> String 
parseLTandSynonym lt x = 
    case (toSing lt) of 
    SomeSing (slt :: SLiftedType lt') -> parseSynonym slt x 

parseSynonym :: forall lt. SLiftedType lt -> String -> String 
parseSynonym slt flv = 
     case (readEither flv :: Either String (Synonym lt)) of 
     Left err -> "Can't parse synonym: " ++ err 
     Right x -> "Synonym value: " ++ show x 

[Ktoś wspomniał w komentarzach, że nie jest to możliwe - czy to dlatego, że jest to technicznie niemożliwe (a jeśli tak, to dlaczego) lub po prostu ograniczenie realizacji GHC?]

Answer 1

Problem polega na tym, że nie możemy umieścić Synonym w głowicy instancji, ponieważ jest to rodzina typów i nie możemy napisać ograniczenia "uniwersalnie określanego ilościowo", takiego jak (forall x. Show (Synonym x)) => ..., ponieważ nie ma czegoś takiego w Haskell.

Jednak możemy korzystać z dwóch rzeczy:

• forall x. f x -> a jest równoważna (exists x. f x) -> a
• singletons „s defunctionalization pozwala nam umieścić typ rodziny język instancji głowach tak.

Tak, możemy zdefiniować egzystencjalne owijkę, która działa na singletons -Style funkcji typ:

data Some :: (TyFun k * -> *) -> * where 
    Some :: Sing x -> f @@ x -> Some f 

I my również zawierać symbol defunctionalization dla LiftedType:

import Data.Singletons.TH 
import Text.Read 
import Control.Applicative 

$(singletons [d| data LiftedType = V1 | V2 | V3 deriving (Eq, Show) |]) 

type family Synonym t where 
    Synonym V1 = Int 
    Synonym V2 =() 
    Synonym V3 = Char 

data SynonymS :: TyFun LiftedType * -> * -- the symbol for Synonym 
type instance Apply SynonymS t = Synonym t 

Teraz możemy użyj Some SynonymS -> a zamiast forall x. Synonym x -> a, a ten formularz może być również używany w instancjach.

instance Show (Some SynonymS) where 
    show (Some SV1 x) = show x 
    show (Some SV2 x) = show x 
    show (Some SV3 x) = show x 

instance Read (Some SynonymS) where 
    readPrec = undefined -- I don't bother with this now... 

parseLTandSynonym :: LiftedType -> String -> String 
parseLTandSynonym lt x = 
    case (toSing lt) of 
    SomeSing (slt :: SLiftedType lt') -> parseSynonym slt x 

parseSynonym :: forall lt. SLiftedType lt -> String -> String 
parseSynonym slt flv = 
     case (readEither flv :: Either String (Some SynonymS)) of 
     Left err -> "Can't parse synonym: " ++ err 
     Right x -> "Synonym value: " ++ show x 

nie bezpośrednio dostarczyć nam Read (Synonym t) dla konkretnego wyboru t, choć nadal możemy czytać Some SynonymS a następnie wzór spotkanie na znaczniku egzystencjalnym, by sprawdzić, czy mamy odpowiedni typ (a nie powieść, jeśli nie jest to dobrze). To prawie obejmuje wszystkie przypadki użycia read.

Jeśli to nie wystarczy, możemy użyć innego opakowania i przenieść instancje Some f do instancji "powszechnie określanych ilościowo".

data At :: (TyFun k * -> *) -> k -> * where 
    At :: Sing x -> f @@ x -> At f x 

At f x jest równoważna f @@ x, ale możemy napisać instancje dla niego.W szczególności możemy napisać sensowną uniwersalną instancję Read tutaj.

instance (Read (Some f), SDecide (KindOf x), SingKind (KindOf x), SingI x) => 
    Read (At f x) where 
    readPrec = do 
     Some tag x <- readPrec :: ReadPrec (Some f) 
     case tag %~ (sing :: Sing x) of 
     Proved Refl -> pure (At tag x) 
     Disproved _ -> empty 

Najpierw analizowania Some f, a następnie sprawdzić, czy analizowany wskaźnik typ jest równy wskaźnikowi którą chcemy analizować. Jest to abstrakcja wzorca, o którym wspomniałem powyżej dla parsowania typów o określonych indeksach. Jest to wygodniejsze, ponieważ mamy tylko jeden przypadek w dopasowaniu wzorca na At, bez względu na to, ile mamy indeksów. Zwróć uwagę na ograniczenie więzów SDecide. Zapewnia on metodę %~, a singletons uzyskuje ją dla nas, jeśli uwzględnimy deriving Eq w definicjach danych singletowych. Umieszczenie tego używać:

parseSynonym :: forall lt. SLiftedType lt -> String -> String 
parseSynonym slt flv = withSingI slt $ 
     case (readEither flv :: Either String (At SynonymS lt)) of 
     Left err -> "Can't parse synonym: " ++ err 
     Right (At tag x) -> "Synonym value: " ++ show (Some tag x :: Some SynonymS) 

Możemy również dokonać konwersji pomiędzy At i Some nieco łatwiejszej:

curry' :: (forall x. At f x -> a) -> Some f -> a 
curry' f (Some tag x) = f (At tag x) 

uncurry' :: (Some f -> a) -> At f x -> a 
uncurry' f (At tag x) = f (Some tag x) 

parseSynonym :: forall lt. SLiftedType lt -> String -> String 
parseSynonym slt flv = withSingI slt $ 
     case (readEither flv :: Either String (At SynonymS lt)) of 
     Left err -> "Can't parse synonym: " ++ err 
     Right atx -> "Synonym value: " ++ uncurry' show atx 

Answer 2

Jeśli dobrze rozumiem, co chcesz zrobić, to nie jest możliwe. Gdyby tak było, można łatwo skonstruować zakaz stałą funkcję typu Proxy t -> Bool, wzdłuż linii

data YesNo = Yes | No 
class Foo (yn :: YesNo) where foo :: Proxy yn -> Bool 
type family (Foo (T t) => T t) where 
    T X = Yes 
    T y = No 

f :: forall t. Proxy t -> Bool 
f _ = foo (Proxy (T t)) 

Ale nie można skonstruować taką funkcję, nawet gdy wszystkie rodzaje zaangażowane są zamknięte (co jest oczywiście albo funkcja lub ograniczenie GHC, w zależności od twojego punktu widzenia).