1
------------------------------------------------------------------------
2
-- Containers, based on the work of Abbott and others
3
------------------------------------------------------------------------
5
{-# OPTIONS --universe-polymorphism #-}
7
module Data.Container where
9
open import Data.Product as Prod hiding (map)
10
open import Function renaming (id to ⟨id⟩; _∘_ to _⟨∘⟩_)
11
open import Function.Equality using (_⟨$⟩_)
12
open import Function.Inverse as Inv using (_⇿_; module Inverse)
14
open import Relation.Binary using (Setoid; module Setoid)
15
open import Relation.Binary.PropositionalEquality as P
16
using (_≡_; _≗_; refl)
17
open import Relation.Unary using (_⊆_)
19
------------------------------------------------------------------------
22
-- A container is a set of shapes, and for every shape a set of
27
record Container (ℓ : Level) : Set (suc ℓ) where
31
Position : Shape → Set ℓ
35
-- The semantics ("extension") of a container.
37
⟦_⟧ : ∀ {ℓ} → Container ℓ → Set ℓ → Set ℓ
38
⟦ C ⟧ X = Σ[ s ∶ Shape C ] (Position C s → X)
40
-- Equality, parametrised on an underlying relation.
42
Eq : ∀ {c ℓ} {C : Container c} {X Y : Set c} →
43
(X → Y → Set ℓ) → ⟦ C ⟧ X → ⟦ C ⟧ Y → Set (c ⊔ ℓ)
44
Eq {C = C} _≈_ (s , f) (s′ , f′) =
45
Σ[ eq ∶ s ≡ s′ ] (∀ p → f p ≈ f′ (P.subst (Position C) eq p))
49
-- Note that, if propositional equality were extensional, then
50
-- Eq _≡_ and _≡_ would coincide.
52
Eq⇒≡ : ∀ {c} {C : Container c} {X : Set c} {xs ys : ⟦ C ⟧ X} →
53
P.Extensionality c c → Eq _≡_ xs ys → xs ≡ ys
54
Eq⇒≡ {C = C} {X} ext (s≡s′ , f≈f′) = helper s≡s′ f≈f′
56
helper : {s s′ : Shape C} (eq : s ≡ s′) →
57
{f : Position C s → X}
58
{f′ : Position C s′ → X} →
59
(∀ p → f p ≡ f′ (P.subst (Position C) eq p)) →
60
_≡_ {A = ⟦ C ⟧ X} (s , f) (s′ , f′)
61
helper refl f≈f′ = P.cong (_,_ _) (ext f≈f′)
63
setoid : ∀ {ℓ} → Container ℓ → Setoid ℓ ℓ → Setoid ℓ ℓ
65
{ Carrier = ⟦ C ⟧ X.Carrier
67
; isEquivalence = record
68
{ refl = (refl , λ _ → X.refl)
70
; trans = λ {_ _ zs} → trans zs
78
sym : {xs ys : ⟦ C ⟧ X.Carrier} → xs ≈ ys → ys ≈ xs
79
sym (eq , f) = helper eq f
81
helper : {s s′ : Shape C} (eq : s ≡ s′) →
82
{f : Position C s → X.Carrier}
83
{f′ : Position C s′ → X.Carrier} →
84
(∀ p → X._≈_ (f p) (f′ $ P.subst (Position C) eq p)) →
86
helper refl eq = (refl , X.sym ⟨∘⟩ eq)
88
trans : ∀ {xs ys : ⟦ C ⟧ X.Carrier} zs → xs ≈ ys → ys ≈ zs → xs ≈ zs
89
trans zs (eq₁ , f₁) (eq₂ , f₂) = helper eq₁ eq₂ (proj₂ zs) f₁ f₂
91
helper : {s s′ s″ : Shape C} (eq₁ : s ≡ s′) (eq₂ : s′ ≡ s″) →
92
{f : Position C s → X.Carrier}
93
{f′ : Position C s′ → X.Carrier} →
94
(f″ : Position C s″ → X.Carrier) →
95
(∀ p → X._≈_ (f p) (f′ $ P.subst (Position C) eq₁ p)) →
96
(∀ p → X._≈_ (f′ p) (f″ $ P.subst (Position C) eq₂ p)) →
98
helper refl refl _ eq₁ eq₂ = (refl , λ p → X.trans (eq₁ p) (eq₂ p))
100
------------------------------------------------------------------------
103
-- Containers are functors.
105
map : ∀ {c} {C : Container c} {X Y} → (X → Y) → ⟦ C ⟧ X → ⟦ C ⟧ Y
106
map f = Prod.map ⟨id⟩ (λ g → f ⟨∘⟩ g)
110
identity : ∀ {c} {C : Container c} X →
111
let module X = Setoid X in
112
(xs : ⟦ C ⟧ X.Carrier) → Eq X._≈_ (map ⟨id⟩ xs) xs
113
identity {C = C} X xs = Setoid.refl (setoid C X)
115
composition : ∀ {c} {C : Container c} {X Y} Z →
116
let module Z = Setoid Z in
117
(f : Y → Z.Carrier) (g : X → Y) (xs : ⟦ C ⟧ X) →
118
Eq Z._≈_ (map f (map g xs)) (map (f ⟨∘⟩ g) xs)
119
composition {C = C} Z f g xs = Setoid.refl (setoid C Z)
121
------------------------------------------------------------------------
122
-- Container morphisms
124
-- Representation of container morphisms.
126
record _⇒_ {c} (C₁ C₂ : Container c) : Set c where
128
shape : Shape C₁ → Shape C₂
129
position : ∀ {s} → Position C₂ (shape s) → Position C₁ s
133
-- Interpretation of _⇒_.
135
⟪_⟫ : ∀ {c} {C₁ C₂ : Container c} →
136
C₁ ⇒ C₂ → ∀ {X} → ⟦ C₁ ⟧ X → ⟦ C₂ ⟧ X
137
⟪ m ⟫ xs = (shape m (proj₁ xs) , proj₂ xs ⟨∘⟩ position m)
139
module Morphism where
143
Natural : ∀ {c} {C₁ C₂ : Container c} →
144
(∀ {X} → ⟦ C₁ ⟧ X → ⟦ C₂ ⟧ X) → Set (suc c)
146
∀ {X} (Y : Setoid c c) → let module Y = Setoid Y in
147
(f : X → Y.Carrier) (xs : ⟦ C₁ ⟧ X) →
148
Eq Y._≈_ (m $ map f xs) (map f $ m xs)
150
-- Natural transformations.
152
NT : ∀ {c} (C₁ C₂ : Container c) → Set (suc c)
153
NT C₁ C₂ = ∃ λ (m : ∀ {X} → ⟦ C₁ ⟧ X → ⟦ C₂ ⟧ X) → Natural m
155
-- Container morphisms are natural.
157
natural : ∀ {c} {C₁ C₂ : Container c}
158
(m : C₁ ⇒ C₂) → Natural ⟪ m ⟫
159
natural {C₂ = C₂} m Y f xs = Setoid.refl (setoid C₂ Y)
161
-- In fact, all natural functions of the right type are container
164
complete : ∀ {c} {C₁ C₂ : Container c} →
166
∃ λ m → (X : Setoid c c) →
167
let module X = Setoid X in
168
(xs : ⟦ C₁ ⟧ X.Carrier) →
169
Eq X._≈_ (proj₁ nt xs) (⟪ m ⟫ xs)
170
complete (nt , nat) =
171
(m , λ X xs → nat X (proj₂ xs) (proj₁ xs , ⟨id⟩))
173
m = record { shape = λ s → proj₁ (nt (s , ⟨id⟩))
174
; position = λ {s} → proj₂ (nt (s , ⟨id⟩))
179
id : ∀ {c} (C : Container c) → C ⇒ C
180
id _ = record {shape = ⟨id⟩; position = ⟨id⟩}
186
_∘_ : ∀ {c} {C₁ C₂ C₃ : Container c} → C₂ ⇒ C₃ → C₁ ⇒ C₂ → C₁ ⇒ C₃
188
{ shape = shape f ⟨∘⟩ shape g
189
; position = position g ⟨∘⟩ position f
192
-- Identity and composition commute with ⟪_⟫.
194
id-correct : ∀ {c} {C : Container c} {X : Set c} →
198
∘-correct : ∀ {c} {C₁ C₂ C₃ : Container c}
199
(f : C₂ ⇒ C₃) (g : C₁ ⇒ C₂) {X : Set c} →
200
⟪ f ∘ g ⟫ {X} ≗ (⟪ f ⟫ ⟨∘⟩ ⟪ g ⟫)
201
∘-correct f g xs = refl
203
------------------------------------------------------------------------
204
-- Linear container morphisms
206
record _⊸_ {c} (C₁ C₂ : Container c) : Set c where
208
shape⊸ : Shape C₁ → Shape C₂
209
position⊸ : ∀ {s} → Position C₂ (shape⊸ s) ⇿ Position C₁ s
214
; position = _⟨$⟩_ (Inverse.to position⊸)
217
⟪_⟫⊸ : ∀ {X} → ⟦ C₁ ⟧ X → ⟦ C₂ ⟧ X
220
open _⊸_ public using (shape⊸; position⊸; ⟪_⟫⊸)
222
------------------------------------------------------------------------
227
□ : ∀ {c} {C : Container c} {X : Set c} →
228
(X → Set c) → (⟦ C ⟧ X → Set c)
229
□ P (s , f) = ∀ p → P (f p)
231
□-map : ∀ {c} {C : Container c} {X : Set c} {P Q : X → Set c} →
232
P ⊆ Q → □ {C = C} P ⊆ □ Q
233
□-map P⊆Q = _⟨∘⟩_ P⊆Q
237
◇ : ∀ {c} {C : Container c} {X : Set c} →
238
(X → Set c) → (⟦ C ⟧ X → Set c)
239
◇ P (s , f) = ∃ λ p → P (f p)
241
◇-map : ∀ {c} {C : Container c} {X : Set c} {P Q : X → Set c} →
242
P ⊆ Q → ◇ {C = C} P ⊆ ◇ Q
243
◇-map P⊆Q = Prod.map ⟨id⟩ P⊆Q
249
_∈_ : ∀ {c} {C : Container c} {X : Set c} →
251
x ∈ xs = ◇ (_≡_ x) xs
253
-- Bag and set equality. Two containers xs and ys are equal when
254
-- viewed as sets if, whenever x ∈ xs, we also have x ∈ ys, and vice
255
-- versa. They are equal when viewed as bags if, additionally, the
256
-- sets x ∈ xs and x ∈ ys have the same size. For alternative but
257
-- equivalent definitions of bag and set equality, see
258
-- Data.Container.AlternativeBagAndSetEquality.
261
using (Kind) renaming (inverse to bag; equivalent to set)
263
[_]-Equality : ∀ {ℓ} → Kind → Container ℓ → Set ℓ → Setoid ℓ ℓ
264
[ k ]-Equality C X = Inv.InducedEquivalence₂ k (_∈_ {C = C} {X = X})
268
_≈[_]_ : ∀ {c} {C : Container c} {X : Set c} →
269
⟦ C ⟧ X → Kind → ⟦ C ⟧ X → Set c
270
xs ≈[ k ] ys = Setoid._≈_ ([ k ]-Equality _ _) xs ys
added
removed
src/Data/Container.agda
