告诉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/