提问人：radrow 提问时间：2/24/2022 更新时间：2/24/2022 访问量：860
：~： 和 ：~~： equalities 和有什么不一样？
What is the difference between :~: and :~~: equalities?
问：
在 Data.Type.Equality 中，定义了两个类型级等式：和 。据说它们分别代表同质和异质平等，但我真的看不出它们之间有任何区别。这是什么？:~::~~:
老实说，我看不出有什么方法可以在 Haskell 类型中实现真正的异构相等，因为类型系统中的值、类型和种类之间存在严格的边界。
答：
12赞
chi
2/24/2022
#1
区别在于它们的种类：
type (:~:) :: k -> k -> Type
type (:~~:) :: k1 -> k2 -> Type
前者只接受两个具有相同类型的类型参数，而后者则没有这样的限制。
该类型是 bad-kinded（它会触发 kind 错误），而 well 是 well-kinded。后者是空的，但至少我们可以在不触发错误的情况下编写它。Bool :~: MaybeBool :~~: Maybe
7赞
Ben
2/24/2022
#2
这很简单。
ghci> :k (:~:)
(:~:) :: k -> k -> *
ghci> :k (:~~:)
(:~~:) :: k1 -> k2 -> *
请注意，Data.Type.Equality 声明这是“种类异构命题相等”（强调我的），因此您需要查看种类。:~~:
基本上类似于术语级别，因为使用它需要您要检查相等的两种类型是同一类型的成员。不同种类的类型（如不同类型的术语）绝对不相等，但是使用（like with）时，您甚至会因为考虑问题而被拉起。:~:==:~:==
但是，即使您尚未确定这两种类型具有相同的类型，也可以使用。当类型（以及种类）不相等时，您将无法构造 a，但是当它们没有相同的类型时，GHC 可以考虑（空）类型的存在，这与 .:~~:Refl :: a :~~: ba :~~: ba :~: b
因此，您可以在某些无法使用的情况下使用 .但有时这种灵活性实际上是一个问题。如果希望两端具有相同的类型，则将它们与编译器进行比较会为编译器添加该信息（编译器可能需要它来解析类型类实例或类型系列等）。如果你使用它，除了在构造函数的实际模式匹配范围内之外，没有说明种类相等，所以如果你想要的话，你可能必须想出另一种方法来添加关于种类相等的信息。:~~::~::~::~~:Refl
评论
0赞
radrow
2/24/2022
那使用那有什么意义呢？:~::~~:
2赞
leftaroundabout
2/24/2022
@radrow与大多数“我为什么要使用更强的类型”的问题几乎相同：它有助于弄清楚如何编写代码并尽早发现错误。
1赞
Ben
2/24/2022
@radrow嗯，一方面，它只是更老了。正如文档所说，可以追溯到 4.7，而只出现在 4.10 中。我不知道是 4.7 中还不能写，还是没有人想到它，但在 4.10 中添加另一种类型而不是更改现有类型可以避免向后不兼容。而且，要求其参数相同类型的事实将该信息添加到您的程序中，有时这很方便（出于同样方便的原因;仅链接两个类型/种类变量本身就很有用）。:~:base:~~:base:~~::~:asTypeOf
2赞
Ben
2/24/2022
@radrow 值得记住的是，到目前为止，最常见的用途（至少我很确定）将同时具有两种类型的 /，因此没有必要支持不同的类型。很多时候，使用哪一个不会有什么区别，但偶尔这将是确定 GHC 变量类型的唯一方法，它将有助于解析类型类实例或其他东西。如果你需要那种异构版本，你可能正在做一些更高级的事情，并希望能认识到你需要它。Type*
评论
Type.Reflection需要异构相等