What is the difference between :~: and :~~: equalities?-CodePudding

In Data.Type.Equality there are two type-level equalities defined: :~: and :~~:. They are said to represent homogenous and heterogenous equality respectively, but I don't really see any differences between them. What is it?

To be honest I don't see a way for having a real heterogenous equality in Haskell type, due to the strict border between values, types and kinds in the typesystem.

CodePudding user response：

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.

CodePudding user response：

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.