haskell - 通知 Haskell `(Reverse (Reverse 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/