Traversable.idr

module Prelude.Traversable

import Builtins

import Prelude.Basics
import Prelude.Applicative
import Prelude.Foldable
import Prelude.Functor

%access public export

traverse_ : (Foldable t, Applicative f) => (a -> f b) -> t a -> f ()
traverse_ f = foldr ((*>) . f) (pure ())

sequence_ : (Foldable t, Applicative f) => t (f a) -> f ()
sequence_ = foldr (*>) (pure ())

for_ : (Foldable t, Applicative f) => t a -> (a -> f b) -> f ()
for_ = flip traverse_

interface (Functor t, Foldable t) => Traversable (t : Type -> Type) where
  traverse : Applicative f => (a -> f b) -> t a -> f (t b)

sequence : (Traversable t, Applicative f) => t (f a) -> f (t a)
sequence = traverse id

for : (Traversable t, Applicative f) => t a -> (a -> f b) -> f (t b)
for = flip traverse