Logo Questions Linux Laravel Mysql Ubuntu Git Menu
 

Unwrapping an existentially quantified GADT

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?

like image 930
Poscat Avatar asked Jun 20 '20 13:06

Poscat


2 Answers

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
like image 139
dfeuer Avatar answered Nov 11 '22 23:11

dfeuer


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))
like image 3
K. A. Buhr Avatar answered Nov 11 '22 22:11

K. A. Buhr