通知Haskell `(反向(反向xs)) ~ xs`

Question

如果Reverse :: [k] -> [k]是一个类型族，那么Haskell就不能分辨出那个(Reverse (Reverse xs)) ~ xs。有没有一种方法可以让类型系统知道这一点而不需要任何运行时成本？

我很想只使用unsafeCoerce，但这似乎是一种遗憾。

Answer 1

据我所知，在GHC中影响~行为的唯一方法是实际构造a :~: b的一个实例(或类似的；重要的是构造一个术语，向类型检查器“证明”这一点)，然后在Refl构造函数上进行模式匹配，这将需要在运行时评估证明见证。我的理解是，目前GHC中依赖类型的设计仍然需要运行类型相等的所有证明。然而，可以使用GHC的重写规则，在类型检查之后，用一个非常低成本的函数(例如unsafeCoerce Refl :: Reverse (Reverse a) :~: a)替换证明证人，这将使评估成本非常低，但仍然是安全的(因为证明证人已经类型检查，表明如果它终止，它将产生正确的证据)。

有关Haskell中依赖类型的当前状态的更多信息可以在此处找到：https://typesandkinds.wordpress.com/2016/07/24/dependent-types-in-haskell-progress-report/