Where is the Idris == operator useful?

Question

As a beginner in type-driven programming, I'm curious about the use of the == operator. Examples demonstrate that it's not sufficient to prove equality between two values of a certain type, and special equality checking types are introduced for the particular data types. In that case, where is == useful at all?

"of a certain type" meaning what exactly? Sounds like you are aware it's used for types other than those, so does that answer your own question? — OneCricketeer
It's used to compare Nat numbers in one of the examples and I find it puzzling the == operator is not sufficient to prove they are equal. To be more specific, let me put it this way: for what types is the == operator sufficient enough to prove equality? — Attila Karoly
Well, I don't actually know Idris, but I'm imagining simple primitives of numbers and booleans. Maybe strings (assuming it's not like Java) — OneCricketeer

Philip Dorrell Philip Dorrell · Accepted Answer · 2017-07-23T01:40:10

(==) (as the single constituent function of the Eq interface) is a function from a type T to Bool, and is good for equational reasoning. Whereas x = y (where x : T and y : T) AKA "intensional equality" is itself a type and therefore a proposition. You can and often will want to bounce back and forth between the two different ways of expressing equality for a particular type.

x == y = True is also a proposition, and is often an intermediate step between reasoning about (==) and reasoning about =.

The exact relationship between the two types of equality is rather complex, and you can read https://github.com/pdorrell/learning-idris/blob/9d3454a77f6e21cd476bd17c0bfd2a8a41f382b7/finished/EqFromEquality.idr for my own attempt to understand some aspects of it. (One thing to note is that even though an inductively defined type will have decideable intensional equality, you still have to go through a few hoops to prove that, and a few more hoops to define a corresponding implementation of Eq.)

One particular handy code snippet is this:

-- for rel x y, provide both the computed value, and the proposition that it is equal to the value (as a dependent pair)
has_value_dpair : (rel : t -> t -> Bool) -> (x : t) -> (y : t) -> (value: Bool ** rel x y = value)
has_value_dpair rel x y = (rel x y ** Refl)

You can use it with the with construct when you have a value returned from rel x y and you want to reason about the proposition rel x y = True or rel x y = False (and rel is some function that might represent a notion of equality between x and y).

(In this answer I assume the case where (==) corresponds to =, but you are entirely free to define a (==) function that doesn't correspond to =, eg when defining a Setoid. So that's another reason to use (==) instead of =.)

Where is the Idris == operator useful?

2 Answers