I'm trying to use :~: from Data.Type.Equality to determine type equality at compile time. My expectation is that it behaves along the line of Scala's standard way of determining type equality:

case class Equals[A >: B <:B , B]()

Equals[Int, Int]     // compiles fine
Equals[String, Int]  // doesn't compile

So I tried

foo :: Int :~: Bool
foo = undefined

which I would expect to fail since Int :~: Bool is inhabitable. But it compiles just fine.

• How is :~: supposed to work? The documentation of Data.Type.Equality is pretty impenetrable to me and I was not able to find a succinct example anywhere.

• Maybe I'm completely off the track. In that case, how could I achieve the semantics of the Equals example in Haskell?

CodePudding user response：

Much as we Haskellers often pretend otherwise, every normal¹ type in Haskell is inhabited. That includes data Void, and it includes a :~: b for all a and b. Besides the polite values we usually acknowledge, there is also the bottom value.

undefined :: a is one way of producing the bottom value in any type a. So in particular undefined :: Int :~: Bool, and thus your code is perfectly type correct.

If you want a type equality that simply fails to compile if the equality can't be proved at compile time, then you want a type equality constraint (which is the ~ operator), not the :~: type. You use that like this:

foo :: Int ~ Int => ()   -- compiles fine
foo = ()

bar :: Int ~ Bool => ()  -- does technically compile
bar = ()

bar compiles only because constraints are assumed in the body of a function that has the constraints. But any attempt to call bar requires the compiler is able to prove the constraints in order to compile the call. So this fails:

baz :: ()
baz = bar

:~:, however, is not a constraint (it doesn't go left of the => arrow in types), but an ordinary type. a :~: b is the type of values that serve as a runtime proof that the type a is equal to the type b. If in fact they are not equal, your program won't fail to compile just before you expressed the type a :~: b; rather you just won't be able to actually come up with a value of that type (other than bottom).

In particular, a :~: b is a type that has a data constructor: Refl. To usefully use it, you usually require a a :~: b as an argument. and then pattern match on it. Within the scope of the pattern match (i.e. the body of a case statement), the compiler will use the assumption that the two types are equal. Since pattern matching on the bottom value will never succeed (it might throw an exception, or it might compute forever), the fact that you can always provide bottom as a "proof" that a :~: b doesn't actually cause huge problems; you can lie to the compiler, but it will never execute code that depended on your lie.

Examples corresponding to those in the OP would be:

foo :: Int :~: Int -> ()
foo proof
  = case proof of
      Refl  -> ()

bar :: Int :~: Bool -> ()
bar proof
  = case proof of
      Refl  -> ()

bar can exist even though it needs an impossible proof. We can even call bar with something like bar undefined, making use of the bottom value in the type Int :~: Bool. This won't be detected as an error at compile time, but it will throw a runtime exception (if it's actually evaluated; lazy evaluation might avoid the error). Whereas foo can simply be called with foo Refl.

:~: (and ~) is of course much more usefully used when the two types are (or contain) variables, rather than simple concrete types like Int and Bool. It's also frequently combined with something like Maybe so you have a way of expressing when the types are not proven to be equal. A slightly less trivial example would be:

strange :: Maybe (a :~: b) -> a -> b -> [a]
strange Nothing x _ = [x]
strange (Just Refl) x y
  = [x, y]

strange takes a maybe-proof that the types a and b are equal, and a value of each. If the maybe is Nothing, then the types might not be equal, so we can only put x in the list of a. If we get Just Refl, however, then a and b are actually the same type (inside the pattern match only!), so it's valid to put x and y in the same list.

But this does show a feature of :~: that cannot be achieved with ~. We can still call strange even when we want to pass it two values of different types; we just in that case are forced to pass Nothing as the first value (or Just undefined, but that won't get us anything useful). It allows us to write code that contemplates that a and b could be equal, without forcing a compilation failure if they actually aren't. Whereas a ~ b (in the constraints) would only allow us to require that they definitely are equal, and provably so at compile time.

¹ Where "normal type" means a member of the kind Type AKA *.