Unwrapping an existentially quantified GADT
You really can't avoid a typeclass or equivalent here. unwrap
, as you've written its type, has no way to know which tag it's looking for, because types are erased. An idiomatic approach uses the singleton pattern.
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
Unlike the IsType
class of your own answer, KnownValType
lets you get type information as well as a value tag out of a pattern match. So you can use it much more generally for handling these types.
For cases where your typeOf
is sufficient, we can write it with no trouble:
typeOf :: KnownValType a => Proxy a -> ValType
typeOf (_ :: Proxy a) = case knownValType @a of
SBool -> Bool
SText -> Text
As yet another alternative, using Typeable
and cast
makes for a pretty concise solution. You still have to carry around a dictionary, but you don't have to build it yourself:
{-# 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))