Search code examples
idris

Where is the Idris == operator useful?

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?

Solution

  • You still need good old equality because sometimes you can't prove things. Sometimes you don't even need to prove. Consider next example:

    countEquals : Eq a => a -> List a -> Nat
countEquals x = length . filter (== x)

    You might want to just count number of equal elements to show some statistics to user. Another example: tests. Yes, even with strong type system and dependent types you might want to perform good old unit tests. So you want to check for expectations and this is rather convenient to do with (==) operator.

    I'm not going to write full list of cases where you might need (==). Equality operator is not enough for proving but you don't always need proofs.