/
Traversable.lagda.md
42 lines (34 loc) · 1.05 KB
/
Traversable.lagda.md
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
<!--
```agda
open import 1Lab.Path
open import 1Lab.Type
open import Meta.Idiom
```
-->
```agda
module Meta.Traversable where
```
# Meta: Traversable
The `Traverse`{.Agda} class captures the idea that some containers
"commute with effects", where an effect is anything implementing
`Idiom`{.Agda}:
```agda
record Traversable (F : Effect) : Typeω where
private module F = Effect F
field
traverse
: ∀ {ℓ₀ ℓ₁} {M : Effect} ⦃ i : Idiom M ⦄ (let module M = Effect M)
{a : Type ℓ₀} {b : Type ℓ₁}
→ (a → M.₀ b) → F.₀ a → M.₀ (F.₀ b)
for
: ∀ {ℓ₀ ℓ₁} {M : Effect} ⦃ i : Idiom M ⦄ (let module M = Effect M)
{a : Type ℓ₀} {b : Type ℓ₁}
→ F.₀ a → (a → M.₀ b) → M.₀ (F.₀ b)
for x f = traverse f x
open Traversable ⦃ ... ⦄ public
sequence
: ∀ {M F : Effect} ⦃ _ : Idiom M ⦄ ⦃ _ : Traversable F ⦄
(let module M = Effect M ; module F = Effect F) {ℓ}
{a : Type ℓ}
→ F.₀ (M.₀ a) → M.₀ (F.₀ a)
sequence = traverse id