当前位置：文江博客话题详情

:~: 和 :~~: 相等有什么区别？

发布于 2025-01-09 19:39:29 字数 333 浏览 1 评论 0原文

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

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

原文

分享到QQ

分享到微博

如果你对这篇内容有疑问，欢迎到本站社区发帖提问参与讨论，获取更多帮助，或者扫码二维码加入 Web 技术交流群。

发布评论

需要登录才能够评论，你可以免费注册一个本站的账号。

你げ笑在眉眼 2025-01-16 19:39:29

区别在于它们的类型：

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

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

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

The difference is in their kinds:

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

The former only accepts two type arguments having the same kind, while the latter has no such restriction.

The type Bool :~: Maybe is ill-kinded (it will trigger a kind error), while Bool :~~: Maybe is well-kinded. The latter is empty, but at least we can write it without triggering errors.

回复收藏 0 原文

国粹 2025-01-16 19:39:29

这非常简单。

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

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

请注意 Data.Type.Equality< /code>声明 :~~: 是“种类异构命题相等”（强调我的），所以你需要查看种类。

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

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

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

It's pretty straightforward.

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

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

Note that Data.Type.Equality states that :~~: is "Kind heterogeneous propositional equality" (emphasis mine), so you need to look at the kinds.

Basically :~: is like term-level == in that using it requires that the two types you're checking equality for are members of the same kind. Types in different kinds (like terms in different types) are definitely not equal, but with :~: (like with ==) you get pulled up for even contemplating the question.

But :~~: can be used even when you haven't established that the two types have the same kind. You won't be able to construct a Refl :: a :~~: b when the types (and thus the kinds) aren't equal, but GHC can contemplate the existence of the (empty) type a :~~: b when they don't have the same kind, unlike with a :~: b.

So you can use :~~: in some situations where you couldn't use :~:. But sometimes that flexibility is actually a problem. If you wanted the two sides to have the same kind, comparing them with :~: adds that information for the compiler (which might need it to resolve type class instances or type families or etc). If you use :~~: it says nothing about the kinds being equal except within the scope of an actual pattern match on the Refl constructor, so you might have to come up with another way to add the information about the kinds being equal if that's what you wanted.

回复收藏 0 原文

~没有更多了~