Typowe odlewanie GADTs

Question

Załóżmy, że piszę DSL i chcę mieć wsparcie zarówno dla typów fantomowych, jak i źle wypisanych wyrażeń. Moje typy wartości mogą być

{-# LANGUAGE GADTs, DataKinds #-} 

data Ty = Num | Bool deriving (Typeable) 

data Val a where 
    VNum :: Int -> Val Num 
    VBool :: Bool -> Val Bool 

i mogę pracować z fantomu skasowane wersja

{-# LANGUAGE ExistentialQuantification #-} 

data Valunk = forall a . Valunk (V' a) 

Teraz mogę pracować na wartościach Valunk przez case ing się zarówno VNum i VBool a nawet przywrócić mój fantom typy w ten sposób

getNum :: Valunk -> Maybe (Val Num) 
getNum (Valunk n@(VNum _)) = Just n 
getNum _     = Nothing 

Ale to po prostu wydaje się być reimplementing Typeable maszyn. Niestety, GHC nie pozwoli mi czerpać Typeable dla Val

src/Types/Core.hs:97:13: 
    Can't make a derived instance of `Typeable (Val a)': 
     Val must only have arguments of kind `*' 
    In the data declaration for Val 

Czy istnieje sposób, aby obejść to ograniczenie? Chciałbym napisać

getIt :: Typeable a => Valunk -> Maybe (Val a) 
getIt (Valunk v) = cast v 

ale teraz muszę uciekać się do maszyn, jak to

class Typeably b x where kast :: x a -> Maybe (x b) 
instance Typeably Num Val where 
    kast n@(VNum _) = Just n 
    kast _   = Nothing 

dla wszystkich moich typów.

Answer 1

można czerpać Data.Typeable na własną rękę:

{-# LANGUAGE GADTs, DataKinds, DeriveDataTypeable, ExistentialQuantification #-} 

import Data.Typeable 

data Ty = TNum | TBool deriving Typeable 

data Valunk = forall a. Typeable a => Valunk a 

data Val a where 
    VInt :: Int -> Val TNum 
    VBool :: Bool -> Val TBool 

instance Show (Val a) where 
    show (VInt a) = show a 
    show (VBool a) = show a 

valtypenam = mkTyCon3 "package" "module" "Val" 

instance Typeable (Val a) where 
    typeOf _ = mkTyConApp valtypenam [] 

getIt :: Valunk -> Maybe (Val a) 
getIt (Valunk p) = cast p 

ten zapewni funkcję zdobyć. Po prostu pamiętaj, aby poprawnie nazwać swój typ (w ten sposób złożyć plik, moduł i typ zgodnie z prawdą), w przeciwnym razie inne pakiety mogą mieć problemy.

Aby uzyskać więcej przykładów tworzenia tych wystąpień, należy sprawdzić: Data.Derive.Typeable source.

EDIT: Miałem bardzo dziwną kopię i błąd przeszłości w kodzie, ale teraz działa.

Answer 2

Przede wszystkim, trzeba przechowywać świadectwo, że ilościowo wpisz Valunk jest w Typeable:

data Valunk = forall a . Typeable a => Valunk (Val a) 

Gdy masz ten problem, można po prostu użyć gcast osiągnąć co pytasz o:

getIt :: Typeable a => Valunk -> Maybe (Val a) 
getIt (Valunk v) = gcast v 

ten badano:

data Val a where 
    VNum :: Int -> Val Int 
    VBool :: Bool -> Val Bool