Converting between heterogeneous lists

Question

I have two heterogeneous list structures. The first HList is a normal heterogeneous list, the second Representation is a heterogeneous list where all the members are sets.

{-# Language KindSignatures, DataKinds, TypeOperators, TypeFamilies, GADTs, FlexibleInstances, FlexibleContexts #-}

import Data.Kind
import Data.Set

data Representation (a :: [Type]) where
  NewRep :: Representation '[]
  AddAttribute :: (Ord a, Eq a) => Set a -> Representation b -> Representation (a ': b)

(%>) :: (Ord a, Eq a) => [a] -> Representation b -> Representation (a ': b)
(%>) = AddAttribute . fromList
infixr 6 %>

-- | A HList is a heterogenenous list.
data HList (a :: [Type]) where
  HEmpty :: HList '[]
  (:>) :: a -> HList b -> HList (a ': b)
infixr 6 :>

^{(I've made these instances of Show at the bottom if that is helpful.)}

Now I have a bunch of functions that work on HLists but don't work on Representations. I could rewrite all the functions but that's a big pain. I'd rather if there was some way to make Representations in HLists and back. That way I can use all the relevant functions without having to redefine them. So I started to do this. It was pretty easy to make a function that goes from Representations to HLists:

type family Map (f :: Type -> Type) (xs :: [Type]) :: [Type] where
  Map f '[] = '[]
  Map f (a ': b) = f a ': Map f b

-- | soften takes an attribute representation and converts it to a heterogeneous list.
soften :: Representation a -> HList (Map Set a)
soften NewRep = HEmpty
soften (AddAttribute a b) = a :> soften b

However the other way is quite a bit harder. I tried the following:

-- | rigify takes a heterogeneous list and converts it to a representation
rigify :: HList (Map Set a) -> Representation a
rigify HEmpty = NewRep
rigify (a :> b) = AddAttribute a $ rigify b

However this fails, the compiler is not able to deduce that a ~ '[] in the first line. And fails in a similar fashion on the second.

It appears to me that the compiler can't reason backwards in the same way it can forward. This is not really very surprising, but I don't know exactly what the issue is, so I'm not really very sure how to get the compiler to reason correctly. My thought was to make a type family that is the reverse of Map like so:

type family UnMap (f :: Type -> Type) (xs :: [Type]) :: [Type] where
  UnMap f '[] = '[]
  UnMap f ((f a) ': b) = a ': UnMap f b

and then rewrite rigify in terms of UnMap instead of Map:

-- | rigify takes a heterogeneous list and converts it to a representation
rigify :: HList a -> Representation (UnMap Set a)
rigify HEmpty = NewRep
rigify (a :> b) = AddAttribute a $ rigify b

This seems to reduce the problem but it still doesn't compile. This time we are having the issue that a in the second line cannot be shown to be of type Set x which is required for AddAttribute. This makes total sense to me but I don't know how I could remedy the issue.

How can I convert from a heterogeneous list to a Representation?

---

Show instances:

instance Show (HList '[]) where
  show HEmpty = "HEmpty"
instance Show a => Show (HList '[a]) where
  show (a :> HEmpty) = "(" ++ show a ++ " :> HEmpty)"
instance (Show a, Show (HList (b ': c))) => Show (HList (a ': b ': c)) where
  show (a :> b) = "(" ++ show a ++ " :> " ++ tail (show b)

instance Show (Representation '[]) where
  show NewRep = "NewRep"
instance Show a => Show (Representation '[a]) where
  show (AddAttribute h NewRep) = '(' : show (toList h) ++ " %> NewRep)"
instance (Show a, Show (Representation (b ': c))) => Show (Representation (a ': b ': c)) where
  show (AddAttribute h t) = '(' : show (toList h) ++ " %> " ++ tail (show t)

Answer 1

HList is usually wrong. What I mean is that as soon as you try to do very much, you're likely to end up with lots of problems. You can solve the problems, but it's annoying and often inefficient. There's another, very similar, construction that can go a lot further before it falls down.

data Rec :: [k] -> (k -> Type) -> Type where
  Nil :: Rec '[] f
  (:::) :: f x -> Rec xs f -> Rec (x ': xs) f

type f ~> g = forall x. f x -> g x

mapRec :: (f ~> g) -> Rec xs f -> Rec xs g
mapRec _ Nil = Nil
mapRec f (x ::: xs) = f x ::: mapRec f xs

Note that you can do a certain sort of mapping without bringing in any type families at all!

Now you can define

data OSet a = Ord a => OSet (Set a)
newtype Representation as = Representation (Rec as OSet)

An awful lot of generic HList functions can be rewritten very easily to support Rec instead.

You can write bidirectional pattern synonyms to simulate your current interface if you like.