类似GADT类型变量的角色的未来是什么？

Question

昨天的一个问题（链接）中提到了HList（来自HList包）的定义，其中使用了数据家族。基本上：

data family HList (l :: [*])
data instance HList '[] = HNil
newtype instance HList (x ': xs) = HCons1 (x, HList xs)

pattern HCons x xs = HCons1 (x, xs)

与通常的（在我看来更加优雅和直观）GADT定义不同

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

这是因为数据家族版本让我们强制转换（我们只能强制转换 HList（x'：xs）情况，因为它是一个 newtype instance ，但那已经足够了）。而GADT仅推断出 l 的名义角色（从而阻止任何强制转换）。 （我回答中提到的问题具有此的具体示例。）

关于 HList 的作用系统对GADT的缺陷在这个两年前的问题中讨论过。基本上，GHC会自动将任何“类似于GADT”的类型变量标记为名义。

鉴于自那以后一些时间已经过去，并且有关使角色在类型/数据族周围更加灵活的讨论，是否有任何前进之路（即一些现有想法、一些开放的Trac票证、任何事情）可以检查GADT中更有趣的角色（如 HList ）？在这里，GADT或DataKinds和角色之间的相互作用存在一些根本性限制吗？需要实现/创建什么才能使其工作？

- Alec

Answer 1

作者在此提供角色系统。我不知道有什么想法能使我们朝这个方向前进。问题在于，我们需要检查一个微妙的属性，以确保强制转换是安全的。具体来说，我们希望能够将例如 HList [Age, Int, String] 强制转换为 HList [Int, Age, String]，但不能越界到 HList [String, String, Int](或者HList 具有三个元素之外的其他东西)。(在此假设 newtype Age = MkAge Int)。实现这一点需要类似 Very Glorious 角色般的系统--能够准确描述对于这样的 GADT 转换是安全的--但我不知道任何已有的工作向创建这样的系统。

数据族方法之所以可行是因为 GHC 可以看到 HList [Age, Int, String] 实际上和 (Age, (Int, (String, HList '[]))) 是相同的，然后它就了解元组，就可以完成其余工作了。

很抱歉没有鼓励的话，但这似乎远超出了我们现在能做的范围。

- Richard Eisenberg