Skip to content

Commit 1b9286b

Browse files
odderwiserodderwiser
committed
Injective abstraction layer
1 parent b7e4c3d commit 1b9286b

File tree

8 files changed

+43
-28
lines changed

8 files changed

+43
-28
lines changed

‎lib/Haskell/Law.agda

+1
Original file line numberDiff line numberDiff line change
@@ -3,6 +3,7 @@ module Haskell.Law where
33
open import Haskell.Prim
44
open import Haskell.Prim.Bool
55

6+
open import Haskell.Law.Def public
67
open import Haskell.Law.Applicative public
78
open import Haskell.Law.Bool public
89
open import Haskell.Law.Either public

‎lib/Haskell/Law/Def.agda

+6
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,6 @@
1+
module Haskell.Law.Def where
2+
3+
open import Haskell.Prim
4+
5+
Injective : (a → b) → Set _
6+
Injective f = ∀ {x y} → f x ≡ f y → x ≡ y

‎lib/Haskell/Law/Either.agda

+7-9
Original file line numberDiff line numberDiff line change
@@ -3,12 +3,10 @@ module Haskell.Law.Either where
33
open import Haskell.Prim
44
open import Haskell.Prim.Either
55

6-
Left-injective : ∀ {a b : Set} {z w : a}
7-
→ (x y : Either a b) → ⦃ x ≡ Left z ⦄ → ⦃ y ≡ Left w ⦄ -> x ≡ y
8-
→ z ≡ w
9-
Left-injective (Left x) (Left y) ⦃ refl ⦄ ⦃ refl ⦄ refl = refl
10-
11-
Right-injective : ∀ {a b : Set} {z w : b}
12-
→ (x y : Either a b) → ⦃ x ≡ Right z ⦄ → ⦃ y ≡ Right w ⦄ -> x ≡ y
13-
→ z ≡ w
14-
Right-injective (Right x) (Right y) ⦃ refl ⦄ ⦃ refl ⦄ refl = refl
6+
open import Haskell.Law.Def
7+
8+
Left-injective : Injective (Left {a}{b})
9+
Left-injective refl = refl
10+
11+
Right-injective : Injective (Right {a}{b})
12+
Right-injective refl = refl

‎lib/Haskell/Law/Eq/Instances.agda

+14-12
Original file line numberDiff line numberDiff line change
@@ -60,12 +60,12 @@ instance
6060
iLawfulEqEither : ⦃ iEqA : Eq a ⦄ → ⦃ iEqB : Eq b ⦄
6161
→ ⦃ IsLawfulEq a ⦄ → ⦃ IsLawfulEq b ⦄
6262
→ IsLawfulEq (Either a b)
63-
iLawfulEqEither .isEquality (Left _) (Right _) = λ ()
64-
iLawfulEqEither .isEquality (Right _) (Left _) = λ ()
65-
iLawfulEqEither .isEquality a@(Left x) b@(Left y) = mapReflects
66-
(cong Left) (Left-injective a b) (isEquality x y)
67-
iLawfulEqEither .isEquality a@(Right x) b@(Right y) = mapReflects
68-
(cong Right) (Right-injective a b) (isEquality x y)
63+
iLawfulEqEither .isEquality (Left _) (Right _) = λ ()
64+
iLawfulEqEither .isEquality (Right _) (Left _) = λ ()
65+
iLawfulEqEither .isEquality (Left x) (Left y) = mapReflects
66+
(cong Left) (Left-injective) (isEquality x y)
67+
iLawfulEqEither .isEquality (Right x) (Right y) = mapReflects
68+
(cong Right) (Right-injective) (isEquality x y)
6969

7070
iLawfulEqInt : IsLawfulEq Int
7171
iLawfulEqInt .isEquality (int64 x) (int64 y) = mapReflects
@@ -92,11 +92,11 @@ instance
9292
... | False = λ h → (nequality x y h₁) (∷-injective-left h)
9393

9494
iLawfulEqMaybe : ⦃ iEqA : Eq a ⦄ → ⦃ IsLawfulEq a ⦄ → IsLawfulEq (Maybe a)
95-
iLawfulEqMaybe .isEquality Nothing Nothing = refl
96-
iLawfulEqMaybe .isEquality Nothing (Just _) = λ()
97-
iLawfulEqMaybe .isEquality (Just _) Nothing = λ()
95+
iLawfulEqMaybe .isEquality Nothing Nothing = refl
96+
iLawfulEqMaybe .isEquality Nothing (Just _) = λ()
97+
iLawfulEqMaybe .isEquality (Just _) Nothing = λ()
9898
iLawfulEqMaybe .isEquality (Just x) (Just y) = mapReflects
99-
(cong Just) injective (isEquality x y)
99+
(cong Just) (injective-Just {x = x} {y = y}) (isEquality x y)
100100

101101
iLawfulEqOrdering : IsLawfulEq Ordering
102102
iLawfulEqOrdering .isEquality LT LT = refl
@@ -112,7 +112,8 @@ instance
112112
iLawfulEqTuple₂ : ⦃ iEqA : Eq a ⦄ ⦃ iEqB : Eq b ⦄
113113
→ ⦃ IsLawfulEq a ⦄ → ⦃ IsLawfulEq b ⦄
114114
→ IsLawfulEq (a × b)
115-
iLawfulEqTuple₂ .isEquality (x₁ , x₂) (y₁ , y₂) with (x₁ == y₁) in h₁
115+
iLawfulEqTuple₂ .isEquality (x₁ , x₂) (y₁ , y₂)
116+
with (x₁ == y₁) in h₁
116117
... | True = mapReflects
117118
(λ h → cong₂ _,_ (equality x₁ y₁ h₁) h)
118119
(cong snd)
@@ -122,7 +123,8 @@ instance
122123
iLawfulEqTuple₃ : ⦃ iEqA : Eq a ⦄ ⦃ iEqB : Eq b ⦄ ⦃ iEqC : Eq c ⦄
123124
→ ⦃ IsLawfulEq a ⦄ → ⦃ IsLawfulEq b ⦄ → ⦃ IsLawfulEq c ⦄
124125
→ IsLawfulEq (a × b × c)
125-
iLawfulEqTuple₃ .isEquality (x₁ , x₂ , x₃) (y₁ , y₂ , y₃) with (x₁ == y₁) in h₁
126+
iLawfulEqTuple₃ .isEquality (x₁ , x₂ , x₃) (y₁ , y₂ , y₃)
127+
with (x₁ == y₁) in h₁
126128
... | True = mapReflects
127129
(λ h → cong₂ (λ a (b , c) → a , b , c) (equality x₁ y₁ h₁) h)
128130
(cong λ h → snd₃ h , thd₃ h)

‎lib/Haskell/Law/Int.agda

+4-2
Original file line numberDiff line numberDiff line change
@@ -1,7 +1,9 @@
11
module Haskell.Law.Int where
22

33
open import Haskell.Prim
4-
open import Haskell.Prim.Int
4+
open import Haskell.Prim.Int using ( int64 )
55

6-
int64-injective : ∀ {a b : Word64} → (int64 a) ≡ (int64 b) → a ≡ b
6+
open import Haskell.Law.Def
7+
8+
int64-injective : Injective int64
79
int64-injective refl = refl

‎lib/Haskell/Law/Integer.agda

+4-2
Original file line numberDiff line numberDiff line change
@@ -2,8 +2,10 @@ module Haskell.Law.Integer where
22

33
open import Haskell.Prim
44

5-
pos-injective : ∀ { a b : Nat } → pos a ≡ pos b → a ≡ b
5+
open import Haskell.Law.Def
6+
7+
pos-injective : Injective pos
68
pos-injective refl = refl
79

8-
neg-injective : ∀ { a b : Nat } → negsuc a ≡ negsuc b → a ≡ b
10+
neg-injective : Injective negsuc
911
neg-injective refl = refl

‎lib/Haskell/Law/Maybe.agda

+4-2
Original file line numberDiff line numberDiff line change
@@ -3,5 +3,7 @@ module Haskell.Law.Maybe where
33
open import Haskell.Prim
44
open import Haskell.Prim.Maybe
55

6-
injective : ∀ {x y : a} → Just x ≡ Just y → x ≡ y
7-
injective refl = refl
6+
open import Haskell.Law.Def
7+
8+
injective-Just : Injective (Just {a = a})
9+
injective-Just refl = refl

‎lib/Haskell/Law/Nat.agda

+3-1
Original file line numberDiff line numberDiff line change
@@ -2,5 +2,7 @@ module Haskell.Law.Nat where
22

33
open import Haskell.Prim
44

5-
suc-injective : ∀ { a b : Nat } → suc a ≡ suc b → a ≡ b
5+
open import Haskell.Law.Def
6+
7+
suc-injective : Injective suc
68
suc-injective refl = refl

0 commit comments

Comments
 (0)