on master help sign in
Comments in Prelude.Traversable
8885f72Edwin Brady
libs/prelude/Prelude/Traversable.idr+8
@@ -9,20 +9,28 @@ import Prelude.Functor
9
9
10%access public export
10%access public export
11
11
12+||| Map each element of a structure to a computation, evaluate those
13+||| computations and discard the results.
12traverse_ : (Foldable t, Applicative f) => (a -> f b) -> t a -> f ()
14traverse_ : (Foldable t, Applicative f) => (a -> f b) -> t a -> f ()
13traverse_ f = foldr ((*>) . f) (pure ())
15traverse_ f = foldr ((*>) . f) (pure ())
14
16
17+||| Evaluate each computation in a structure and discard the results
15sequence_ : (Foldable t, Applicative f) => t (f a) -> f ()
18sequence_ : (Foldable t, Applicative f) => t (f a) -> f ()
16sequence_ = foldr (*>) (pure ())
19sequence_ = foldr (*>) (pure ())
17
20
21+||| Like `traverse_` but with the arguments flipped
18for_ : (Foldable t, Applicative f) => t a -> (a -> f b) -> f ()
22for_ : (Foldable t, Applicative f) => t a -> (a -> f b) -> f ()
19for_ = flip traverse_
23for_ = flip traverse_
20
24
21interface (Functor t, Foldable t) => Traversable (t : Type -> Type) where
25interface (Functor t, Foldable t) => Traversable (t : Type -> Type) where
26+ ||| Map each element of a structure to a computation, evaluate those
27+ ||| computations and combine the results.
22 traverse : Applicative f => (a -> f b) -> t a -> f (t b)
28 traverse : Applicative f => (a -> f b) -> t a -> f (t b)
23
29
30+||| Evaluate each computation in a structure and collect the results
24sequence : (Traversable t, Applicative f) => t (f a) -> f (t a)
31sequence : (Traversable t, Applicative f) => t (f a) -> f (t a)
25sequence = traverse id
32sequence = traverse id
26
33
34+||| Like `traverse` but with the arguments flipped
27for : (Traversable t, Applicative f) => t a -> (a -> f b) -> f (t b)
35for : (Traversable t, Applicative f) => t a -> (a -> f b) -> f (t b)
28for = flip traverse
36for = flip traverse