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

open import Data.List.Base

open import Meta.Idiom

open import Prim.Data.Maybe

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