展开存在量化的 GADT

Question

我有一个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 for'Bool和'Text，但是如何定义多态unwrap？

Answer 1

你真的无法避免在这里使用类型类或等价物。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