← Back to branch summary

~ubuntu-branches/ubuntu/utopic/agda-stdlib/utopic-proposed

« back to all changes in this revision

Viewing changes to src/Data/Container/Combinator.agda

  • Committer: Package Import Robot
  • Author(s): Iain Lane
  • Date: 2011-11-29 17:00:35 UTC
  • mfrom: (1.1.3)
  • Revision ID: package-import@ubuntu.com-20111129170035-00v3pq4mmhoo5ulf
Tags: 0.6~darcs20111129t1640-1
* [ef445ab] Imported Upstream version 0.6~darcs20111129t1640
  + Darcs snapshot required for Agda 2.3.0 compatibility
* [f801f83] Update BDs and deps to require Agda 2.3.0
* [c52be90] Use 3.0 (quilt) for bz2 orig

Show diffs side-by-side

added added

removed removed

Lines of Context:
src/Data/Container/Combinator.agda
1
1
------------------------------------------------------------------------
 
2
-- The Agda standard library
 
3
--
2
4
-- Container combinators
3
5
------------------------------------------------------------------------
4
6
 
5
 
{-# OPTIONS --universe-polymorphism #-}
6
 
 
7
7
module Data.Container.Combinator where
8
8
 
9
9
open import Data.Container
12
12
open import Data.Sum renaming (_⊎_ to _⟨⊎⟩_)
13
13
open import Data.Unit using (⊤)
14
14
open import Function as F hiding (id; const) renaming (_∘_ to _⟨∘⟩_)
15
 
open import Function.Inverse using (_⇿_)
 
15
open import Function.Inverse using (_↔_)
16
16
open import Level
17
17
open import Relation.Binary.PropositionalEquality as P
18
18
  using (_≗_; refl)
23
23
-- Identity.
24
24
 
25
25
id : ∀ {c} → Container c
26
 
id = Lift ⊤ ◃ F.const (Lift ⊤)
 
26
id = Lift ⊤ ▷ F.const (Lift ⊤)
27
27
 
28
28
-- Constant.
29
29
 
30
30
const : ∀ {c} → Set c → Container c
31
 
const X = X ◃ F.const (Lift ⊥)
 
31
const X = X ▷ F.const (Lift ⊥)
32
32
 
33
33
-- Composition.
34
34
 
35
35
infixr 9 _∘_
36
36
 
37
37
_∘_ : ∀ {c} → Container c → Container c → Container c
38
 
C₁ ∘ C₂ = ⟦ C₁ ⟧ (Shape C₂) ◃ ◇ (Position C₂)
 
38
C₁ ∘ C₂ = ⟦ C₁ ⟧ (Shape C₂) ▷ ◇ (Position C₂)
39
39
 
40
40
-- Product. (Note that, up to isomorphism, this is a special case of
41
41
-- indexed product.)
44
44
 
45
45
_×_ : ∀ {c} → Container c → Container c → Container c
46
46
C₁ × C₂ =
47
 
  (Shape C₁ ⟨×⟩ Shape C₂) ◃
 
47
  (Shape C₁ ⟨×⟩ Shape C₂) ▷
48
48
  uncurry (λ s₁ s₂ → Position C₁ s₁ ⟨⊎⟩ Position C₂ s₂)
49
49
 
50
50
-- Indexed product.
51
51
 
52
52
Π : ∀ {c} {I : Set c} → (I → Container c) → Container c
53
 
Π C = (∀ i → Shape (C i)) ◃ λ s → ∃ λ i → Position (C i) (s i)
 
53
Π C = (∀ i → Shape (C i)) ▷ λ s → ∃ λ i → Position (C i) (s i)
54
54
 
55
55
-- Sum. (Note that, up to isomorphism, this is a special case of
56
56
-- indexed sum.)
58
58
infixr 1 _⊎_
59
59
 
60
60
_⊎_ : ∀ {c} → Container c → Container c → Container c
61
 
C₁ ⊎ C₂ = (Shape C₁ ⟨⊎⟩ Shape C₂) ◃ [ Position C₁ , Position C₂ ]
 
61
C₁ ⊎ C₂ = (Shape C₁ ⟨⊎⟩ Shape C₂) ▷ [ Position C₁ , Position C₂ ]
62
62
 
63
63
-- Indexed sum.
64
64
 
65
65
Σ : ∀ {c} {I : Set c} → (I → Container c) → Container c
66
 
Σ C = (∃ λ i → Shape (C i)) ◃ λ s → Position (C (proj₁ s)) (proj₂ s)
 
66
Σ C = (∃ λ i → Shape (C i)) ▷ λ s → Position (C (proj₁ s)) (proj₂ s)
67
67
 
68
68
-- Constant exponentiation. (Note that this is a special case of
69
69
-- indexed product.)
82
82
 
83
83
module Identity where
84
84
 
85
 
  correct : ∀ {c} {X : Set c} → ⟦ id ⟧ X ⇿ F.id X
 
85
  correct : ∀ {c} {X : Set c} → ⟦ id ⟧ X ↔ F.id X
86
86
  correct {c} = record
87
87
    { to         = P.→-to-⟶ {a  = c} λ xs → proj₂ xs _
88
88
    ; from       = P.→-to-⟶ {b₁ = c} λ x → (_ , λ _ → x)
94
94
 
95
95
module Constant (ext : ∀ {ℓ} → P.Extensionality ℓ ℓ) where
96
96
 
97
 
  correct : ∀ {ℓ} (X : Set ℓ) {Y} → ⟦ const X ⟧ Y ⇿ F.const X Y
 
97
  correct : ∀ {ℓ} (X : Set ℓ) {Y} → ⟦ const X ⟧ Y ↔ F.const X Y
98
98
  correct X {Y} = record
99
99
    { to         = P.→-to-⟶ to
100
100
    ; from       = P.→-to-⟶ from
114
114
module Composition where
115
115
 
116
116
  correct : ∀ {c} (C₁ C₂ : Container c) {X : Set c} →
117
 
            ⟦ C₁ ∘ C₂ ⟧ X ⇿ (⟦ C₁ ⟧ ⟨∘⟩ ⟦ C₂ ⟧) X
 
117
            ⟦ C₁ ∘ C₂ ⟧ X ↔ (⟦ C₁ ⟧ ⟨∘⟩ ⟦ C₂ ⟧) X
118
118
  correct C₁ C₂ {X} = record
119
119
    { to         = P.→-to-⟶ to
120
120
    ; from       = P.→-to-⟶ from
133
133
module Product (ext : ∀ {ℓ} → P.Extensionality ℓ ℓ) where
134
134
 
135
135
  correct : ∀ {c} (C₁ C₂ : Container c) {X : Set c} →
136
 
            ⟦ C₁ × C₂ ⟧ X ⇿ (⟦ C₁ ⟧ X ⟨×⟩ ⟦ C₂ ⟧ X)
 
136
            ⟦ C₁ × C₂ ⟧ X ↔ (⟦ C₁ ⟧ X ⟨×⟩ ⟦ C₂ ⟧ X)
137
137
  correct {c} C₁ C₂ {X} = record
138
138
    { to         = P.→-to-⟶ to
139
139
    ; from       = P.→-to-⟶ from
156
156
module IndexedProduct where
157
157
 
158
158
  correct : ∀ {c I} (C : I → Container c) {X : Set c} →
159
 
            ⟦ Π C ⟧ X ⇿ (∀ i → ⟦ C i ⟧ X)
 
159
            ⟦ Π C ⟧ X ↔ (∀ i → ⟦ C i ⟧ X)
160
160
  correct {I = I} C {X} = record
161
161
    { to         = P.→-to-⟶ to
162
162
    ; from       = P.→-to-⟶ from
175
175
module Sum where
176
176
 
177
177
  correct : ∀ {c} (C₁ C₂ : Container c) {X : Set c} →
178
 
            ⟦ C₁ ⊎ C₂ ⟧ X ⇿ (⟦ C₁ ⟧ X ⟨⊎⟩ ⟦ C₂ ⟧ X)
 
178
            ⟦ C₁ ⊎ C₂ ⟧ X ↔ (⟦ C₁ ⟧ X ⟨⊎⟩ ⟦ C₂ ⟧ X)
179
179
  correct C₁ C₂ {X} = record
180
180
    { to         = P.→-to-⟶ to
181
181
    ; from       = P.→-to-⟶ from
199
199
module IndexedSum where
200
200
 
201
201
  correct : ∀ {c I} (C : I → Container c) {X : Set c} →
202
 
            ⟦ Σ C ⟧ X ⇿ (∃ λ i → ⟦ C i ⟧ X)
 
202
            ⟦ Σ C ⟧ X ↔ (∃ λ i → ⟦ C i ⟧ X)
203
203
  correct {I = I} C {X} = record
204
204
    { to         = P.→-to-⟶ to
205
205
    ; from       = P.→-to-⟶ from
218
218
module ConstantExponentiation where
219
219
 
220
220
  correct : ∀ {c X} (C : Container c) {Y : Set c} →
221
 
            ⟦ const[ X ]⟶ C ⟧ Y ⇿ (X → ⟦ C ⟧ Y)
 
221
            ⟦ const[ X ]⟶ C ⟧ Y ↔ (X → ⟦ C ⟧ Y)
222
222
  correct C = IndexedProduct.correct (F.const C)