CODEWITHSUNDEEP
idris
Kevin Meredith
Kevin Meredith

Reputation: 41909

How to Compare Types for Equality?

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?

Upvotes: 6

Views: 1182

Answers (2)

brainrape
brainrape

Reputation: 346

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

Upvotes: 1

xash
xash

Reputation: 3722

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.

Upvotes: 6

Related Questions