GADT cast in modo normale

Question

Diciamo che sto scrivendo una DSL e voglio avere supporto sia per il supporto di tipo fantasma che per le espressioni mal digitate. I miei tipi di valore potrebbero essere

{-# LANGUAGE GADTs, DataKinds #-} 

data Ty = Num | Bool deriving (Typeable) 

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

e posso lavorare con un fantasma cancellata versione

{-# LANGUAGE ExistentialQuantification #-} 

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

Ora, posso operare su valori di Valunk da case ing fuori sia VNum e VBool e anche ristabilire il mio fantasma tipi in questo modo

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

Ma questo mi sembra di reimplementare lo Typeable macchinario. Purtroppo, GHC non mi permette di ricavare una Typeable per 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 

C'è un modo per aggirare questa limitazione? Mi piacerebbe scrivere

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

ma adesso devo ricorrere a macchinari come questo

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

per tutti i miei tipi.

Answer 1

È possibile derivare Data.Typeable da soli:

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

Ciò fornirà la funzione di ottenerlo. Assicurati di dare un nome corretto al tuo tipo (quindi file il pacchetto, modulo e tipo sinceramente) altrimenti gli altri pacchetti possono entrare nei problemi.

Per ulteriori esempi su come scrivere queste istanze, esaminare: Data.Derive.Typeable source.

EDIT: Ho avuto una copia molto strana e un errore passato nel codice, ma ora funziona.

Answer 2

Prima di tutto, è necessario memorizzare una testimonianza che il tipo quantificato in Valunk è in Typeable:

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

Una volta fatto questo, si può semplicemente utilizzare gcast per ottenere quello che stai chiedendo:

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

Questo è stato testato con:

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