does this GADT actually have type role representational

Question

This data type can have type role HCons' representational representational, which allows using coerce to add or remove newtypes applied to the elements, without needing to traverse the list.

data HNil' = HNil'
data HCons' a b = HCons' a b

However the syntax for those lists is not as nice as those with the following GADT

data HList (l::[*]) where
    HNil  :: HList '[]
    HCons :: e -> HList l -> HList (e ': l)

I have a class to convert between these two representations, such that Prime (HList [a,b]) ~ HCons' a (HCons' b HNil'). Does that class make

coerceHList :: Coercible (Prime a) (Prime b) => HList a -> HList b
coerceHList = unsafeCoerce

safe?

FWIW, yes, I think so. But I don't know enough about the internals of roles to actually make a convincing argument. Your example seems to be another case where the current role system is not quite expressive enough. — kosmikus

GS - Apologise to Monica GS - Apologise to Monica · Accepted Answer · 2014-06-24T05:57:29

I don't think the existence of a conversion on its own is enough. For example, the following also lets me convert between a GADT and a coercible pair of types, but it certainly wouldn't be safe to directly coerce the GADT:

newtype Age = Age Int

data Foo a where
   I :: Bool -> Int -> Foo Int
   A :: Age -> Bool -> Foo Age

class ConvFoo a where
   toFoo :: (Bool, a) -> Foo a
   fromFoo :: Foo a -> (Bool, a)

instance ConvFoo Int where
   toFoo (b, i) = I b i
   fromFoo (I b i) = (b, i)

instance ConvFoo Age where
   toFoo (b, a) = A a b
   fromFoo (A a b) = (b, a)

I could also trivially define an UnFoo type function similar to Prime.

I think the key difference between the two examples is that in mine, Age and Int do have the same representation, whereas in yours '[] and e':l don't have the same representation.

So there's still a case for saying, as you suggest in the title, that l has type role representational, because it's kind of obvious that HList l1 and HList l2 have the same representations if l1 and l2 have the same representations.

However since in theory representations are implementation-dependent, I don't think you can ever consider this absolutely safe until GHC accepts it directly.

does this GADT actually have type role representational

1 Answers