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.
