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.

Answer 2

Use a type class

The desired behavior for rigify can be obtained by using a multi paramater type class instead.

class Rigible (xs :: [Type]) (ys :: [Type]) | xs -> ys where
  rigify :: HList xs -> Representation ys

instance Rigible '[] '[] where
  rigify HEmpty = NewRep

instance (Ord h, Rigible t t') => Rigible (Set h ': t) (h ': t') where
  rigify (a :> b) = AddAttribute a $ rigify b

Here we use a multiparam type class Rigible with an attached function rigify. Our two parameters are the type for the representation and the type for the heterogeneous list. They are functionally dependent to avoid ambiguity.

In this way only HLists that are composed entirely of sets are Rigible. From here you can even add the definition of soften to Rigible as well.

-- | soften takes a representation and converts it to a heterogeneous list.
-- | rigify takes a heterogeneous list and converts it to a representation.
class Rigible (xs :: [Type]) (ys :: [Type]) | xs -> ys where
  rigify :: HList xs -> Representation ys
  soften :: Representation ys -> HList xs

instance Rigible '[] '[] where
  rigify HEmpty = NewRep
  soften NewRep = HEmpty

instance (Ord h, Rigible t t') => Rigible (Set h ': t) (h ': t') where
  rigify (a :> b) = AddAttribute a $ rigify b
  soften (AddAttribute a b) = a :> soften b

This requires the additional pragma

{-# Language MultiParamTypeClasses, FunctionalDependencies, UndecidableInstances #-}

Answer 3

1. Ord a makes Eq a redundant: Ord a implies Eq a because class Eq a => Ord a.

   data Representation (a :: [Type]) where
     ...
     AddAttribute :: Ord a => Set a -> Representation b -> Representation (a ': b)
   
   (%>) :: Ord a => [a] -> Representation b -> Representation (a ': b)
   

2. You can't write rigify with quite this type: soften throws away the Ord-ness stored at each AddAttribute. You can use

   data OSet a where OSet :: Ord a => Set a -> OSet a
   soften :: Representation xs -> HList (Map OSet xs)
   rigify :: HList (Map OSet xs) -> Representation xs
   

   and you may apply the age old "list of pairs is a pair of lists" trick on top of that

   type family AllCon (xs :: [Constraint]) :: Constraint where
     AllCon '[] = ()
     AllCon (x : xs) = (x, AllCon xs)
   data Dict c = c => Dict
   soften :: Representation xs -> (HList (Map Set xs), Dict (AllCon (Map Ord xs)))
   rigify :: AllCon (Map Ord xs) => HList (Map Set xs) -> Representation xs
   

   though I shall go with the former because it is more concise.

3. Use unsafeCoerce. The alternative is to reify some type information with a GADT and write a proof. While that is good practice, that requires you to drag around (potentially large) values that represent things that are simply true, so you'll end up using unsafeCoerce anyway to avoid them. You can skip the proofs and go to the end products directly.

   -- note how I always wrap the unsafeCoerce with a type signature
   -- this means that I reduce the chance of introducing something actually bogus
   -- I use these functions instead of raw unsafeCoerce in rigify, because I trust
   -- these to be correct more than I trust unsafeCoerce.
   mapNil :: forall f xs. Map f xs :~: '[] -> xs :~: '[]
   mapNil Refl = unsafeCoerce Refl
   
   data IsCons xs where IsCons :: IsCons (x : xs)
   mapCons :: forall f xs. IsCons (Map f xs) -> IsCons xs
   mapCons IsCons = unsafeCoerce IsCons
   
   rigify :: HList (Map OSet xs) -> Representation xs
   rigify HEmpty = case mapNil @OSet @xs Refl of Refl -> NewRep
   rigify (x :> xs) = case mapCons @OSet @xs IsCons of
                           IsCons -> case x of OSet x' -> AddAttribute x' (rigify xs)
   

   A proper proof would go as follows:

   data Spine :: [k] -> Type where
     SpineN :: Spine '[]
     SpineC :: Spine xs -> Spine (x : xs)
   
   mapNil' :: forall f xs. Spine xs -> Map f xs :~: '[] -> xs :~: '[]
   mapNil' SpineN Refl = Refl
   mapNil' (SpineC _) impossible = case impossible of {}
   
   mapCons' :: forall f xs. Spine xs -> IsCons (Map f xs) -> IsCons xs
   mapCons' SpineN impossible = case impossible of {}
   mapCons' (SpineC _) IsCons = IsCons
   

   For every list xs, there is one and only one (fully defined) value of Spine xs (it is a singleton type). To get from real proofs (like mapNil') to their convenience versions (like mapNil), remove all the singleton arguments and make sure the return type is a mere proposition. (A mere proposition is a type with 0 or 1 values.) Replace the body with one that deeply evaluates the remaining arguments and uses unsafeCoerce for the return value.