ハスケルに `（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/