How to do existential quantification with GADT?

Question

I have the following data type:

{-# LANGUAGE ExistentialQuantification #-}

data ExType = forall a. One a | forall a. Two a | forall a. Three a

With that I am able to create heterogeneous lists:

[One 3, Two "hello", One 'G']

I have been told that GADTs are the new way to do this. That GADTs can implicitly do what I am trying to do above. I have, so far, not been able to create a type with GADTs that allow me to do a heterogeneous list. How do I do this?

Thanks

Answer 1

Normally a GADT with a polymorphic constructor would have a type argument, so that you could know what type was used when constructing it, such as:

{-# LANGUAGE GADTs #-}
data Value a where
  Str :: String -> ExType String
  Number :: Int -> ExType Int
  Other :: a -> ExType a

However, the key thing an existential type does is bury this type, so that you can't know what a it was constructed with, merely that some type a exists that it contains. So, simply drop the type argument from its type constructor, and from the result types of the data constructors.

{-# LANGUAGE GADTs #-}
data ExType where
  One :: a -> ExType
  Two :: a -> ExType
  Three :: a -> ExType

foo :: [ExType]
foo = [One 3, Two "hello", One 'G']

Answer 2

I cannot tell if GADTs are the new black but - here is your example using this syntax.

{-# LANGUAGE ExplicitForAll     #-}
{-# LANGUAGE GADTs              #-}

data ExType where
  One :: forall a. a -> ExType
  Two :: forall a. a -> ExType
  Three :: forall a. a -> ExType

lst :: [ExType]
lst = [One 3, Two "hello", Three 'A']

Note that deriving instances for GADTs is best done with {-# LANGUAGE StandaloneDeriving #-}, though even basic stuff like Eq won't work because of the constraint forall a.