agda-stdlib-meta/Class/Convertible.agda at 85a2719f264bd19142e9ebc4e87f55b330f7019a · zahnsimo/agda-stdlib-meta · GitHub

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
module Class.Convertible where

open import Function
open import Class.HasHsType
open import Class.Core
open import Class.Functor
open import Class.Bifunctor
open import Data.Maybe
open import Data.Product
open import Data.Sum
open import Data.List

record Convertible (A B : Set) : Set where
  field to   : A → B
        from : B → A
open Convertible ⦃...⦄ public

HsConvertible : (A : Set) → ⦃ HasHsType A ⦄ → Set
HsConvertible A = Convertible A (HsType A)

Convertible-Refl : ∀ {A} → Convertible A A
Convertible-Refl = λ where .to → id; .from → id

Convertible₁ : (Set → Set) → (Set → Set) → Set₁
Convertible₁ T U = ∀ {A B} → ⦃ Convertible A B ⦄ → Convertible (T A) (U B)

Convertible₂ : (Set → Set → Set) → (Set → Set → Set) → Set₁
Convertible₂ T U = ∀ {A B} → ⦃ Convertible A B ⦄ → Convertible₁ (T A) (U B)

Functor⇒Convertible : ∀ {F : Type↑} → ⦃ Functor F ⦄ → Convertible₁ F F
Functor⇒Convertible = λ where
  .to   → fmap to
  .from → fmap from

Bifunctor⇒Convertible : ∀ {F} → ⦃ Bifunctor F ⦄ → Convertible₂ F F
Bifunctor⇒Convertible = λ where
  .to   → bimap to to
  .from → bimap from from

_⨾_ : ∀ {A B C} → Convertible A B → Convertible B C → Convertible A C
(c ⨾ c') .to   = c' .to   ∘ c  .to
(c ⨾ c') .from = c  .from ∘ c' .from

-- ** instances

open import Foreign.Haskell
open import Foreign.Haskell.Coerce using (coerce)

open import Data.Nat

instance
  Convertible-ℕ : Convertible ℕ ℕ
  Convertible-ℕ = λ where
    .to   → id
    .from → id

  Convertible-Maybe : Convertible₁ Maybe Maybe
  Convertible-Maybe = Functor⇒Convertible

  Convertible-× : Convertible₂ _×_ _×_
  Convertible-× = Bifunctor⇒Convertible

  Convertible-Pair : Convertible₂ _×_ Pair
  Convertible-Pair = λ where
    .to   → coerce ∘ bimap to to
    .from → bimap from from ∘ coerce

  Convertible-⊎ : Convertible₂ _⊎_ _⊎_
  Convertible-⊎ = Bifunctor⇒Convertible

  Convertible-Either : Convertible₂ _⊎_ Either
  Convertible-Either = λ where
    .to   → coerce ∘ bimap to to
    .from → bimap from from ∘ coerce

  Convertible-List : Convertible₁ List List
  Convertible-List = λ where
    .to   → fmap to
    .from → fmap from

  Convertible-Fun : ∀ {A A' B B'} → ⦃ Convertible A A' ⦄ → ⦃ Convertible B B' ⦄ → Convertible (A → B) (A' → B')
  Convertible-Fun = λ where
    .to   → λ f → to   ∘ f ∘ from
    .from → λ f → from ∘ f ∘ to