Смазываемые GADT

Question

Предположим, я пишу DSL и хочу иметь поддержку как поддержки фантомного типа, так и плохо типизированных выражений. Мои типы значений могут быть

{-# LANGUAGE GADTs, DataKinds #-} 

data Ty = Num | Bool deriving (Typeable) 

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

и я могу работать с фантом стерта версия

{-# LANGUAGE ExistentialQuantification #-} 

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

Теперь я могу работать на значениях Valunk по case ИНГ из обоих VNum и VBool и даже восстановить свой фантом типы таким образом

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

Но это просто похоже на то,машины. К сожалению, GHC не позволит мне получить Typeable для 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 

Есть ли способ обойти это ограничение? Я хотел бы написать

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

, но сейчас я должен прибегнуть к оборудованию, как этот

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

для всех моих типов.

Answer 1

Вы можете получить Data.Typeable самостоятельно:

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

Это обеспечит функцию получить его. Просто не забудьте правильно назвать свой тип (таким образом, файл, модуль и тип правдиво), иначе другие пакеты могут попасть в проблемы.

Дополнительные примеры того, как писать эти экземпляры, рассмотрим: Data.Derive.Typeable source.

EDIT: У меня была очень странная копия и прошлая ошибка в коде, но теперь она работает.

Answer 2

Прежде всего, вам нужно хранить свидетельство о том, что количественно тип в Valunk находится в Typeable:

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

После того как вы это, вы можете просто использовать gcast, чтобы добиться того, что вы просите:

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

Это было проверено с:

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