这个 GADT 是否真的具有类型角色代表性

Question

此数据类型可以有type role HCons' representational representational，它允许使用coerce 添加或删除应用于元素的新类型，而无需遍历列表。

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

但是，这些列表的语法不如以下 GADT 的语法好

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

我有一个convert between these two representations 的课程，例如Prime (HList [a,b]) ~ HCons' a (HCons' b HNil')。那个班会做吗

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

安全吗？

Answer 1

我认为仅存在转换是不够的。例如，下面的代码也让我可以在 GADT 和可强制类型对之间进行转换，但直接强制 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)

我还可以简单地定义一个类似于Prime 的UnFoo 类型函数。

我认为这两个示例之间的主要区别在于，在我的示例中，Age 和 Int 具有相同的表示，而在您的示例中，'[] 和 e':l 的表示不同。

所以仍然有理由说，正如您在标题中所建议的那样，l 具有类型角色表示，因为很明显HList l1 和 HList l2 具有相同的表示，如果 l1 和 @ 987654332@具有相同的表示。

但是，由于理论上表示是依赖于实现的，我认为在 GHC 直接接受之前，您永远不会认为这是绝对安全的。