展开存在量化的 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)

我可以分别为 'Bool 和 'Text 定义 unwrap，但是如何定义多态 unwrap？

Answer 1

可能的解决方案，定义了一个类型类来具体化类型 ValType 回到术语：

class IsType a where
  typeOf :: Proxy a -> ValType

instance IsType 'Text where
  typeOf _ = Text

instance IsType 'Bool where
  typeOf _ = Bool

unwarp :: IsType tag => SomeValue -> Maybe (Value tag)
unwarp (SomeValue v) =
  case typeOf (Proxy @tag) of
    Bool ->
      case v of
        B _ -> Just v
        _ -> Nothing
    Text ->
      case v of
        T _ -> Just v
        _ -> Nothing

但我必须随身携带那个不太优雅的类型类字典。

Answer 2

你真的无法避免类型class 或类似的东西。 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 class 不同，KnownValType 允许您从模式匹配中获取类型信息和值标记。因此，您可以更普遍地使用它来处理这些类型。

如果你的typeOf够用，我们可以毫不费力地写出来：

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

Answer 3

作为另一种选择，使用 Typeable 和 cast 是一个非常简洁的解决方案。你仍然需要随身携带一本字典，但你不必自己构建它：

{-# LANGUAGE DataKinds, FlexibleInstances, GADTs,
    KindSignatures, StandaloneDeriving, OverloadedStrings #-}

import Data.Text (Text)
import Data.Typeable

data ValType
  = Text
  | Bool

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

data SomeValue = forall tag. SomeValue (Value tag)

unwrap :: (Typeable tag) => SomeValue -> Maybe (Value tag)
unwrap (SomeValue (T t)) = cast (T t)
unwrap (SomeValue (B b)) = cast (B b)

main = do
  print (unwrap (SomeValue (T "foo")) :: Maybe (Value 'Text))
  print (unwrap (SomeValue (T "foo")) :: Maybe (Value 'Bool))

Answer 4

这可以接受吗？

data SomeValue = forall tag. (Typeable tag) => SomeValue (Value tag)

unwrap :: (Typeable tag) => SomeValue -> Maybe (Value tag)
unwrap (SomeValue t) = cast t

“将通用类型转换为 Maybe 特定类型”模式几乎就是 Typeable 的用途。

展开存在量化的 GADT

Unwrapping an existentially quantified GADT

haskell

dependent-type

gadt

existential-type