Search code examples
haskellgadtexistential-typephantom-types

Haskell: Heterogeneous list for data with phantom variable


I'm learning about existential quantification, phantom types, and GADTs at the moment. How do I go about creating a heterogeneous list of a data type with a phantom variable? For example:

{-# LANGUAGE GADTs #-}
{-# LANGUAGE ExistentialQuantification #-}

data Toy a where
  TBool :: Bool -> Toy Bool
  TInt  :: Int  -> Toy Int

instance Show (Toy a) where
  show (TBool b) = "TBool " ++ show b
  show (TInt  i) = "TInt "  ++ show i

bools :: [Toy Bool]
bools = [TBool False, TBool True]

ints  :: [Toy Int]
ints  = map TInt [0..9]

Having functions like below are OK:

isBool :: Toy a -> Bool
isBool (TBool _) = True
isBool (TInt  _) = False

addOne :: Toy Int -> Toy Int
addOne (TInt a) = TInt $ a + 1

However, I would like to be able to declare a heterogeneous list like so:

zeros :: [Toy a]
zeros =  [TBool False, TInt 0]

I tried using an empty type class to restrict the type on a by:

class Unify a
instance Unify Bool
instance Unify Int

zeros :: Unify a => [Toy a]
zeros =  [TBool False, TInt 0]

But the above would fail to compile. I was able to use existential quantification to do get the following:

data T = forall a. (Forget a, Show a) => T a

instance Show T where
  show (T a) = show a

class (Show a) => Forget a
instance Forget (Toy a)
instance Forget T

zeros :: [T]
zeros = [T (TBool False), T (TInt 0)]

But this way, I cannot apply a function that was based on the specific type of a in Toy a to T e.g. addOne above.

In conclusion, what are some ways I can create a heterogeneous list without forgetting/losing the phantom variable?


Solution

  • Start with the Toy type:

    data Toy a where
      TBool :: Bool -> Toy Bool
      TInt :: Int -> Toy Int
    

    Now you can wrap it up in an existential without over-generalizing with the class system:

    data WrappedToy where
      Wrap :: Toy a -> WrappedToy
    

    Since the wrapper only holds Toys, we can unwrap them and get Toys back:

    incIfInt :: WrappedToy -> WrappedToy
    incIfInt (Wrap (TInt n)) = Wrap (TInt (n+1))
    incIfInt w = w
    

    And now you can distinguish things within the list:

    incIntToys :: [WrappedToy] -> [WrappedToy]
    incIntToys = map incIfInt
    

    Edit

    As Cirdec points out, the different pieces can be teased apart a bit:

    onInt :: (Toy Int -> WrappedToy) -> WrappedToy -> WrappedToy
    onInt f (Wrap t@(TInt _)) = f t
    onInt _ w = w
    
    mapInt :: (Int -> Int) -> Toy Int -> Toy Int
    mapInt f (TInt x) = TInt (f x)
    
    incIntToys :: [WrappedToy] -> [WrappedToy]
    incIntToys = map $ onInt (Wrap . mapInt (+1))
    

    I should also note that nothing here so far really justifies the Toy GADT. bheklilr's simpler approach of using a plain algebraic datatype should work just fine.