13

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?

aavogt
  • 1,308
  • 6
  • 14
  • 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 Jun 15 '14 at 20:30

1 Answers1

2

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.

Ganesh Sittampalam
  • 28,821
  • 4
  • 79
  • 98
  • I'm not so sure about "it's kind of obvious that HList l1 and HList l2 have the same representations if l1 and l2 have the same representations". We could write `HCons :: (el ~ (e ': l)) => e -> HList l -> HList el`. Then it is possible ghc stores something for `el ~ (e ': l)` that references the original `e, el, l` types, and not the ones that are currently in the constructor? – aavogt Jun 24 '14 at 15:31
  • Even then, every `HCons` would still have the same surface representation as every other `HCons`, wouldn't it? So if `e` and `HList l` also had the same representations then the whole `HCons` would. – Ganesh Sittampalam Jun 24 '14 at 21:30
  • I think the key point is that `':` and `'[]` are concrete types that must be different, so there's no risk of confusing `HCons` and `HNil`. I'm not at all sure how to formulate the condition precisely though! – Ganesh Sittampalam Jun 24 '14 at 21:32