haskell - 可打字类型转换 GADT

Question

假设我正在编写一个 DSL，并希望同时支持幻像类型和错误类型的表达式。我的值(value)类型可能是

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

首先，您需要在 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