Remove Reflects type from Haskell.Law.Equality in favor of the one in…

… Haskell.Extra.Dec
agda · Dec 20, 2023 · aa0ae8d · aa0ae8d
1 parent 6bf9767
commit aa0ae8d
Show file tree

Hide file tree

Showing 7 changed files with 54 additions and 51 deletions.
diff --git a/lib/Haskell/Extra/Dec.agda b/lib/Haskell/Extra/Dec.agda
@@ -4,10 +4,32 @@ open import Haskell.Prelude
 open import Haskell.Extra.Refinement
 open import Agda.Primitive
 
-@0 Reflects : ∀ {ℓ} → Set ℓ → Bool → Set ℓ
+private variable
+  ℓ : Level
+  P : Set
+
+@0 Reflects : Set ℓ → Bool → Set ℓ
 Reflects P True  = P
 Reflects P False = P → ⊥
 
+of : {b : Bool} → if b then P else (P → ⊥) → Reflects P b
+of {b = False} np = np
+of {b = True}  p  = p
+
+invert : ∀ {b} → Reflects P b → if b then P else (P → ⊥)
+invert {b = False} np = np
+invert {b = True}  p  = p
+
+extractTrue : ∀ { b } → ⦃ true : b ≡ True ⦄ → Reflects P b → P
+extractTrue {b = True} p = p
+
+extractFalse : ∀ { b } → ⦃ true : b ≡ False ⦄ → Reflects P b → (P → ⊥)
+extractFalse {b = False} np = np
+
+mapReflects : ∀ {cond} → (a → b) → (b → a)
+            → Reflects a cond → Reflects b cond
+mapReflects {cond = False} f g x = x ∘ g
+mapReflects {cond = True}  f g x = f x
 
 Dec : ∀ {ℓ} → @0 Set ℓ → Set ℓ
 Dec P = ∃ Bool (Reflects P)

diff --git a/lib/Haskell/Law.agda b/lib/Haskell/Law.agda
@@ -3,3 +3,13 @@ module Haskell.Law where
 open import Haskell.Prim
 open import Haskell.Prim.Bool
 
+open import Haskell.Law.Applicative  public
+open import Haskell.Law.Bool         public
+open import Haskell.Law.Eq           public
+open import Haskell.Law.Equality     public
+open import Haskell.Law.Functor      public
+open import Haskell.Law.List         public
+open import Haskell.Law.Maybe        public
+open import Haskell.Law.Monad        public
+open import Haskell.Law.Monoid       public
+open import Haskell.Law.Ord          public
diff --git a/lib/Haskell/Law/Eq/Bool.agda b/lib/Haskell/Law/Eq/Bool.agda
@@ -8,8 +8,8 @@ open import Haskell.Law.Equality
 
 instance
   iLawfulEqBool : IsLawfulEq Bool
-  iLawfulEqBool .isEquality False False = ofY refl
-  iLawfulEqBool .isEquality False True = ofN λ()
-  iLawfulEqBool .isEquality True False = ofN λ()
-  iLawfulEqBool .isEquality True True = ofY refl
+  iLawfulEqBool .isEquality False False = refl
+  iLawfulEqBool .isEquality False True = λ()
+  iLawfulEqBool .isEquality True False = λ()
+  iLawfulEqBool .isEquality True True = refl
 
diff --git a/lib/Haskell/Law/Eq/Def.agda b/lib/Haskell/Law/Eq/Def.agda
@@ -12,6 +12,8 @@ open import Haskell.Prim.Either
 
 open import Haskell.Prim.Eq
 
+open import Haskell.Extra.Dec
+
 open import Haskell.Law.Bool
 open import Haskell.Law.Equality
 

diff --git a/lib/Haskell/Law/Eq/Maybe.agda b/lib/Haskell/Law/Eq/Maybe.agda
@@ -4,21 +4,16 @@ open import Haskell.Prim
 open import Haskell.Prim.Eq
 open import Haskell.Prim.Maybe
 
+open import Haskell.Extra.Dec
+
 open import Haskell.Law.Eq.Def
 open import Haskell.Law.Equality
 open import Haskell.Law.Maybe
 
-private
-  reflectsJust : ⦃ iEqA : Eq a ⦄ → ⦃ IsLawfulEq a ⦄
-    → ∀ (x y : a) → Reflects (Just x ≡ Just y) ((Just x) == (Just y))
-  reflectsJust x y with (x == y) in h
-  ... | True  = ofY (cong Just (equality x y h))
-  ... | False = ofN (λ eq → (nequality x y h) (injective eq))
-
 instance
   iLawfulEqMaybe : ⦃ iEqA : Eq a ⦄ → ⦃ IsLawfulEq a ⦄ → IsLawfulEq (Maybe a)
-  iLawfulEqMaybe .isEquality Nothing Nothing = ofY refl
-  iLawfulEqMaybe .isEquality Nothing (Just _) = ofN λ()
-  iLawfulEqMaybe .isEquality (Just _) Nothing = ofN λ()
-  iLawfulEqMaybe .isEquality (Just x) (Just y) = reflectsJust x y
+  iLawfulEqMaybe .isEquality Nothing Nothing = refl
+  iLawfulEqMaybe .isEquality Nothing (Just _) = λ()
+  iLawfulEqMaybe .isEquality (Just _) Nothing = λ()
+  iLawfulEqMaybe .isEquality (Just x) (Just y) = mapReflects (cong Just) injective (isEquality x y)
 
diff --git a/lib/Haskell/Law/Eq/Ordering.agda b/lib/Haskell/Law/Eq/Ordering.agda
@@ -10,13 +10,13 @@ open import Haskell.Law.Equality
 instance
   iLawfulEqOrdering : IsLawfulEq Ordering
 
-  iLawfulEqOrdering .isEquality LT LT = ofY refl
-  iLawfulEqOrdering .isEquality LT EQ = ofN λ()
-  iLawfulEqOrdering .isEquality LT GT = ofN λ()
-  iLawfulEqOrdering .isEquality EQ LT = ofN λ()
-  iLawfulEqOrdering .isEquality EQ EQ = ofY refl
-  iLawfulEqOrdering .isEquality EQ GT = ofN λ()
-  iLawfulEqOrdering .isEquality GT LT = ofN λ()
-  iLawfulEqOrdering .isEquality GT EQ = ofN λ()
-  iLawfulEqOrdering .isEquality GT GT = ofY refl
+  iLawfulEqOrdering .isEquality LT LT = refl
+  iLawfulEqOrdering .isEquality LT EQ = λ()
+  iLawfulEqOrdering .isEquality LT GT = λ()
+  iLawfulEqOrdering .isEquality EQ LT = λ()
+  iLawfulEqOrdering .isEquality EQ EQ = refl
+  iLawfulEqOrdering .isEquality EQ GT = λ()
+  iLawfulEqOrdering .isEquality GT LT = λ()
+  iLawfulEqOrdering .isEquality GT EQ = λ()
+  iLawfulEqOrdering .isEquality GT GT = refl
 
diff --git a/lib/Haskell/Law/Equality.agda b/lib/Haskell/Law/Equality.agda
@@ -54,29 +54,3 @@ _∎ _ = refl
 
 syntax step-≡  x y≡z x≡y = x ≡⟨  x≡y ⟩ y≡z
 syntax step-≡˘ x y≡z y≡x = x ≡˘⟨ y≡x ⟩ y≡z
-
---------------------------------------------------
--- Reflects idiom
-
-data Reflects {p} (P : Set p) : Bool → Set p where
-  ofY : ( p :   P )      → Reflects P True
-  ofN : ( np : (P → ⊥) ) → Reflects P False
-
-private
-  variable
-    p : Level
-    P : Set p
-
-of : ∀ {b} → if b then P else (P → ⊥) → Reflects P b
-of {b = False} np = ofN np
-of {b = True }  p = ofY p
-
-invert : ∀ {b} → Reflects P b → if b then P else (P → ⊥)
-invert (ofY  p) = p
-invert (ofN np) = np
-
-extractTrue : ∀ { b } → ⦃ true : b ≡ True ⦄ → Reflects P b → P
-extractTrue (ofY p) = p
-
-extractFalse : ∀ { b } → ⦃ true : b ≡ False ⦄ → Reflects P b → (P → ⊥)
-extractFalse (ofN np) = np