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
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
|
------------------------------------------------------------------------
-- The Agda standard library
--
-- Example showing how the free monad construction on containers can be
-- used
------------------------------------------------------------------------
{-# OPTIONS --cubical-compatible --sized-types #-}
module README.Data.Container.FreeMonad where
open import Level using (0ℓ)
open import Effect.Monad
open import Data.Empty
open import Data.Unit
open import Data.Bool.Base using (Bool; true)
open import Data.Nat
open import Data.Sum.Base using (inj₁; inj₂)
open import Data.Product.Base
open import Data.Container using (Container; _▷_)
open import Data.Container.Combinator hiding (_×_)
open import Data.Container.FreeMonad
open import Data.W
open import Relation.Binary.PropositionalEquality as ≡
------------------------------------------------------------------------
-- Defining the signature of an effect and building trees describing
-- computations leveraging that effect.
-- The signature of state and its (generic) operations.
State : Set → Container _ _
State S = ⊤ ⟶ S ⊎ S ⟶ ⊤
where
_⟶_ : Set → Set → Container _ _
I ⟶ O = I ▷ λ _ → O
get : ∀ {S} → State S ⋆ S
get = impure (inj₁ _ , pure)
put : ∀ {S} → S → State S ⋆ ⊤
put s = impure (inj₂ s , pure)
-- Using the above we can, for example, write a stateful program that
-- delivers a boolean.
prog : State ℕ ⋆ Bool
prog =
get >>= λ n →
put (suc n) >>
pure true
where
open RawMonad monad using (_>>_)
runState : {S X : Set} → State S ⋆ X → (S → X × S)
runState (pure x) = λ s → x , s
runState (impure ((inj₁ _) , k)) = λ s → runState (k s) s
runState (impure ((inj₂ s) , k)) = λ _ → runState (k _) s
test : runState prog 0 ≡ (true , 1)
test = ≡.refl
-- It should be noted that @State S ⋆ X@ is not the state monad. If we
-- could quotient @State S ⋆ X@ by the seven axioms of state (see
-- Plotkin and Power's "Notions of Computation Determine Monads", 2002)
-- then we would get the state monad.
------------------------------------------------------------------------
-- Defining effectful inductive data structures
-- The definition of `C ⋆ A` is strictly positive in `A`, meaning that we
-- can use `C ⋆_` when defining (co)inductive datatypes.
open import Size
open import Codata.Sized.Thunk
open import Data.Vec.Base using (Vec; []; _∷_)
-- A `Tap C A` is a infinite source of `A`s provided that we can perform
-- the effectful computations described by `C`.
-- The first one can be accessed readily but the rest of them is hidden
-- under layers of `C` computations.
module _ (C : Container 0ℓ 0ℓ) (A : Set 0ℓ) where
data Tap (i : Size) : Set 0ℓ where
_∷_ : A → Thunk (λ i → C ⋆ Tap i) i → Tap i
-- We can run a given tap for a set number of steps and collect the elements
-- thus generated along the way. This gives us a `C ⋆_` computation of a vector.
module _ {C : Container 0ℓ 0ℓ} {A : Set 0ℓ} where
take : Tap C A _ → (n : ℕ) → C ⋆ Vec A n
take _ 0 = pure []
take (x ∷ _) 1 = pure (x ∷ [])
take (x ∷ mxs) (suc n) = do
xs ← mxs .force
rest ← take xs n
pure (x ∷ rest)
-- A stream of all the natural numbers starting from a given value is an
-- example of a tap.
natsFrom : ∀ {i} → State ℕ ⋆ Tap (State ℕ) ℕ i
natsFrom = let open RawMonad monad using (_>>_) in do
n ← get
put (suc n)
pure (n ∷ λ where .force → natsFrom)
-- We can use `take` to capture an initial segment of the `natsFrom` tap
-- and, after running the state operations, observe that it does generate
-- successive numbers.
_ : ∀ k →
runState (natsFrom >>= λ ns → take ns 5) k
≡ (k ∷ 1 + k ∷ 2 + k ∷ 3 + k ∷ 4 + k ∷ [] , 5 + k)
_ = λ k → refl
|
