其中Data.Type.Equality定义了两个类型级别的等式：:~:和:~~:。据说它们分别代表同质平等和异质平等，但我并没有真正看到它们之间有什么区别。它是什么？
老实说，由于类型系统中值、类型和种类之间的严格边界，我没有看到在 Haskell 类型中实现真正的异构平等的方法。
chi*_*chi 12
区别在于它们的种类：
type (:~:) :: k -> k -> Type
type (:~~:) :: k1 -> k2 -> Type
前者只接受两个具有相同类型的类型参数，而后者则没有这样的限制。
该类型Bool :~: Maybe是不善意的（它将触发善意错误），而是Bool :~~: Maybe善意的。后者是空的，但至少我们可以在不触发错误的情况下编写它。
这非常简单。
ghci> :k (:~:)
(:~:) :: k -> k -> *
ghci> :k (:~~:)
(:~~:) :: k1 -> k2 -> *
请注意，Data.Type.Equality声明:~~:是“种类异构命题相等”（强调我的），因此您需要查看种类。
基本上:~:就像术语级别一样==，使用它要求您检查相等性的两种类型是同一类型的成员。不同类型的类型（例如不同类型的术语）绝对不相等，但是使用:~:（例如 with ==）你甚至会因为思考这个问题而被拉起来。
但:~~:即使您尚未确定这两种类型是否属于同一类型，也可以使用。Refl :: a :~~: b当类型（以及种类）不相等时，您将无法构造 a ，但是a :~~: b当它们没有相同的种类时，GHC 可以考虑（空）类型的存在，这与 不同a :~: b。
所以你可以:~~:在某些不能使用的情况下使用:~:. 但有时这种灵活性实际上是一个问题。如果您希望两侧具有相同的类型，请将它们与添加:~: 该信息给编译器（可能需要它来解析类型类实例或类型族等）。如果您使用:~~:它，除了在构造函数上的实际模式匹配范围内之外Refl，它不会说明类型是否相等，因此您可能必须想出另一种方法来添加有关类型相等的信息（如果这是您想要的）。