其中Data.Type.Equality定義了兩個型別級別的等式：:~:和:~~:. 據說它們分別代表同質和異質平等，但我真的看不出它們之間有什么區別。它是什么？
老實說，由于型別系統中值、型別和種類之間的嚴格界限，我看不到在 Haskell 型別中實作真正的異構平等的方法。
uj5u.com熱心網友回復：
區別在于它們的種類：
type (:~:) :: k -> k -> Type
type (:~~:) :: k1 -> k2 -> Type
前者只接受兩個具有相同種類的型別引數，而后者沒有這樣的限制。
型別Bool :~: Maybe是 ill-kinded（它會觸發 kind 錯誤），而Bool :~~: Maybeis well-kinded。后者是空的，但至少我們可以在不觸發錯誤的情況下撰寫它。
uj5u.com熱心網友回復：
這很簡單。
ghci> :k (:~:)
(:~:) :: k -> k -> *
ghci> :k (:~~:)
(:~~:) :: k1 -> k2 -> *
請注意，Data.Type.Equality宣告:~~:是“種類異質命題相等”（強調我的），因此您需要查看種類。
基本上:~:就像術語級別一樣==，使用它要求您檢查相等性的兩種型別是同一型別的成員。不同型別的型別（如不同型別的術語）絕對不相等，但使用:~:（如 with ==）你甚至會因為思考這個問題而被拉起來。
但:~~:即使在您尚未確定這兩種型別具有相同種類的情況下也可以使用。Refl :: a :~~: b當型別（以及種類）不相等時，您將無法構造 a ，但a :~~: b與a :~: b.
所以你可以:~~:在一些你不能使用的情況下使用:~:. 但有時這種靈活性實際上是一個問題。如果您希望兩側具有相同的型別，請將它們與編譯器:~: 添加該資訊（可能需要它來決議型別類實體或型別族等）。如果您使用:~~:它，則除了在建構式上的實際模式匹配范圍內之外，沒有說明種類是否相等Refl，因此如果您想要的話，您可能必須想出另一種方法來添加有關種類相等的資訊。
轉載請註明出處，本文鏈接：https://www.uj5u.com/houduan/434055.html