Add Decidable typeclass.

Author: omelkonian

Class/Applicative/Core.agda

@@ -4,15 +4,6 @@ open import Class.Prelude
 open import Class.Core
 open import Class.Functor.Core
 
-{-
-Applicative : (Type ℓ → Type ℓ) → Type (lsuc ℓ)
-Applicative {ℓ = ℓ} = RawApplicative {f = ℓ}
-open RawApplicative ⦃...⦄ public
-  using (pure)
-  renaming ( _⊛_ to _<*>_; _<⊛_ to _<*_ ; _⊛>_ to _*>_)
--}
-
--- record Applicative (F : Type ℓ → Type ℓ′) : Type (lsuc ℓ ⊔ₗ ℓ′) where
 record Applicative (F : Type↑) : Typeω where
   infixl 4 _<*>_ _⊛_ _<*_ _<⊛_ _*>_ _⊛>_
   infix  4 _⊗_
@@ -51,8 +42,7 @@ open Applicative₀ ⦃...⦄ public
 record Alternative (F : Type↑) : Typeω where
   infixr 3 _<|>_
   field _<|>_ : F A → F A → F A
-    -- overlap ⦃ ap₀ ⦄ : Applicative₀ F
-open Alternative ⦃...⦄ {- hiding (ap₀) -} public
+open Alternative ⦃...⦄ public
 
 infix -1 ⋃⁺_ ⋃_
 

Class/DecEq.agda

@@ -2,3 +2,4 @@ module Class.DecEq where
 
 open import Class.DecEq.Core public
 open import Class.DecEq.Instances public
+-- open import Class.DecEq.WithK public

Class/DecEq/Derive.agda

@@ -1,18 +1,10 @@
-{-# OPTIONS --safe #-}
+{-# OPTIONS --with-K #-}
 module Class.DecEq.WithK where
 
-open import Agda.Primitive using () renaming (Set to Type)
-open import Level using (Level)
-open import Data.Product
-open import Relation.Nullary
-open import Relation.Nullary.Decidable
-open import Relation.Binary.PropositionalEquality
-
+open import Class.Prelude
 open import Class.DecEq.Core
 
-private variable ℓ ℓ′ : Level
-
-module _ {A : Type ℓ} ⦃ _ : DecEq A ⦄ where
+module _ ⦃ _ : DecEq A ⦄ where
   ≟-refl : ∀ (x : A) → (x ≟ x) ≡ yes refl
   ≟-refl x with refl , p ← dec-yes (x ≟ x) refl = p
 

Class/DecEq/WithK.agda

@@ -0,0 +1,4 @@
+module Class.Decidable where
+
+open import Class.Decidable.Core public
+open import Class.Decidable.Instances public

Class/Decidable.agda

@@ -0,0 +1,57 @@
+module Class.Decidable.Core where
+
+open import Class.Prelude
+
+open import Relation.Nullary.Decidable using (True; False; toWitness; toWitnessFalse)
+
+record _⁇ (P : Type ℓ) : Type ℓ where
+  constructor ⁇_
+  field dec : Dec P
+
+  auto : ⦃ True dec ⦄ → P
+  auto ⦃ pr ⦄ = toWitness pr
+
+  contradict : ∀ {X : Type} {pr : False dec} → P → X
+  contradict {pr = pr} = ⊥-elim ∘ toWitnessFalse pr
+
+open _⁇ ⦃ ... ⦄ public
+
+¿_¿ : ∀ (X : Type ℓ) → ⦃ X ⁇ ⦄ → Dec X
+¿ _ ¿ = dec
+
+module _ {A : Type ℓ} where
+
+  _⁇¹ : Pred A ℓ′ → Type (ℓ ⊔ ℓ′)
+  P ⁇¹ = ∀ {x} → P x ⁇
+
+  dec¹ : {P : Pred A ℓ′} → ⦃ P ⁇¹ ⦄ → Decidable¹ P
+  dec¹ _ = dec
+
+  ¿_¿¹ : (P : Pred A ℓ′) → ⦃ P ⁇¹ ⦄ → Decidable¹ P
+  ¿ _ ¿¹ = dec¹
+
+module _ {A B : Type ℓ} where
+
+  _⁇² : REL A B ℓ′ → Type (ℓ ⊔ ℓ′)
+  _~_ ⁇² = ∀ {x y} → (x ~ y) ⁇
+
+  dec² : {_~_ : REL A B ℓ′} → ⦃ _~_ ⁇² ⦄ → Decidable² _~_
+  dec² _ _ = dec
+
+  ¿_¿² : (_~_ : REL A B ℓ′) → ⦃ _~_ ⁇² ⦄ → Decidable² _~_
+  ¿ _ ¿² = dec²
+
+module _ {A B C : Type ℓ} where
+
+  _⁇³ : (P : 3REL A B C ℓ′) → Type (ℓ ⊔ ℓ′)
+  _~_~_ ⁇³ = ∀ {x y z} → (x ~ y ~ z) ⁇
+
+  dec³ : {_~_~_ : 3REL A B C ℓ′} → ⦃ _~_~_ ⁇³ ⦄ → Decidable³ _~_~_
+  dec³ _ _ _ = dec
+
+  ¿_¿³ : (_~_~_ : 3REL A B C ℓ′) → ⦃ _~_~_ ⁇³ ⦄ → Decidable³ _~_~_
+  ¿ _ ¿³ = dec³
+
+infix -100 auto∶_
+auto∶_ : ∀ (X : Type ℓ) → ⦃ X ⁇ ⦄ → Type
+auto∶_ A = True ¿ A ¿

Class/Decidable/Core.agda

@@ -0,0 +1,81 @@
+module Class.Decidable.Instances where
+
+open import Class.Prelude
+open import Class.Decidable.Core
+open import Class.DecEq.Core
+
+instance
+  Dec-⊥ : ⊥ ⁇
+  Dec-⊥ .dec = no λ()
+
+  Dec-⊤ : ⊤ ⁇
+  Dec-⊤ .dec = yes tt
+
+  Dec-→ : ⦃ A ⁇ ⦄ → ⦃ B ⁇ ⦄ → (A → B) ⁇
+  Dec-→ .dec = dec →-dec dec
+    where open import Relation.Nullary.Implication using (_→-dec_)
+
+  Dec-× : ⦃ A ⁇ ⦄ → ⦃ B ⁇ ⦄ → (A × B) ⁇
+  Dec-× .dec = dec ×-dec dec
+    where open import Relation.Nullary.Product using (_×-dec_)
+
+  Dec-⊎ : ⦃ A ⁇ ⦄ → ⦃ B ⁇ ⦄ → (A ⊎ B) ⁇
+  Dec-⊎ .dec = dec ⊎-dec dec
+    where open import Relation.Nullary.Sum using (_⊎-dec_)
+
+  DecEq⇒Dec : ⦃ DecEq A ⦄ → _≡_ {A = A} ⁇²
+  DecEq⇒Dec .dec = _ ≟ _
+
+  import Data.Bool as 𝔹
+
+  Dec-T : ∀ {t} → T t ⁇
+  Dec-T .dec = 𝔹.T? _
+
+  import Data.List.Relation.Unary.All as L
+  import Data.List.Relation.Unary.Any as L
+
+  private variable n : ℕ; P¹ : Pred A ℓ; P² : Rel A ℓ
+
+  Dec-All : ⦃ P¹ ⁇¹ ⦄ → L.All P¹ ⁇¹
+  Dec-All .dec = L.all? dec¹ _
+
+  Dec-Any : ⦃ P¹ ⁇¹ ⦄ → L.Any P¹ ⁇¹
+  Dec-Any .dec = L.any? dec¹ _
+
+  import Data.List.Relation.Unary.AllPairs as AP
+
+  Dec-AllPairs : ⦃ P² ⁇² ⦄ → AP.AllPairs P² ⁇¹
+  Dec-AllPairs .dec = AP.allPairs? dec² _
+
+  open import Data.Vec as V
+  open import Data.Vec.Relation.Unary.All as V
+  open import Data.Vec.Relation.Unary.Any as V
+
+  Dec-VAll : ⦃ P¹ ⁇¹ ⦄ → V.All P¹ {n} ⁇¹
+  Dec-VAll .dec = V.all? dec¹ _
+
+  Dec-VAny : ⦃ P¹ ⁇¹ ⦄ → V.Any P¹ {n} ⁇¹
+  Dec-VAny .dec = V.any? dec¹ _
+
+  import Data.Maybe as M
+  import Data.Maybe.Relation.Unary.All as M renaming (dec to all?)
+  import Data.Maybe.Relation.Unary.Any as M renaming (dec to any?)
+
+  Dec-MAll : ⦃ _ : P¹ ⁇¹ ⦄ → M.All P¹ ⁇¹
+  Dec-MAll .dec = M.all? dec¹ _
+
+  Dec-MAny : ⦃ _ : P¹ ⁇¹ ⦄ → M.Any P¹ ⁇¹
+  Dec-MAny .dec = M.any? dec¹ _
+
+private
+  open import Data.List.Membership.Propositional using (_∈_; _∉_)
+  open import Class.DecEq.Instances
+
+  0⋯2 = List ℕ ∋ 0 ∷ 1 ∷ 2 ∷ []
+
+  _ = 1 ∈ 0⋯2
+    ∋ auto
+  _ = 3 ∉ 0⋯2
+    ∋ auto
+  f = (3 ∈ 0⋯2 → 2 ≡ 3)
+    ∋ contradict

Class/Decidable/Instances.agda

@@ -5,12 +5,6 @@ open import Class.Core
 
 private variable a b c : Level
 
-{-
-Functor : (Type ℓ → Type ℓ) → Type (lsuc ℓ)
-Functor {ℓ = ℓ} = RawFunctor {ℓ = ℓ} {ℓ′ = ℓ}
-open RawFunctor ⦃...⦄ public
--}
-
 record Functor (F : Type↑) : Typeω where
   infixl 4 _<$>_ _<$_
   infixl 1 _<&>_

Class/Functor/Core.agda

@@ -1,10 +1,11 @@
 module Class.Monad.Core where
 
 open import Class.Prelude
+open import Class.Core
 open import Class.Functor
 open import Class.Applicative
 
-record Monad (M : ∀ {a} → Type a → Type a) : Typeω where
+record Monad (M : Type↑) : Typeω where
   infixl 1 _>>=_ _>>_ _>=>_
   infixr 1 _=<<_ _<=<_
 

Class/Functor/Derive.agda

@@ -7,14 +7,16 @@ open import Level public
 open import Function public
   using (id; _∘_; _∋_; _$_; const; constᵣ; flip)
 
+open import Data.Empty public
+  using (⊥; ⊥-elim)
 open import Data.Unit public
   using (⊤; tt)
 open import Data.Product public
   using (_×_; _,_; proj₁; proj₂; Σ; ∃; -,_)
 open import Data.Sum public
   using (_⊎_; inj₁; inj₂)
 open import Data.Bool public
-  using (Bool; true; false; not; if_then_else_)
+  using (Bool; true; false; not; if_then_else_; T)
 open import Data.Nat public
   using (ℕ; zero; suc)
 open import Data.Fin as Fin public
@@ -39,12 +41,21 @@ open import Data.These public
   using (These; this; that; these)
 
 open import Relation.Nullary public
-  using (yes; no)
+  using (Dec; yes; no)
 open import Relation.Nullary.Decidable public
   using (⌊_⌋; dec-yes)
+open import Relation.Unary public
+  using (Pred)
+  renaming (Decidable to Decidable¹)
 open import Relation.Binary public
-  using (Rel; DecidableEquality)
+  using (REL; Rel; DecidableEquality)
   renaming (Decidable to Decidable²)
+module _ {a b c} where
+  3REL : (A : Set a) (B : Set b) (C : Set c) (ℓ : Level) → Type _
+  3REL A B C ℓ = A → B → C → Type ℓ
+
+  Decidable³ : ∀ {A B C ℓ} → 3REL A B C ℓ → Type _
+  Decidable³ _~_~_ = ∀ x y z → Dec (x ~ y ~ z)
 open import Relation.Binary.PropositionalEquality public
   using (_≡_; refl; sym; cong)
 

Class/Monad/Core.agda

@@ -1,5 +1,6 @@
 module Classes where
 
+-- ** Algebraic structures
 open import Class.Semigroup public
 open import Class.Monoid public
 open import Class.Functor public
@@ -8,7 +9,10 @@ open import Class.Applicative public
 open import Class.Monad public
 open import Class.Traversable public
 
-open import Class.Show public
+-- ** Decidability
 open import Class.DecEq public
+open import Class.Decidable public
 
+-- ** Others
+open import Class.Show public
 open import Class.Default public