GADTs or phantom types to type-check function calls but keep homogeneity of type

Question

I assume the following problem can be solved using type arithmetic but haven't found the solution yet.

Problem

I have a finite map from strings to values (using Tries as implementation) that I parse from a binary/text file (json, xml, ...).

type Value = ...
type Attributes = Data.Trie Value 
data Object = Object Attributes

Each map has the same type of values but not the same set of keys. I group maps with the same set of keys together to be able to prevent having to type-switch all the time I have a specialised function that requires certain keys:

data T1
data T2 
...

data Object a where
    T1 :: Attributes -> Object T1
    T2 :: Attributes -> Object T2
    ...

This allows me to write something like:

f1 :: Object T1 -> ...

instead of

f1 :: Object ->
f1 o | check_if_T1 o = ...

This works but has two disadvantages:

1. Homogeneous lists of Object now become heterogeneous, i.e. I cannot have a list [Object] anymore.

2. I need to write a lot of boilerplate to get/set attributes:

   get :: Object a -> Attributes
   get (T1 a) = a
   get (T2 a) = a
   ...
   

Question

1. Is there a better way to specialise functions depending on the constructor of an ADT?

2. How could I regain the ability to have a list [Object]? Is there a specialized version of Dynamic that only allows certain types? I thought about wrapping the Object again, but this would add a lot of boilerplate. For instance,

   data TObject = TT1 T1 | TT2 T2 ...

What I need is:

get :: a -> TObject -> Object a

So that I can then derive:

collect :: a -> [TObject] -> [Object a]

I looked into HList but I don't think it fits my problem. Especially, since the order of types in [Object] is not known at compile time.

It sounds to me like this can be solved using functional dependency / type arithmetic but I simply haven't found a nice way yet.

Answer 1

1. If all the constructors return a monomorphic Object type and there's no recursion, you might want to think about just using separate types. Instead of

   data T1
   data T2
   
   data Object a where
       T1 :: Attributes -> Object T1
       T2 :: Attributes -> Object T2
   

   consider

   data T1 = T1 Attributes
   data T2 = T2 Attributes
   

2. Dynamic is one way, and using the above you could just add deriving Typeable and be done. Alternately, you can do it by hand:

   data TSomething = It's1 T1 | It's2 T2
   
   getT1s :: [TSomething] -> [T1]
   getT2s :: [TSomething] -> [T2]
   getT1s xs = [t1 | It's1 t1 <- xs]
   getT2s xs = [t2 | It's2 t2 <- xs]
   

   As you say, this involves a bit of boilerplate. The Typeable version looks a bit nicer:

   deriving Typeable T1
   deriving Typeable T2
   
   -- can specialize at the call-site to
   -- getTs :: [Dynamic] -> [T1] or
   -- getTs :: [Dynamic] -> [T2]
   getTs :: Typeable a => [Dynamic] -> [a]
   getTs xs = [x | Just x <- map fromDynamic xs]