class Data.Traversable (T : Type u → Type u) extends Functor T : Type (u + 1)

Traversable captures structures that can be traversed left-to-right, performing an applicative action at each element and collecting results.

For a traversable $T$ and applicative $G$: $$\text{traverse} : (\alpha \to G\,\beta) \to T\,\alpha \to G\,(T\,\beta)$$ $$\text{sequence} : T\,(G\,\alpha) \to G\,(T\,\alpha)$$

The key insight: traverse generalizes both map (using Identity) and foldMap (using Const).

• map {α β : Type u} : (α → β) → T α → T β
• mapConst {α β : Type u} : α → T β → T α
• traverse {α β : Type u} {G : Type u → Type u} [Applicative G] : (α → G β) → T α → G (T β)

  Traverse a structure, applying an effectful function to each element and collecting results. $$\text{traverse}(f, [x_1, \ldots, x_n]) = f(x_1) \circledast f(x_2) \circledast \cdots \circledast f(x_n)$$ where $\circledast$ denotes applicative combination.

@[inline]

def Data.Traversable.sequence {T : Type u → Type u} {α : Type u} [Traversable T] {G : Type u → Type u} [Applicative G] (t : T (G α)) : G (T α)

Sequence effectful values left-to-right. $$\text{sequence}([m_1, \ldots, m_n]) = m_1 \circledast m_2 \circledast \cdots \circledast m_n$$ Equivalent to traverse id.

Equations

• Data.Traversable.sequence t = Data.Traversable.traverse id t

class Data.LawfulTraversable (T : Type u → Type u) [Traversable T] : Prop

Laws for a lawful traversable functor.

Identity: Traversing with pure is pure. $$\text{traverse}(\text{pure}) = \text{pure}$$

Naturality: Natural transformations commute with traverse.

• traverse_identity {α : Type u} (t : T α) : Traversable.traverse Functor.Identity.mk t = { runIdentity := t }

  Traversing with pure (Identity) is identity. $$\text{traverse}(\text{Identity.mk}) = \text{Identity.mk}$$

@[implicit_reducible]

instance Data.instTraversableList : Traversable List

Equations

• One or more equations did not get rendered due to their size.

@[implicit_reducible]

instance Data.instTraversableOption : Traversable Option

Equations

• One or more equations did not get rendered due to their size.

@[implicit_reducible]

instance Data.instTraversableNonEmpty : Traversable List.NonEmpty

Equations

• One or more equations did not get rendered due to their size.