适当地铸造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

但这只是感觉我正在重新实现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 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 

这将提供 get it 功能。只需确保正确命名您的类型（从而如实归档包、模块和类型），否则其他包可能会出现问题。

有关如何编写这些实例的更多示例，请查看：Data.Derive.Typeable source。

编辑： 我在代码中有一个非常奇怪的副本和过去的错误，但现在它可以工作了。