module Meta.Traverse where

Meta: TraverseπŸ”—

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

record Traverse (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 Traverse ⦃ ... ⦄ public

instance
  Traverse-List : Traverse (eff List)
  Traverse-List .Traverse.traverse {M = M} {a = a} {b = b} = go where
    private module M = Effect M
    go : (a β†’ M.β‚€ b) β†’ List a β†’ M.β‚€ (List b)
    go f []       = pure []
    go f (x ∷ xs) = ⦇ f x ∷ go f xs ⦈

  Traverse-Maybe : Traverse (eff Maybe)
  Traverse-Maybe .Traverse.traverse f (just x) = just <$> f x
  Traverse-Maybe .Traverse.traverse f nothing  = pure nothing