module Data.Dec.Base where

Decidable typesπŸ”—

The type Dec, of decisions for a type A, is a renaming of the coproduct A + Β¬ A. A value of Dec A witnesses not that A is decidable, but that it has been decided; A witness of decidability, then, is a proof assigning decisions to values of a certain type.

data Dec {β„“} (A : Type β„“) : Type β„“ where
  yes : (a  :   A) β†’ Dec A
  no  : (Β¬a : Β¬ A) β†’ Dec A

Dec-elim
  : βˆ€ {β„“ β„“'} {A : Type β„“} (P : Dec A β†’ Type β„“')
  β†’ (βˆ€ y β†’ P (yes y))
  β†’ (βˆ€ y β†’ P (no y))
  β†’ βˆ€ x β†’ P x
Dec-elim P f g (yes x) = f x
Dec-elim P f g (no x)  = g x

Dec-rec
  : βˆ€ {β„“ β„“'} {A : Type β„“} {X : Type β„“'}
  β†’ (A β†’ X)
  β†’ (Β¬ A β†’ X)
  β†’ Dec A β†’ X
Dec-rec = Dec-elim _

A type is discrete if it has decidable equality.

Discrete : βˆ€ {β„“} β†’ Type β„“ β†’ Type β„“
Discrete A = {x y : A} β†’ Dec (x ≑ y)

If we can construct a pair of maps A→BA \to B and B→AB \to A, then we can deduce decidability of BB from decidability of AA.

Dec-map
  : (A β†’ B) β†’ (B β†’ A)
  β†’ Dec A β†’ Dec B
Dec-map to from (yes a) = yes (to a)
Dec-map to from (no ¬a) = no (¬a ∘ from)

Dec-≃ : A ≃ B β†’ Dec A β†’ Dec B
Dec-≃ e = Dec-map (Equiv.to e) (Equiv.from e)

This lets us show the following useful lemma: if AA injects into a discrete type, then AA is also discrete.

Discrete-inj
  : (f : A β†’ B)
  β†’ (βˆ€ {x y} β†’ f x ≑ f y β†’ x ≑ y)
  β†’ Discrete B β†’ Discrete A
Discrete-inj f inj eq? {x} {y} =
  Dec-map inj (ap f) (eq? {f x} {f y})

Programming with decisionsπŸ”—

Despite the failure of Dec A to be a proposition for general A, in the 1Lab, we like to work with decisions through instance search. This is facilitated by the following functions, which perform instance search:

-- Searches for a type given explicitly.
holds? : βˆ€ {β„“} (A : Type β„“) ⦃ d : Dec A ⦄ β†’ Dec A
holds? A ⦃ d ⦄ = d

-- Searches for equality of inhabitants of a discrete type.
_≑?_ : ⦃ d : Discrete A ⦄ (x y : A) β†’ Dec (x ≑ y)
x ≑? y = holds? (x ≑ y)

infix 3 _≑?_

And the following operators, which combine instance search with case analysis:

caseᡈ_of_ : βˆ€ {β„“ β„“'} (A : Type β„“) ⦃ d : Dec A ⦄ {B : Type β„“'} β†’ (Dec A β†’ B) β†’ B
caseᡈ A of f = f (holds? A)

caseᡈ_return_of_ : βˆ€ {β„“ β„“'} (A : Type β„“) ⦃ d : Dec A ⦄ (B : Dec A β†’ Type β„“') β†’ (βˆ€ x β†’ B x) β†’ B d
caseᡈ A return P of f = f (holds? A)

{-# INLINE caseᡈ_of_        #-}
{-# INLINE caseᡈ_return_of_ #-}

We then have the following basic instances for combining decisions, expressing that the class of decidable types is closed under products and negation, and contains the empty type.

instance
  Dec-Γ— : ⦃ _ : Dec P ⦄ ⦃ _ : Dec Q ⦄ β†’ Dec (P Γ— Q)
  Dec-Γ— {Q = _} ⦃ yes p ⦄ ⦃ yes q ⦄ = yes (p , q)
  Dec-Γ— {Q = _} ⦃ yes p ⦄ ⦃ no Β¬q ⦄ = no Ξ» z β†’ Β¬q (snd z)
  Dec-Γ— {Q = _} ⦃ no Β¬p ⦄ ⦃ _ ⦄     = no Ξ» z β†’ Β¬p (fst z)

  Dec-⊀ : Dec ⊀
  Dec-⊀ = yes tt

  Dec-βŠ₯ : Dec βŠ₯
  Dec-βŠ₯ = no id

  Dec-Β¬ : ⦃ _ : Dec A ⦄ β†’ Dec (A β†’ βŠ₯)
  Dec-Β¬ {A = _} ⦃ yes a ⦄ = no Ξ» Β¬a β†’ Β¬a a
  Dec-Β¬ {A = _} ⦃ no Β¬a ⦄ = yes Β¬a