If you have known setoid in Agda, the decidable setoid may be quite easy to understand. We first explain (I hope so …) what is decidable relation. A decidable relation is defined as follows in Agda,

`data Dec (P : Set) : Set where`

`yes : ( p : P) → Dec P`

no : (¬p : ¬ P) → Dec P

It defines a type which has two element: yes if the given proposition is not empty(which means we could give the proof term!) , and no otherwise. Next, a function which translates a relation to a decidable one,

`Decidable : {a : Set} → Rel a → Set`

Decidable _∼_ = ∀ x y → Dec (x ∼ y)

By combining these two, we could define a decidable judgement of relations. Consider the example given in `Data.Nat`

as follows,

`_≤?_ : Decidable _≤_`

zero ≤? _ = yes z≤n

suc m ≤? zero = no λ()

suc m ≤? suc n with m ≤? n

... | yes m≤n = yes (s≤s m≤n)

... | no m≰n = no (m≰n ∘ ≤-pred)

We define a relation `_≤_`

, and a function decide whether two element are related to each other. Moreover, the function returns the proof together.

Then, the decidable setoid is just a setoid with a decidable equality. That is,

`record IsDecEquivalence {a : Set} (_≈_ : Rel a) : Set where`

`field`

`isEquivalence : IsEquivalence _≈_`

_≟_ : Decidable _≈_

`record DecSetoid : Set1 where`

`field`

`carrier : Set`

_≈_ : Rel carrier

isDecEquivalence : IsDecEquivalence _≈_

There is no magic. Back to the earlier example `ListLen`

, we could define a judgement about that relation. But we first modify the relation without using any other datatype.

`data _∼_ {a : Set} : (List a) → (List a) → Set where`

`[]-eq : [] ∼ []`

∷-eq : ∀ {xs ys x y} → (xs∼ys : xs ∼ ys) → (x ∷ xs) ∼ (y ∷ ys)

The corresponding function is defined as follows,

`_∼?_ : ∀ {a} → Decidable (_∼_ {a})`

_∼?_ [] [] = yes []-eq

_∼?_ [] (y ∷ ys) = no (λ ())

_∼?_ (x ∷ xs) [] = no (λ ())

_∼?_ (x ∷ xs) (y ∷ ys) with xs ∼? ys

... | yes eq = yes (∷-eq eq)

... | no neq = no (neq ∘ ∼-pre)

`where`

`∼-pre : ∀ {a} → {x y : a}{xs ys : List a} → (x ∷ xs) ∼ (y ∷ ys) → xs ∼ ys`

∼-pre (∷-eq xs∼ys) = xs∼ys

It’s almost the same as `Data.Nat._≟_`

. We have the decidable version of `ListLen`

immediately.

`decListLen : (a : Set) → DecSetoid`

decListLen a = record

`{ carrier = Setoid.carrier (ListLen a)`

; _≈_ = _∼_

; isDecEquivalence = record

`{ isEquivalence = Setoid.isEquivalence (ListLen a)`

; _≟_ = _∼?_

}}