How to Compare Types for Equality?

Question

I attempted to compare a String and String, expecting True.

Idris> String == String
Can't find implementation for Eq Type

Then I expected False when comparing a String to a Bool.

Idris> String /= Bool
Can't find implementation for Eq Type

Am I missing an import?

Answer 1

You can't as it would break parametricity, which we have in Idris. We can't pattern match on types. But this would be necessary to write the Eq implementation, for example:

{- Doesn't work!
eqNat : Type -> Bool
eqNat Nat = True
eqNat _ = False -}

Also, if one could pattern match on types, they would be needed in the run-time. Right now types get erased when compiling.

Answer 2

Just to add some simple examples to the above: types can't be pattern matched on, but there's a two parameter type constructor for propositional equality, described in the documentation section on Theorem Proving. Notice that the only constructor, Refl, makes only values of type (=) x x, where both type parameters are the same. (this is ≡ in Agda)

So this will typecheck:

twoPlusTwoEqFour : 2 + 2 = 4
twoPlusTwoEqFour = Refl

so will this:

stringEqString : String = String
stringEqString = Refl

but not this:

stringEqInt : String = Int
stringEqInt = Refl

-- type error: Type mismatch between String and Int

and this needs extra work to prove, because addition is defined by recursion on the left argument, and n + 0 can't be reduced further:

proof : n = n + 0