:~: 和 :~~: 等式有什么区别？答案

【问题标题】：What is the difference between :~: and :~~: equalities?:~: 和 :~~: 等式有什么区别？
【发布时间】：2022-02-24 20:52:51
【问题描述】：

在Data.Type.Equality 中定义了两个类型级别的等式：:~: 和:~~:。据说它们分别代表同质和异质平等，但我真的看不出它们之间有什么区别。这是什么？

说实话，由于类型系统中值、类型和种类之间的严格界限，我看不到在 Haskell 类型中实现真正的异构平等的方法。

【问题讨论】：

几篇论文：A reflection on types, An overabundance of equality: Implementing kind equalities into Haskell
Type.Reflection 需要异构相等

标签： haskell equality

【解决方案1】：

区别在于它们的种类：

type (:~:)  :: k  -> k  -> Type
type (:~~:) :: k1 -> k2 -> Type

前者只接受两个相同种类的类型参数，而后者没有这种限制。

Bool :~: Maybe 类型不善（会触发 kind 错误），而 Bool :~~: Maybe 类型善意。后者是空的，但至少我们可以在不触发错误的情况下编写它。

【讨论】：

【解决方案2】：

这很简单。

ghci> :k (:~:)
(:~:) :: k -> k -> *

ghci> :k (:~~:)
(:~~:) :: k1 -> k2 -> *

请注意，Data.Type.Equality 声明 :~~: 是“种类异构命题相等”（强调我的），因此您需要查看种类。

基本上:~: 类似于术语级别的==，因为使用它要求您检查相等性的两种类型是同一类型的成员。不同种类的类型（如不同类型的术语）绝对不相等，但:~:（如==）即使考虑问题也会被拉起来。

但是:~~: 可以使用，即使您还没有确定这两种类型具有相同的种类。当类型（以及种类）不相等时，您将无法构造 Refl :: a :~~: b，但 GHC 可以考虑（空）类型 a :~~: b 在它们不具有相同种类时的存在，不像a :~: b。

因此，您可以在某些无法使用:~: 的情况下使用:~~:。但有时这种灵活性实际上是一个问题。如果您希望两侧具有相同的类型，请将它们与 :~: 进行比较添加编译器的信息（可能需要它来解析类型类实例或类型族等）。如果您使用:~~:，除了在Refl 构造函数上的实际模式匹配范围内，它没有说明种类是否相等，因此您可能必须想出另一种方法来添加有关种类相等的信息，如果这就是你想要的。

【讨论】：

那么使用:~: 而不是:~~: 有什么意义呢？
@radrow 与大多数“我为什么要使用更强的类型”问题的观点几乎相同：它有助于弄清楚如何编写代码并及早发现错误。
@radrow 好吧，一方面它更老了。正如文档所说，:~: 可以追溯到base 4.7，而:~~: 仅出现在base 4.10 中。我不知道:~~: 是否还不能在 4.7 中编写，或者只是没有人想到它，但是在 4.10 中添加另一种类型而不是更改现有类型可以避免向后不兼容。而且，:~: 要求它的参数是同一类型的事实添加到您的程序中，有时这很方便（出于同样的原因 asTypeOf 很方便；只是链接两个类型/种类变量本身就很有用）。
@radrow 值得牢记的是，far 最常见的用途（至少我很确定）将有两种类型 Type/@987654348 @，所以没有需要来支持不同的种类。很多时候它只是不会影响你使用哪个，但偶尔这将是唯一确定 GHC 变量类型的东西，它将有助于解析类型类实例或其他东西。如果您需要种类不同的版本，您可能正在做一些更高级的事情，并希望能够认识到您需要它。