question from yesterday有一个使用数据族的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)而不是通常的（IMO更优雅和直观）GADT定义
data HList (l :: [*]) where
HNil :: HList '[]
HCons :: x -> HList xs -> HList (x ': xs)这是因为数据族版本允许我们强制（我们只能强制HList (x ': xs)，因为它是newtype instance，但这就足够了），而GADT只能为l推断一个名义角色（因此阻止了任何强制）（My answer to the mentioned question has a concrete example of this）。
在two year old question中讨论了与HList相关的GADT角色系统的缺陷。基本上，GHC自动将任何“GADT类”类型变量标记为nominal。
考虑到从那时到there is talk of making roles more flexible around type/data families已经过去了一段时间，是否有任何前进的道路（即一些现有的想法，一些开放的Trac票证，任何真正的东西）来检查GADT中更有趣的角色（如HList）？这里是否有一些GADT或DataKinds和角色的相互作用的基本限制？需要实现/创建什么才能工作？
1条答案
按热度按时间6kkfgxo01#
作者的角色系统在这里。我知道没有想法将推动我们在这个方向前进。问题是，我们需要检查一个微妙的财产，以确保强制是安全的。具体来说，我们希望能够将例如
HList [Age, Int, String]强制为HList [Int, Age, String]，但不能强制为HList [String, String, Int]（或者HList具有三个元素以外的元素）。（这里我假设是newtype Age = MkAge Int。）实现这一点需要一些非常光荣的角色类系统--能够准确地描述什么样的强制对这样的GADT是安全的--而我不知道。I don“我不知道有任何建立这样一个系统工作。数据族方法起作用的原因是GHC可以看到
HList [Age, Int, String]实际上与(Age, (Int, (String, HList '[])))相同，然后它对元组的了解足以完成其余的工作。很抱歉，我没有鼓励你，但这似乎远远超出了我们现在所能做的。