Skip to content

Commit 158822e

Browse files
omelkonianomelkonian
committed
Convertible/HasHsType: general cleanup
1 parent 480242a commit 158822e

31 files changed

+532
-539
lines changed

‎Class/Convertible.agda‎

Lines changed: 2 additions & 82 deletions
Original file line numberDiff line numberDiff line change
@@ -1,84 +1,4 @@
11
module Class.Convertible where
22

3-
open import Function
4-
open import Class.HasHsType
5-
open import Class.Core
6-
open import Class.Functor
7-
open import Class.Bifunctor
8-
open import Data.Maybe
9-
open import Data.Product
10-
open import Data.Sum
11-
open import Data.List
12-
13-
record Convertible (A B : Set) : Set where
14-
field to : A → B
15-
from : B → A
16-
open Convertible ⦃...⦄ public
17-
18-
HsConvertible : (A : Set) → ⦃ HasHsType A ⦄ → Set
19-
HsConvertible A = Convertible A (HsType A)
20-
21-
Convertible-Refl : ∀ {A} → Convertible A A
22-
Convertible-Refl = λ where .to → id; .from → id
23-
24-
Convertible₁ : (Set → Set) → (Set → Set) → Set₁
25-
Convertible₁ T U = ∀ {A B} → ⦃ Convertible A B ⦄ → Convertible (T A) (U B)
26-
27-
Convertible₂ : (Set → Set → Set) → (Set → Set → Set) → Set₁
28-
Convertible₂ T U = ∀ {A B} → ⦃ Convertible A B ⦄ → Convertible₁ (T A) (U B)
29-
30-
Functor⇒Convertible : ∀ {F : Type↑} → ⦃ Functor F ⦄ → Convertible₁ F F
31-
Functor⇒Convertible = λ where
32-
.to → fmap to
33-
.from → fmap from
34-
35-
Bifunctor⇒Convertible : ∀ {F} → ⦃ Bifunctor F ⦄ → Convertible₂ F F
36-
Bifunctor⇒Convertible = λ where
37-
.to → bimap to to
38-
.from → bimap from from
39-
40-
_⨾_ : ∀ {A B C} → Convertible A B → Convertible B C → Convertible A C
41-
(c ⨾ c') .to = c' .to ∘ c .to
42-
(c ⨾ c') .from = c .from ∘ c' .from
43-
44-
-- ** instances
45-
46-
open import Foreign.Haskell
47-
open import Foreign.Haskell.Coerce using (coerce)
48-
49-
open import Data.Nat
50-
51-
instance
52-
Convertible-ℕ : Convertible ℕ ℕ
53-
Convertible-ℕ = λ where
54-
.to → id
55-
.from → id
56-
57-
Convertible-Maybe : Convertible₁ Maybe Maybe
58-
Convertible-Maybe = Functor⇒Convertible
59-
60-
Convertible-× : Convertible₂ _×_ _×_
61-
Convertible-× = Bifunctor⇒Convertible
62-
63-
Convertible-Pair : Convertible₂ _×_ Pair
64-
Convertible-Pair = λ where
65-
.to → coerce ∘ bimap to to
66-
.from → bimap from from ∘ coerce
67-
68-
Convertible-⊎ : Convertible₂ _⊎_ _⊎_
69-
Convertible-⊎ = Bifunctor⇒Convertible
70-
71-
Convertible-Either : Convertible₂ _⊎_ Either
72-
Convertible-Either = λ where
73-
.to → coerce ∘ bimap to to
74-
.from → bimap from from ∘ coerce
75-
76-
Convertible-List : Convertible₁ List List
77-
Convertible-List = λ where
78-
.to → fmap to
79-
.from → fmap from
80-
81-
Convertible-Fun : ∀ {A A' B B'} → ⦃ Convertible A A' ⦄ → ⦃ Convertible B B' ⦄ → Convertible (A → B) (A' → B')
82-
Convertible-Fun = λ where
83-
.to → λ f → to ∘ f ∘ from
84-
.from → λ f → from ∘ f ∘ to
3+
open import Class.Convertible.Core public
4+
open import Class.Convertible.Instances public

‎Class/Convertible/Core.agda‎

Lines changed: 35 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,35 @@
1+
module Class.Convertible.Core where
2+
3+
open import Meta.Prelude
4+
5+
open import Class.Core
6+
open import Class.Functor
7+
open import Class.Bifunctor
8+
9+
record Convertible (A B : Set) : Set where
10+
field to : A → B
11+
from : B → A
12+
open Convertible ⦃...⦄ public
13+
14+
Convertible-Refl : ∀ {A} → Convertible A A
15+
Convertible-Refl = λ where .to → id; .from → id
16+
17+
Convertible₁ : (Set → Set) → (Set → Set) → Set₁
18+
Convertible₁ T U = ∀ {A B} → ⦃ Convertible A B ⦄ → Convertible (T A) (U B)
19+
20+
Convertible₂ : (Set → Set → Set) → (Set → Set → Set) → Set₁
21+
Convertible₂ T U = ∀ {A B} → ⦃ Convertible A B ⦄ → Convertible₁ (T A) (U B)
22+
23+
Functor⇒Convertible : ∀ {F : Type↑} → ⦃ Functor F ⦄ → Convertible₁ F F
24+
Functor⇒Convertible = λ where
25+
.to → fmap to
26+
.from → fmap from
27+
28+
Bifunctor⇒Convertible : ∀ {F} → ⦃ Bifunctor F ⦄ → Convertible₂ F F
29+
Bifunctor⇒Convertible = λ where
30+
.to → bimap to to
31+
.from → bimap from from
32+
33+
_⨾_ : ∀ {A B C} → Convertible A B → Convertible B C → Convertible A C
34+
(c ⨾ c') .to = c' .to ∘ c .to
35+
(c ⨾ c') .from = c .from ∘ c' .from

‎Class/Convertible/Instances.agda‎

Lines changed: 52 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,52 @@
1+
module Class.Convertible.Instances where
2+
3+
open import Meta.Prelude
4+
5+
open import Class.Functor
6+
open import Class.Bifunctor
7+
8+
open import Class.Convertible.Core
9+
10+
open import Class.HasHsType.Core
11+
12+
HsConvertible : (A : Set) → ⦃ HasHsType A ⦄ → Set
13+
HsConvertible A = Convertible A (HsType A)
14+
15+
open import Foreign.Haskell using (Pair; Either)
16+
open import Foreign.Haskell.Coerce using (coerce)
17+
18+
instance
19+
Convertible-ℕ : Convertible ℕ ℕ
20+
Convertible-ℕ = λ where
21+
.to → id
22+
.from → id
23+
24+
Convertible-Maybe : Convertible₁ Maybe Maybe
25+
Convertible-Maybe = Functor⇒Convertible
26+
27+
Convertible-× : Convertible₂ _×_ _×_
28+
Convertible-× = Bifunctor⇒Convertible
29+
30+
Convertible-Pair : Convertible₂ _×_ Pair
31+
Convertible-Pair = λ where
32+
.to → coerce ∘ bimap to to
33+
.from → bimap from from ∘ coerce
34+
35+
Convertible-⊎ : Convertible₂ _⊎_ _⊎_
36+
Convertible-⊎ = Bifunctor⇒Convertible
37+
38+
Convertible-Either : Convertible₂ _⊎_ Either
39+
Convertible-Either = λ where
40+
.to → coerce ∘ bimap to to
41+
.from → bimap from from ∘ coerce
42+
43+
Convertible-List : Convertible₁ List List
44+
Convertible-List = λ where
45+
.to → fmap to
46+
.from → fmap from
47+
48+
Convertible-Fun : ∀ {A A' B B'} →
49+
⦃ Convertible A A' ⦄ → ⦃ Convertible B B' ⦄ → Convertible (A → B) (A' → B')
50+
Convertible-Fun = λ where
51+
.to → λ f → to ∘ f ∘ from
52+
.from → λ f → from ∘ f ∘ to

‎Class/HasHsType.agda‎

Lines changed: 2 additions & 49 deletions
Original file line numberDiff line numberDiff line change
@@ -1,51 +1,4 @@
11
module Class.HasHsType where
22

3-
open import Level using (Level)
4-
open import Data.Bool.Base using (Bool)
5-
open import Data.Nat.Base using (ℕ)
6-
open import Data.String.Base using (String)
7-
open import Data.List.Base using (List)
8-
open import Data.Maybe.Base using (Maybe)
9-
open import Data.Sum.Base using (_⊎_)
10-
open import Data.Product.Base using (_×_)
11-
open import Data.Unit using (⊤)
12-
13-
open import Foreign.Haskell.Pair using (Pair)
14-
open import Foreign.Haskell.Either using (Either)
15-
16-
private variable
17-
l : Level
18-
A B : Set l
19-
20-
record HasHsType (A : Set l) : Set₁ where
21-
field
22-
HsType : Set
23-
24-
HsType : (A : Set l) → ⦃ HasHsType A ⦄ → Set
25-
HsType _ ⦃ i ⦄ = i .HasHsType.HsType
26-
27-
MkHsType : (A : Set l) (Hs : Set) → HasHsType A
28-
MkHsType A Hs .HasHsType.HsType = Hs
29-
30-
instance
31-
32-
iHsTy-ℕ = MkHsType ℕ ℕ
33-
iHsTy-Bool = MkHsType Bool Bool
34-
iHsTy-⊤ = MkHsType ⊤ ⊤
35-
iHsTy-String = MkHsType String String
36-
37-
-- Could make a macro for these kind of congruence instances.
38-
iHsTy-List : ⦃ HasHsType A ⦄ → HasHsType (List A)
39-
iHsTy-List {A = A} .HasHsType.HsType = List (HsType A)
40-
41-
iHsTy-Maybe : ⦃ HasHsType A ⦄ → HasHsType (Maybe A)
42-
iHsTy-Maybe {A = A} .HasHsType.HsType = Maybe (HsType A)
43-
44-
iHsTy-Fun : ⦃ HasHsType A ⦄ → ⦃ HasHsType B ⦄ → HasHsType (A → B)
45-
iHsTy-Fun {A = A} {B = B} .HasHsType.HsType = HsType A → HsType B
46-
47-
iHsTy-Sum : ⦃ HasHsType A ⦄ → ⦃ HasHsType B ⦄ → HasHsType (A ⊎ B)
48-
iHsTy-Sum {A = A} {B = B} .HasHsType.HsType = Either (HsType A) (HsType B)
49-
50-
iHsTy-Pair : ⦃ HasHsType A ⦄ → ⦃ HasHsType B ⦄ → HasHsType (A × B)
51-
iHsTy-Pair {A = A} {B = B} .HasHsType.HsType = Pair (HsType A) (HsType B)
3+
open import Class.HasHsType.Core public
4+
open import Class.HasHsType.Instances public

‎Class/HasHsType/Core.agda‎

Lines changed: 14 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,14 @@
1+
module Class.HasHsType.Core where
2+
3+
open import Meta.Prelude
4+
5+
record HasHsType (A : Set ℓ) : Set₁ where
6+
field HsType : Set
7+
8+
module _ (A : Set ℓ) where
9+
mkHsType : Set → HasHsType A
10+
mkHsType Hs .HasHsType.HsType = Hs
11+
12+
module _ ⦃ i : HasHsType A ⦄ where
13+
HsType : Set
14+
HsType = i .HasHsType.HsType

‎Class/HasHsType/Instances.agda‎

Lines changed: 32 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,32 @@
1+
module Class.HasHsType.Instances where
2+
3+
open import Meta.Prelude
4+
5+
open import Foreign.Haskell.Pair using (Pair)
6+
open import Foreign.Haskell.Either using (Either)
7+
8+
open import Class.HasHsType.Core
9+
10+
instance
11+
iHsTy-ℕ = mkHsType ℕ ℕ
12+
iHsTy-Bool = mkHsType Bool Bool
13+
iHsTy-⊤ = mkHsType ⊤ ⊤
14+
iHsTy-String = mkHsType String String
15+
16+
-- TODO: macro for these kind of congruence instances
17+
module _ ⦃ _ : HasHsType A ⦄ where instance
18+
iHsTy-List : HasHsType (List A)
19+
iHsTy-List .HasHsType.HsType = List (HsType A)
20+
21+
iHsTy-Maybe : HasHsType (Maybe A)
22+
iHsTy-Maybe .HasHsType.HsType = Maybe (HsType A)
23+
24+
module _ ⦃ _ : HasHsType B ⦄ where instance
25+
iHsTy-Fun : HasHsType (A → B)
26+
iHsTy-Fun .HasHsType.HsType = HsType A → HsType B
27+
28+
iHsTy-Sum : HasHsType (A ⊎ B)
29+
iHsTy-Sum .HasHsType.HsType = Either (HsType A) (HsType B)
30+
31+
iHsTy-Pair : HasHsType (A × B)
32+
iHsTy-Pair .HasHsType.HsType = Pair (HsType A) (HsType B)

‎Class/MonadError.agda‎

Lines changed: 1 addition & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -9,10 +9,7 @@ open import Reflection using (TC; ErrorPart; typeError; catchTC; strErr)
99

1010
module Class.MonadError where
1111

12-
private
13-
variable
14-
e f : Level
15-
A : Set f
12+
private variable e f : Level
1613

1714
record MonadError (E : Set e) (M : ∀ {f} → Set f → Set f) : Setω where
1815
field

‎Class/MonadReader.agda‎

Lines changed: 0 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -8,8 +8,6 @@ open import Class.Monad
88
open import Class.Functor
99
open import Class.MonadError
1010

11-
private variable ℓ : Level
12-
1311
open MonadError ⦃...⦄
1412

1513
record MonadReader (R : Set ℓ) (M : ∀ {a} → Set a → Set a) ⦃ _ : Monad M ⦄ : Setω where

‎Class/MonadTC.agda‎

Lines changed: 2 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -18,10 +18,6 @@ open import Class.Functor
1818
open import Class.Monad
1919
open import Class.Traversable
2020

21-
private variable
22-
a f : Level
23-
A B : Set f
24-
2521
data ReductionOptions : Set where
2622
onlyReduce : List Name → ReductionOptions
2723
dontReduce : List Name → ReductionOptions
@@ -71,7 +67,7 @@ record MonadTC (M : ∀ {f} → Set f → Set f)
7167
⦃ m : Monad M ⦄ ⦃ me : MonadError (List ErrorPart) M ⦄ : Setω₁ where
7268
field
7369
unify : Term → Term → M ⊤
74-
typeError : ∀ {A : Set f} → List ErrorPart → M A
70+
typeError : List ErrorPart → M A
7571
inferType : Term → M Type
7672
checkType : Term → Type → M Term
7773
normalise : Term → M Term
@@ -156,7 +152,7 @@ module _ {M : ∀ {f} → Set f → Set f}
156152
open MonadTC mtc
157153
open MonadReader mre
158154

159-
record IsMErrorPart (A : Set a) : Setω where
155+
record IsMErrorPart (A : Set ℓ) : Setω where
160156
field toMErrorPart : A → M (List ErrorPart)
161157

162158
open IsMErrorPart ⦃...⦄ public

‎Meta/Prelude.agda‎

Lines changed: 30 additions & 15 deletions
Original file line numberDiff line numberDiff line change
@@ -2,30 +2,45 @@
22

33
module Meta.Prelude where
44

5-
open import Level renaming (_⊔_ to _⊔ˡ_; suc to sucˡ; zero to zeroˡ) public
5+
-- ** stdlib re-exports
6+
open import Level public
7+
renaming (_⊔_ to _⊔ˡ_; suc to sucˡ; zero to zeroˡ)
68
open import Function public
79

8-
open import Data.Bool hiding (_≟_; _≤_; _≤?_; _<_; _<?_) public
10+
open import Data.Bool public
11+
hiding (_≟_; _≤_; _≤?_; _<_; _<?_)
912
open import Data.Empty public
10-
open import Data.List hiding (align; alignWith; fromMaybe; map; zip; zipWith) public
11-
open import Data.Maybe hiding (_>>=_; ap; align; alignWith; fromMaybe; map; zip; zipWith) public
12-
open import Data.Unit hiding (_≟_) public
13-
open import Data.Sum hiding (assocʳ; assocˡ; map; map₁; map₂; reduce; swap) public
14-
open import Data.Product hiding (assocʳ; assocˡ; map; map₁; map₂; swap; zip; zipWith) public
15-
open import Data.Nat hiding (_≟_; _≤_; _≤?_; _<_; _<?_; _≤ᵇ_; _≡ᵇ_) public
16-
open import Data.String using (String; _<+>_) public
17-
18-
open import Relation.Binary.PropositionalEquality hiding (preorder; setoid; [_]; module ≡-Reasoning; decSetoid) public
19-
13+
open import Data.List public
14+
hiding (align; alignWith; fromMaybe; map; zip; zipWith)
15+
open import Data.Maybe public
16+
hiding (_>>=_; ap; align; alignWith; fromMaybe; map; zip; zipWith)
17+
open import Data.Unit public
18+
hiding (_≟_)
19+
open import Data.Sum public
20+
hiding (assocʳ; assocˡ; map; map₁; map₂; reduce; swap)
21+
open import Data.Product public
22+
hiding (assocʳ; assocˡ; map; map₁; map₂; swap; zip; zipWith)
23+
open import Data.Nat public
24+
hiding (_≟_; _≤_; _≤?_; _<_; _<?_; _≤ᵇ_; _≡ᵇ_)
25+
open import Data.String public
26+
using (String; _<+>_)
27+
28+
open import Relation.Binary.PropositionalEquality public
29+
hiding (preorder; setoid; [_]; module ≡-Reasoning; decSetoid)
30+
31+
-- ** helper funs
2032
lookupᵇ : {A B : Set} → (A → A → Bool) → List (A × B) → A → Maybe B
2133
lookupᵇ f [] n = nothing
2234
lookupᵇ f ((k , v) ∷ l) n = if f k n then just v else lookupᵇ f l n
2335

24-
open import Data.Fin
25-
open import Data.List
26-
2736
zipWithIndex : {A B : Set} → (ℕ → A → B) → List A → List B
2837
zipWithIndex f l = zipWith f (upTo $ length l) l
38+
where open import Data.Fin; open import Data.List
2939

3040
enumerate : {A : Set} → List A → List (ℕ × A)
3141
enumerate = zipWithIndex _,_
42+
43+
-- ** variables
44+
variable
45+
ℓ ℓ′ ℓ″ : Level
46+
A B C D : Set ℓ

0 commit comments

Comments
 (0)