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