鍵入鑄造GADT

假設我正在編寫DSL並希望支持幻像類型支持和嚴重類型表達式。我的值類型可能是鍵入鑄造GADT

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

現在，我可以通過case上的Valunk值進行操作荷蘭國際集團出既VNum和VBool，甚至重新建立我的幻象這種方式

getNum :: Valunk -> Maybe (Val Num) 
getNum (Valunk [email protected](VNum _)) = Just n 
getNum _     = Nothing

但這只是感覺就像我在重新實現Typeable機械。不幸的是，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 [email protected](VNum _) = Just n 
    kast _   = Nothing

我所有的類型。

來源

2013-08-07 J. Abrahamson

它LOO：

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

這與測試ks像'deriving（Typeable）'機器還沒有與'DataKinds'一起使用。 'DataKinds'不會給你任何驚人的，只是一點額外的檢查。你可以使用'data Num'和'data Bool'來代替你的'Ty'類型。 – luqui

你可以自己得出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。

編輯：我在代碼中有一個非常奇怪的副本和過去的錯誤，但現在它的工作。

來源

2013-08-11 21:28:57

首先，你需要存儲的證人，在Valunk的量化類型是Typeable：

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

一旦你有了這個，你可以使用gcast實現你問的：

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

來源

2013-08-15 05:32:38 emilaxelsson

回答

相關問題