list of heterogeneous GADTs

Question

I have a GADT like the following

data MyTypes
    = MyInt
    | MyDouble

data Test (t :: MyTypes) where
    A :: Int -> Test 'MyInt
    B :: Double -> Test 'MyDouble

this allows me to to keep track of the value contained in the Test values at the type level, so that I can also do something like

data Test2 (t :: MyTypes) where
    A2 :: Test 'MyInt -> Test2 'MyInt
    B2 :: Test 'MyDouble -> Test2 'MyDouble

and pass along the information.

However, if I want to have a list of Test values with different MyTypes, like

myData :: [Test (t :: MyTypes)]
myData =
    [ A (3 :: Int)
    , B (5.0 :: Double)
    ]

I get as expected ‘t’ is a rigid type variable bound error message.

I tried to use existential types to overcome the problem of rigid type variables, but then I lose the ability to pass on the type level information about MyType.

How should I approach such a problem?

Can you elaborate on how would you like to "pass on the type level information" when using a list which has heterogeneous tags? I'd think that either you can do that with existentials or the task is impossible to achieve in a type safe way. — chi
You don't lose the ability to pass on the type-level information about MyType; you're just required to re-wrap in an existential after you've passed it on. But to set you straight we'd have to see what it was you tried that didn't work. — Daniel Wagner
Another direction is a list type that exposes the types of its contents. See, for example, Data.Vinyl.Core in the vinyl package. — dfeuer

Jon Purdy Jon Purdy · Accepted Answer · 2018-03-27T21:13:50

The solution here is an existential:

data Test a where
  A :: Int -> Test Int
  B :: Double -> Test Double

data SomeTest where
  SomeTest :: Test a -> SomeTest

myData :: [SomeTest]
myData =
  [ SomeTest (A (3 :: Int))
  , SomeTest (B (5.0 :: Double))
  ]

This just changes how you can consume this type. You can recover type information by pattern-matching on it:

consume :: Test a -> Int
consume (A a) = a + 1
consume (B b) = truncate b

map (\ (SomeTest x) -> consume x) myData :: [Int]

With RankNTypes you can unwrap it with a continuation that recovers the type:

test :: (forall a. Test a -> r) -> SomeTest -> r
test k (SomeTest x) = k x

test (\ x -> case x of
  A a -> a + 1 {- ‘a’ is known to be ‘Int’ here -}
  B b -> truncate b {- ‘b’ is known to be ‘Double’ here -})
  :: SomeTest -> Int

An existential without any typeclass constraints is mostly useful when you’re using it to pack multiple things together in a sort of “module” where they all must agree on the type, but that type is opaque from the outside. This constrains the operations that the consumer can do—for example, consider a pair of a request and a variable to store the result of that request:

data SomeRequest where
  SomeRequest :: IO a -> IORef a -> SomeRequest

fetchRequests :: [SomeRequest] -> IO ()
fetchRequests = traverse_ fetchRequest
  where

    -- ‘fetchRequest’ controls the fetching strategy (sync/async)
    -- but can’t do anything with the fetched value
    -- other than store it in the ‘IORef’.
    fetchRequest :: SomeRequest -> IO ()
    fetchRequest (SomeRequest request result) = do
      value <- request
      writeIORef result value

If you have a totally polymorphic type, like:

data Test a where
  Test :: a -> Test a

Then you can recover more interesting information about the type by adding typeclass constraints. For example, if you want full dynamic information, you can get it with Typeable:

data SomeTest where
  SomeTest :: Typeable a => Test a -> SomeTest

test :: (forall a. Typeable a => Test a -> r) -> SomeTest -> r
test k (SomeTest x) = k x

test (\ (Test a) -> case cast a of
  Just a' -> (a' :: Int) + 1
  Nothing -> case cast a of
    Just a' -> length (a' :: String)
    Nothing -> 0)

Most of the time you can use a typeclass with less power than this, depending on the operations you actually need.

list of heterogeneous GADTs

1 Answers