open import 1Lab.Path
open import 1Lab.Type

open import Meta.Idiom

module Meta.Traversable where

Meta: Traversable🔗

The Traverse class captures the idea that some containers “commute with effects”, where an effect is anything implementing Idiom:

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