Skip to content

Commit e00e780

Browse files
gallaisJacquesCarettejamesmckinna
authored
[ new ] Effect.Monad.Random (#2372)
* [ new ] Effect.Monad.Random Still TODO: instances for transformers * [ more ] add lifting along transformer * [ test ] for the new mtl-style constraint * [ cleanup ] this is not meant to be uploaded * [ fix ] declare effect.monad.random as unsafe * [ changelog ] listing new modules too * fix: `CHANGELOG` --------- Co-authored-by: Jacques Carette <[email protected]> Co-authored-by: jamesmckinna <[email protected]> Co-authored-by: jamesmckinna <[email protected]>
1 parent a7aac85 commit e00e780

File tree

10 files changed

+380
-2
lines changed

10 files changed

+380
-2
lines changed

‎CHANGELOG.md‎

Lines changed: 8 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -61,6 +61,8 @@ New modules
6161

6262
* `Data.List.Relation.Binary.Permutation.Declarative{.Properties}` for the least congruence on `List` making `_++_` commutative, and its equivalence with the `Setoid` definition.
6363

64+
* `Effect.Monad.Random` and `Effect.Monad.Random.Instances` for an mtl-style randomness monad constraint.
65+
6466
Additions to existing modules
6567
-----------------------------
6668

@@ -156,3 +158,9 @@ Additions to existing modules
156158
¬¬-η : A → ¬ ¬ A
157159
contradiction′ : ¬ A → A → Whatever
158160
```
161+
162+
* In `System.Random`:
163+
```agda
164+
randomIO : IO Bool
165+
randomRIO : RandomRIO {A = Bool} _≤_
166+
```

‎GenerateEverything.hs‎

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -59,6 +59,8 @@ unsafeModules = map modToFile
5959
, "Debug.Trace"
6060
, "Effect.Monad.IO"
6161
, "Effect.Monad.IO.Instances"
62+
, "Effect.Monad.Random"
63+
, "Effect.Monad.Random.Instances"
6264
, "Foreign.Haskell"
6365
, "Foreign.Haskell.Coerce"
6466
, "Foreign.Haskell.Either"

‎src/Effect/Monad/Random.agda‎

Lines changed: 249 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,249 @@
1+
------------------------------------------------------------------------
2+
-- The Agda standard library
3+
--
4+
-- The Random monad class
5+
------------------------------------------------------------------------
6+
7+
{-# OPTIONS --cubical-compatible --guardedness #-}
8+
9+
module Effect.Monad.Random where
10+
11+
open import Algebra using (RawMonoid)
12+
open import Effect.Functor using (RawFunctor)
13+
open import Function.Base using (id; const)
14+
open import IO.Base using (IO)
15+
open import Level using (Level; _⊔_)
16+
open import Relation.Binary.Core using (Rel)
17+
18+
open import System.Random as Random using (RandomRIO; InBounds)
19+
20+
private
21+
variable
22+
e f g s w : Level
23+
A : Set f
24+
B : Set g
25+
E : Set e
26+
S : Set s
27+
R : Rel A f
28+
M : Set f → Set g
29+
30+
------------------------------------------------------------------------
31+
-- Random monad operations
32+
33+
record RawMonadRandom
34+
(A : Set f)
35+
(M : Set f → Set g)
36+
: Set (f ⊔ g) where
37+
field
38+
getRandom : M A
39+
40+
record RawMonadRandomR
41+
(A : Set f) (_≤_ : Rel A f)
42+
(M : Set f → Set g)
43+
: Set (f ⊔ g) where
44+
field
45+
getRandom : M A
46+
getRandomR : (lo hi : A) → .(lo≤hi : lo ≤ hi) → M (InBounds _≤_ lo hi)
47+
48+
------------------------------------------------------------------------
49+
-- Operations over RawMonadRandom
50+
51+
forgetRanged : RawMonadRandomR A R M → RawMonadRandom A M
52+
forgetRanged m = record { getRandom = RawMonadRandomR.getRandom m }
53+
54+
------------------------------------------------------------------------
55+
-- IO monad specifics
56+
57+
module MkRandomIOInstances
58+
{a} {A : Set a} (_≤_ : Rel A a)
59+
(randomIO : IO A)
60+
(randomRIO : RandomRIO _≤_) where
61+
62+
monadRandomR : RawMonadRandomR A _≤_ IO
63+
monadRandomR = record
64+
{ getRandom = randomIO
65+
; getRandomR = randomRIO }
66+
67+
monadRandom : RawMonadRandom A IO
68+
monadRandom = forgetRanged monadRandomR
69+
70+
module Char where
71+
72+
open import Data.Char.Base using (Char; _≤_)
73+
open MkRandomIOInstances _≤_ Random.Char.randomIO Random.Char.randomRIO public
74+
75+
module Float where
76+
77+
open import Data.Float.Base using (Float; _≤_)
78+
open MkRandomIOInstances _≤_ Random.Float.randomIO Random.Float.randomRIO public
79+
80+
module ℤ where
81+
82+
open import Data.Integer.Base using (ℤ; _≤_)
83+
open MkRandomIOInstances _≤_ Random.ℤ.randomIO Random.ℤ.randomRIO public
84+
85+
module ℕ where
86+
87+
open import Data.Nat.Base using (ℕ; _≤_)
88+
open MkRandomIOInstances _≤_ Random.ℕ.randomIO Random.ℕ.randomRIO public
89+
90+
module Word64 where
91+
92+
open import Data.Word64.Base using (Word64; _≤_)
93+
open MkRandomIOInstances _≤_ Random.Word64.randomIO Random.Word64.randomRIO public
94+
95+
module Fin where
96+
97+
open import Data.Nat.Base using (ℕ; NonZero)
98+
open import Data.Fin.Base using (Fin; _≤_)
99+
100+
module _ (n : ℕ) .{{p : NonZero n}} where
101+
open MkRandomIOInstances _≤_ (Random.Fin.randomIO {{p}}) Random.Fin.randomRIO public
102+
103+
module Bool where
104+
105+
open import Data.Bool.Base using (Bool; _≤_)
106+
open MkRandomIOInstances _≤_ Random.Bool.randomIO Random.Bool.randomRIO public
107+
108+
module List {a} {A : Set a} (rIO : IO A) where
109+
110+
open import Data.List.Base using (List)
111+
112+
monadRandom : RawMonadRandom (List A) IO
113+
monadRandom = record { getRandom = Random.List.randomIO rIO }
114+
115+
116+
open import Data.Nat.Base using (ℕ)
117+
118+
module Vec {a} {A : Set a} (rIO : IO A) (n : ℕ) where
119+
120+
open import Data.Vec.Base using (Vec)
121+
122+
monadRandom : RawMonadRandom (Vec A n) IO
123+
monadRandom = record { getRandom = Random.Vec.randomIO rIO n }
124+
125+
module Vec≤ {a} {A : Set a} (rIO : IO A) (n : ℕ) where
126+
127+
open import Data.Vec.Bounded.Base using (Vec≤)
128+
129+
monadRandom : RawMonadRandom (Vec≤ A n) IO
130+
monadRandom = record { getRandom = Random.Vec≤.randomIO rIO n }
131+
132+
module String where
133+
134+
open import Data.String.Base using (String)
135+
136+
monadRandom : RawMonadRandom String IO
137+
monadRandom = record { getRandom = Random.String.randomIO }
138+
139+
module String≤ (n : ℕ) where
140+
141+
open import Data.String.Base using (String)
142+
143+
monadRandom : RawMonadRandom String IO
144+
monadRandom = record { getRandom = Random.String≤.randomIO n }
145+
146+
open import Data.Char.Base using (Char; _≤_)
147+
148+
module RangedString≤ (a b : Char) .(a≤b : a ≤ b) (n : ℕ) where
149+
150+
open import Data.String.Base using (String)
151+
152+
monadRandom : RawMonadRandom String IO
153+
monadRandom = record { getRandom = Random.RangedString≤.randomIO a b a≤b n }
154+
155+
open import Effect.Monad.Reader.Transformer.Base
156+
157+
liftReaderT : RawMonadRandom A M → RawMonadRandom A (ReaderT B M)
158+
liftReaderT rand = record
159+
{ getRandom = mkReaderT (const Rand.getRandom)
160+
} where module Rand = RawMonadRandom rand
161+
162+
liftRReaderT : RawMonadRandomR A R M → RawMonadRandomR A R (ReaderT B M)
163+
liftRReaderT randR = record
164+
{ getRandom = mkReaderT (const RandR.getRandom)
165+
; getRandomR = λ lo hi lo≤hi → mkReaderT (const (RandR.getRandomR lo hi lo≤hi))
166+
} where module RandR = RawMonadRandomR randR
167+
168+
open import Data.Product.Base using (_,_)
169+
open import Effect.Monad.Writer.Transformer.Base
170+
171+
module _ {𝕎 : RawMonoid w g} where
172+
173+
open RawMonoid 𝕎 renaming (Carrier to W)
174+
175+
liftWriterT : RawFunctor M →
176+
RawMonadRandom A M →
177+
RawMonadRandom A (WriterT 𝕎 M)
178+
liftWriterT M rand = record
179+
{ getRandom = mkWriterT (λ w → (w ,_) <$> Rand.getRandom)
180+
} where open RawFunctor M
181+
module Rand = RawMonadRandom rand
182+
183+
liftRWriterT : RawFunctor M →
184+
RawMonadRandomR A R M →
185+
RawMonadRandomR A R (WriterT 𝕎 M)
186+
liftRWriterT M randR = record
187+
{ getRandom = mkWriterT (λ w → (w ,_) <$> RandR.getRandom)
188+
; getRandomR = λ lo hi lo≤hi → mkWriterT (λ w → (w ,_) <$> RandR.getRandomR lo hi lo≤hi)
189+
} where open RawFunctor M
190+
module RandR = RawMonadRandomR randR
191+
192+
open import Effect.Monad.State.Transformer.Base
193+
194+
liftStateT : RawFunctor M →
195+
RawMonadRandom A M →
196+
RawMonadRandom A (StateT S M)
197+
liftStateT M rand = record
198+
{ getRandom = mkStateT (λ w → (w ,_) <$> Rand.getRandom)
199+
} where open RawFunctor M
200+
module Rand = RawMonadRandom rand
201+
202+
liftRStateT : RawFunctor M →
203+
RawMonadRandomR A R M →
204+
RawMonadRandomR A R (StateT S M)
205+
liftRStateT M randR = record
206+
{ getRandom = mkStateT (λ s → (s ,_) <$> RandR.getRandom)
207+
; getRandomR = λ lo hi lo≤hi → mkStateT (λ s → (s ,_) <$> RandR.getRandomR lo hi lo≤hi)
208+
} where open RawFunctor M
209+
module RandR = RawMonadRandomR randR
210+
211+
212+
open import Data.Sum.Base using (inj₁; inj₂; [_,_]′)
213+
open import Data.Sum.Effectful.Left.Transformer
214+
215+
liftSumₗT : RawFunctor M →
216+
RawMonadRandom A M →
217+
RawMonadRandom A (SumₗT E _ M)
218+
liftSumₗT M rand = record
219+
{ getRandom = mkSumₗT (inj₂ <$> Rand.getRandom)
220+
} where open RawFunctor M
221+
module Rand = RawMonadRandom rand
222+
223+
liftRSumₗT : RawFunctor M →
224+
RawMonadRandomR A R M →
225+
RawMonadRandomR A R (SumₗT E _ M)
226+
liftRSumₗT M randR = record
227+
{ getRandom = mkSumₗT (inj₂ <$> RandR.getRandom)
228+
; getRandomR = λ lo hi lo≤hi → mkSumₗT (inj₂ <$> RandR.getRandomR lo hi lo≤hi)
229+
} where open RawFunctor M
230+
module RandR = RawMonadRandomR randR
231+
232+
open import Data.Sum.Effectful.Right.Transformer
233+
234+
liftSumᵣT : RawFunctor M →
235+
RawMonadRandom A M →
236+
RawMonadRandom A (SumᵣT _ E M)
237+
liftSumᵣT M rand = record
238+
{ getRandom = mkSumᵣT (inj₁ <$> Rand.getRandom)
239+
} where open RawFunctor M
240+
module Rand = RawMonadRandom rand
241+
242+
liftRSumᵣT : RawFunctor M →
243+
RawMonadRandomR A R M →
244+
RawMonadRandomR A R (SumᵣT _ E M)
245+
liftRSumᵣT M randR = record
246+
{ getRandom = mkSumᵣT (inj₁ <$> RandR.getRandom)
247+
; getRandomR = λ lo hi lo≤hi → mkSumᵣT (inj₁ <$> RandR.getRandomR lo hi lo≤hi)
248+
} where open RawFunctor M
249+
module RandR = RawMonadRandomR randR

‎src/Effect/Monad/Random/Instances.agda‎

Lines changed: 57 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,57 @@
1+
------------------------------------------------------------------------
2+
-- The Agda standard library
3+
--
4+
-- Typeclass instances for the IO monad
5+
------------------------------------------------------------------------
6+
7+
{-# OPTIONS --cubical-compatible --guardedness #-}
8+
9+
module Effect.Monad.Random.Instances where
10+
11+
open import IO.Base using (IO)
12+
open import Level renaming (suc to lsuc)
13+
open import Effect.Monad.Random
14+
15+
instance
16+
ioMonadRandChar = Char.monadRandom
17+
ioMonadRandRChar = Char.monadRandomR
18+
19+
ioMonadRandFloat = Float.monadRandom
20+
ioMonadRandRFloat = Float.monadRandomR
21+
22+
ioMonadRandℤ = ℤ.monadRandom
23+
ioMonadRandRℤ = ℤ.monadRandomR
24+
25+
ioMonadRandℕ = ℕ.monadRandom
26+
ioMonadRandRℕ = ℕ.monadRandomR
27+
28+
ioMonadRandWord64 = Word64.monadRandom
29+
ioMonadRandRWord64 = Word64.monadRandomR
30+
31+
ioMonadRandFin = λ {n} {{nz}} → Fin.monadRandom n {{nz}}
32+
ioMonadRandRFin = λ {n} {{nz}} → Fin.monadRandomR n {{nz}}
33+
34+
ioMonadRandBool = Bool.monadRandom
35+
ioMonadRandRBool = Bool.monadRandomR
36+
37+
ioMonadRandList = λ {a} {A} {{rA}} → List.monadRandom {a} {A} (RawMonadRandom.getRandom {a} {lsuc a} {A} {IO} rA)
38+
39+
ioMonadRandVec = λ {a} {A} {{rA}} {n} → Vec.monadRandom {a} {A} (RawMonadRandom.getRandom {a} {lsuc a} {A} {IO} rA) n
40+
41+
ioMonadRandVec≤ = λ {a} {A} {{rA}} {n} → Vec≤.monadRandom {a} {A} (RawMonadRandom.getRandom {a} {lsuc a} {A} {IO} rA) n
42+
43+
ioMonadRandString = String.monadRandom
44+
45+
ioMonadRandString≤ = λ {n} → String≤.monadRandom n
46+
47+
ioMonadRandRangedString≤ = λ {a} {b} .{a≤b} {n} → RangedString≤.monadRandom a b a≤b n
48+
49+
50+
stateTMonadRand = λ {a} {s} {A} {S} {M} {{m}} {{mrand}} → liftStateT {a} {s} {A} {S} {M} m mrand
51+
stateTMonadRandR = λ {a} {s} {A} {R} {S} {M} {{m}} {{mrand}} → liftRStateT {a} {s} {A} {R} {S} {M} m mrand
52+
53+
readerTMonadRand = λ {a} {b} {A} {B} {M} {{mrand}} → liftReaderT {a} {b} {A} {B} {M} mrand
54+
readerTMonadRandR = λ {a} {b} {A} {R} {B} {M} {{mrand}} → liftRReaderT {a} {b} {A} {R} {B} {M} mrand
55+
56+
writerTMonadRand = λ {a} {f} {w} {A} {W} {M} {{m}} {{mrand}} → liftWriterT {a} {f} {w} {A} {W} {M} m mrand
57+
writerTMonadRandR = λ {a} {f} {w} {A} {R} {W} {M} {{m}} {{mrand}} → liftRWriterT {a} {f} {w} {A} {R} {W} {M} m mrand

‎src/System/Random.agda‎

Lines changed: 18 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -10,8 +10,9 @@ module System.Random where
1010

1111
import System.Random.Primitive as Prim
1212

13-
open import Data.Bool.Base using (T)
13+
open import Data.Bool.Base using (Bool; T) hiding (module Bool)
1414
open import Data.Nat.Base using (ℕ; z≤n) hiding (module ℕ)
15+
open import Data.Vec.Base using ([]; _∷_; lookup)
1516
open import Foreign.Haskell.Pair using (_,_)
1617
open import Function.Base using (_$_; _∘_)
1718
open import IO.Base using (IO; lift; lift!; _<$>_; _>>=_; pure)
@@ -30,7 +31,7 @@ record InBounds {a r} {A : Set a} (_≤_ : Rel A r) (lo hi : A) : Set (a ⊔ r)
3031
.isUpperBound : value ≤ hi
3132

3233
RandomRIO : ∀ {a r} {A : Set a} (_≤_ : Rel A r) → Set (suc (a ⊔ r))
33-
RandomRIO {A = A} _≤_ = (lo hi : A) → .(lo ≤ hi) → IO (InBounds _≤_ lo hi)
34+
RandomRIO {A = A} _≤_ = (lo hi : A) → .(lo≤hi : lo ≤ hi) → IO (InBounds _≤_ lo hi)
3435

3536
------------------------------------------------------------------------
3637
-- Instances
@@ -139,6 +140,21 @@ module Fin where
139140
k ← ℕ.randomRIO (toℕ lo) (toℕ hi) (Fin.toℕ-mono-≤ p)
140141
pure (toℕ-cancel-InBounds k)
141142

143+
module Bool where
144+
145+
open import Data.Bool.Base as Bool using (true; false; _≤_)
146+
open import Data.Bool.Properties using (≤-refl; ≤-minimum; ≤-maximum)
147+
148+
randomIO : IO Bool
149+
randomIO = lookup (true ∷ false ∷ []) <$> Fin.randomIO
150+
151+
randomRIO : RandomRIO {A = Bool} _≤_
152+
randomRIO false false lo≤hi = pure (false ∈[ ≤-refl , ≤-refl ])
153+
randomRIO false true lo≤hi = do
154+
b ← randomIO
155+
pure (b ∈[ ≤-minimum b , ≤-maximum b ])
156+
randomRIO true true lo≤hi = pure (true ∈[ ≤-refl , ≤-refl ])
157+
142158
module List {a} {A : Set a} (rIO : IO A) where
143159

144160
open import Data.List.Base using (List; replicate)

0 commit comments

Comments
 (0)