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
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
|
------------------------------------------------------------------------
-- The Agda standard library
--
-- Example showing how to define an indexed container
------------------------------------------------------------------------
{-# OPTIONS --with-K --safe --guardedness #-}
module README.Data.Container.Indexed.VectorExample where
open import Data.Unit
open import Data.Empty
open import Data.Nat.Base
open import Data.Product.Base using (_,_)
open import Function.Base using (_∋_)
open import Data.W.Indexed
open import Data.Container.Indexed
open import Data.Container.Indexed.WithK
module _ {a} (A : Set a) where
------------------------------------------------------------------------
-- Vector as an indexed container
-- An indexed container is defined by three things:
-- 1. Commands the user can emit
-- 2. Responses the indexed container returns to these commands
-- 3. Update of the index based on the command and the response issued.
-- For a vector, commands are constructors, responses are the number
-- of subvectors (0 if the vector is empty, 1 otherwise) and the
-- update corresponds to setting the size of the tail (if it exists).
-- We can formalize these ideas like so:
-- Depending on the size of the vector, we may have reached the end
-- already (nil) or we may specify what the head should be (cons).
-- This is the type of commands.
data VecC : ℕ → Set a where
nil : VecC zero
cons : ∀ n → A → VecC (suc n)
Vec : Container ℕ ℕ a _
Command Vec = VecC
-- We then treat each command independently, specifying both the response and the
-- next index based on that response.
-- In the nil case, the response is the empty type: there won't be any tail. As
-- a consequence, the next index won't be needed (and we can rely on the fact the
-- user will never be able to call it).
Response Vec nil = ⊥
next Vec nil = λ ()
-- In the cons case, the response is the unit type: there is exactly one tail. The
-- next index is the predecessor of the current one. It is handily handed over to
-- use by `cons`.
-- cons
Response Vec (cons n a) = ⊤
next Vec (cons n a) = λ _ → n
-- Finally we can define the type of Vector as the least fixed point of Vec.
Vector : ℕ → Set a
Vector = μ Vec
module _ {a} {A : Set a} where
-- We can recover the usual constructors by using `sup` to enter the fixpoint
-- and then using the appropriate pairing of a command & a handler for the
-- response.
-- For [], the response is ⊥ which makes it easy to conclude.
[] : Vector A 0
[] = sup (nil , λ ())
-- For _∷_, the response is ⊤ so we need to pass a tail. We give the one we took
-- as an argument.
infixr 3 _∷_
_∷_ : ∀ {n} → A → Vector A n → Vector A (suc n)
x ∷ xs = sup (cons _ x , λ _ → xs)
-- We can now use these constructors to build up vectors:
1⋯3 : Vector ℕ 3
1⋯3 = 1 ∷ 2 ∷ 3 ∷ []
-- Horrible thing to check the definition of _∈_ is not buggy.
-- Not sure whether we can say anything interesting about it in the case of Vector...
open import Relation.Binary.HeterogeneousEquality
_ : _∈_ {C = Vec ℕ} {X = Vector ℕ} 1⋯3 (⟦ Vec ℕ ⟧ (Vector ℕ) 4 ∋ cons _ 0 , λ _ → 1⋯3)
_ = _ , refl
|
