时间戳

首页 > 解决方案 > 展开存在量化的 GADT

haskell - 展开存在量化的 GADT

问题描述

我有一个Value按其类型标记的自定义值类型ValType：

data ValType
  = Text
  | Bool

data Value (tag :: ValType) where
  T :: Text -> Value 'Text
  B :: Bool -> Value 'Bool

我想定义一个解开存在量化的函数Value，即它应该具有以下类型签名：

data SomeValue = forall tag. SomeValue (Value tag)

unwrap :: SomeValue -> Maybe (Value tag)

我可以单独定义 unwrap 'Bool，'Text但是如何定义多态unwrap？

标签： haskelldependent-typegadtexistential-type

解决方案

你真的不能在这里避免一个类型类或等价物。unwrap，因为您已经编写了它的类型，所以无法知道它正在寻找哪个标签，因为类型已被删除。惯用的方法使用单例模式。

data SValType v where
  SText :: SValType 'Text
  SBool :: SValType 'Bool

class KnownValType (v :: ValType) where
  knownValType :: SValType v
instance KnownValType 'Text where
  knownValType = SText
instance KnownValType 'Bool where
  knownValType = SBool

unwrap :: forall tag. KnownValType tag => SomeValue -> Maybe (Value tag)
unwrap (SomeValue v) = case knownValType @tag of
  SText
    | T _ <- v -> Just v
    | otherwise -> Nothing
  SBool
    | B _ <- v -> Just v
    | otherwise -> Nothing

与IsType您自己答案的类别不同，它KnownValType允许您从模式匹配中获取类型信息和值标记。因此，您可以更广泛地使用它来处理这些类型。

对于你typeOf的情况足够的情况，我们可以毫不费力地编写它：

 typeOf :: KnownValType a => Proxy a -> ValType
 typeOf (_ :: Proxy a) = case knownValType @a of
   SBool -> Bool
   SText -> Text

推荐阅读