# Decidable Equality

### Decidability

In mathematics there are undecidable problems, problems for which it is proved to be impossible to construct an algorithm that always leads to a correct yes-or-no answer, for more about this lookup 'halting problem' and Gödel's incompleteness theorem.

This is reflected in our use of types, rather than Boolean values, to represent propositions. That is, we may not know at runtime whether a constructor for a given type exists.

However the propositions we work with tend to be decidable. A property is decidable if you can always say whether the property holds for some specific values and in these case we need a way to test if a proposition is true, that is, we want to know (at runtime) whether a given type be constructed?

In these cases we use the type 'Dec' (for decidability) which is defined in: Idris-dev/libs/prelude/Prelude/Basics.idr. This is like 'Boolean' in that it only has two possible values ('Yes' and 'No' instead of 'True' and 'False') and, in addition, it also has a proof of why it is true or not.

Using Dec you can compute at runtime whether a property is guaranteed to hold or guaranteed not to hold. It is defined in Prelude.Basics like this:

```||| Decidability. A decidable property either holds or is a contradiction.
data Dec : Type -> Type where```
``` ||| The case where the property holds
||| @ prf the proof
Yes : (prf : prop) -> Dec prop```
``` ||| The case where the property holding would be a contradiction
||| @ contra a demonstration that prop would be a contradiction
No : (contra : prop -> Void) -> Dec prop```

Examples

```Idris> Dec (1=1)
Dec (1 = 1) : Type```
```Idris> Dec (1=2)
Dec (1 = 2) : Type```
```Idris> Yes (1=1)
Yes (1 = 1) : Dec Type```
```Idris> Yes (1=2)
Yes (1 = 2) : Dec Type```
```Idris> No (1=1)
(input):1:1-8:When checking argument contra to constructor Prelude.Basics.No:
Type mismatch between
Type (Type of x = y)
and
prop -> Void (Expected type)

Idris> No (1=2)
(input):1:1-8:When checking argument contra to constructor Prelude.Basics.No:
Type mismatch between
Type (Type of x = y)
and
prop -> Void (Expected type)```

### Exists Quantifier

This equality: (S n) = 2 is only true for n=1. This can be written:

(n : Nat) -> Dec (n = 1) -> Dec (S n = 2)

### Decidable Equality

 DecEq is defined in: Idris-dev/libs/prelude/Decidable/Equality.idr definition: ```||| Decision procedures for propositional equality interface DecEq t where ||| Decide whether two elements of `t` ||| are propositionally equal total decEq : (x1 : t) -> (x2 : t) -> Dec (x1 = x2)```

this is implemented for various types, for example Bool:

```implementation DecEq Bool where
decEq True  True  = Yes Refl
decEq False False = Yes Refl
decEq True  False = No trueNotFalse
decEq False True  = No (negEqSym trueNotFalse)   ```

Examples

```Idris> decEq 1 1
Yes Refl : Dec (1 = 1)

Idris> decEq 1 2
No (Decidable.Equality.Decidable.Equality.Integer implementation of
Decidable.Equality.DecEq, method decEq, primitiveNotEq 1
2) : Dec (1 =
2)

Idris> :let a=1
Idris> :let b=2
Idris> decEq a b
No (Decidable.Equality.Decidable.Equality.Integer implementation of
Decidable.Equality.DecEq, method decEq, primitiveNotEq 1
2) : Dec (1 =
2)
Idris> decEq (length [1,2]) (length [3,4])
Yes Refl : Dec (2 = 2)

Idris> (1=1)
1 = 1 : Type

Idris> decEq Int Int
Can't find implementation for DecEq Type

Idris> decEq x x
When checking argument x1 to function Decidable.Equality.decEq:
No such variable x```

### Equality of Types

How do we determine whether two types are the same at compile time? This is difficult if the types are dependant on values. This is important since many functions must operate on terms of the same type (example vector addition), even if we just want to compare values, we must know if they are of the same type.

The value of terms my be indeterminable until runtime. Where we can determine equal types from static code we need something which has the form of a proof.

Where I can, I have put links to Amazon for books that are relevant to the subject, click on the appropriate country flag to get more details of the book or to buy it from them.

 Type-Driven Development with Idris

Commercial Software Shop

Where I can, I have put links to Amazon for commercial software, not directly related to the software project, but related to the subject being discussed, click on the appropriate country flag to get more details of the software or to buy it from them.

This site may have errors. Don't use for critical systems.