Unwrapping an existentially quantified GADT

Question

I have a custom value type Value labeled by its type ValType:

data ValType
  = Text
  | Bool

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

and I would like to define a function that unwraps an existentially quantified Value, that is it should have the following type signature:

data SomeValue = forall tag. SomeValue (Value tag)

unwrap :: SomeValue -> Maybe (Value tag)

I can define unwrap for 'Bool and 'Text separately, but how do I define a polymorphic unwrap?

Riella

One possible workaround is to use an open union, but I'm still curious whether this can be done for GADT. – Riella

basically, how do I pattern match on promoted types? I think you can do that at type-level with type families but how do you do that at the term level? – Riella

Answer 1

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

Maury

For this specific example, unwrap :: SomeValue -> Either (Value 'Text) (Value 'Bool) also looks appropriate. – Phoebe

Answer 2

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))

Wyck

Typeable seems like overkill for a closed universe. – Maury

I guess, but so does writing a polymorphic unwrap. – Wyck

Answer 3

possible solution, defined a typeclass to reify types of kind ValType back to terms:

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

But I'll have to carry around that typeclass dictionary which is not very elegant.

Riella

Answer 4

Would this be acceptable?

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

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

The "cast general type to Maybe specific type" pattern is pretty much what Typeable is for.

Spheroidicity