mathlib documentation

control.traversable.basic

Traversable type class #

Type classes for traversing collections. The concepts and laws are taken from http://hackage.haskell.org/package/base-4.11.1.0/docs/Data-Traversable.html

Traversable collections are a generalization of functors. Whereas functors (such as list) allow us to apply a function to every element, it does not allow functions which external effects encoded in a monad. Consider for instance a functor invite : email → io response that takes an email address, sends an email and waits for a response. If we have a list guests : list email, using calling invite using map gives us the following: map invite guests : list (io response). It is not what we need. We need something of type io (list response). Instead of using map, we can use traverse to send all the invites: traverse invite guests : io (list response). traverse applies invite to every element of guests and combines all the resulting effects. In the example, the effect is encoded in the monad io but any applicative functor is accepted by traverse.

For more on how to use traversable, consider the Haskell tutorial: https://en.wikibooks.org/wiki/Haskell/Traversable

Main definitions #

Tags #

traversable iterator functor applicative

References #

structure applicative_transformation (F : Type uType v) [applicative F] [is_lawful_applicative F] (G : Type uType w) [applicative G] [is_lawful_applicative G] :
Type (max (u+1) v w)
  • app : Π (α : Type ?), F αG α
  • preserves_pure' : ∀ {α : Type ?} (x : α), self.app α (pure x) = pure x
  • preserves_seq' : ∀ {α β : Type ?} (x : F (α → β)) (y : F α), self.app β (x <*> y) = self.app (α → β) x <*> self.app α y

A transformation between applicative functors. It is a natural transformation such that app preserves the has_pure.pure and functor.map (<*>) operations. See applicative_transformation.preserves_map for naturality.

@[protected, instance]
def applicative_transformation.has_coe_to_fun (F : Type uType v) [applicative F] [is_lawful_applicative F] (G : Type uType w) [applicative G] [is_lawful_applicative G] :
has_coe_to_fun (applicative_transformation F G) (λ (_x : applicative_transformation F G), Π {α : Type u}, F αG α)
Equations
@[simp]
theorem applicative_transformation.app_eq_coe {F : Type uType v} [applicative F] [is_lawful_applicative F] {G : Type uType w} [applicative G] [is_lawful_applicative G] (η : applicative_transformation F G) :
η.app = η
@[simp]
theorem applicative_transformation.coe_mk {F : Type uType v} [applicative F] [is_lawful_applicative F] {G : Type uType w} [applicative G] [is_lawful_applicative G] (f : Π (α : Type u), F αG α) (pp : ∀ {α : Type u} (x : α), f α (pure x) = pure x) (ps : ∀ {α β : Type u} (x : F (α → β)) (y : F α), f β (x <*> y) = f (α → β) x <*> f α y) :
{app := f, preserves_pure' := pp, preserves_seq' := ps} = f
@[protected]
theorem applicative_transformation.congr_fun {F : Type uType v} [applicative F] [is_lawful_applicative F] {G : Type uType w} [applicative G] [is_lawful_applicative G] (η η' : applicative_transformation F G) (h : η = η') {α : Type u} (x : F α) :
η x = η' x
@[protected]
theorem applicative_transformation.congr_arg {F : Type uType v} [applicative F] [is_lawful_applicative F] {G : Type uType w} [applicative G] [is_lawful_applicative G] (η : applicative_transformation F G) {α : Type u} {x y : F α} (h : x = y) :
η x = η y
theorem applicative_transformation.coe_inj {F : Type uType v} [applicative F] [is_lawful_applicative F] {G : Type uType w} [applicative G] [is_lawful_applicative G] ⦃η η' : applicative_transformation F G⦄ (h : η = η') :
η = η'
@[ext]
theorem applicative_transformation.ext {F : Type uType v} [applicative F] [is_lawful_applicative F] {G : Type uType w} [applicative G] [is_lawful_applicative G] ⦃η η' : applicative_transformation F G⦄ (h : ∀ (α : Type u) (x : F α), η x = η' x) :
η = η'
theorem applicative_transformation.ext_iff {F : Type uType v} [applicative F] [is_lawful_applicative F] {G : Type uType w} [applicative G] [is_lawful_applicative G] {η η' : applicative_transformation F G} :
η = η' ∀ (α : Type u) (x : F α), η x = η' x
theorem applicative_transformation.preserves_pure {F : Type uType v} [applicative F] [is_lawful_applicative F] {G : Type uType w} [applicative G] [is_lawful_applicative G] (η : applicative_transformation F G) {α : Type u} (x : α) :
η (pure x) = pure x
theorem applicative_transformation.preserves_seq {F : Type uType v} [applicative F] [is_lawful_applicative F] {G : Type uType w} [applicative G] [is_lawful_applicative G] (η : applicative_transformation F G) {α β : Type u} (x : F (α → β)) (y : F α) :
η (x <*> y) = η x <*> η y
theorem applicative_transformation.preserves_map {F : Type uType v} [applicative F] [is_lawful_applicative F] {G : Type uType w} [applicative G] [is_lawful_applicative G] (η : applicative_transformation F G) {α β : Type u} (x : α → β) (y : F α) :
η (x <$> y) = x <$> η y
theorem applicative_transformation.preserves_map' {F : Type uType v} [applicative F] [is_lawful_applicative F] {G : Type uType w} [applicative G] [is_lawful_applicative G] (η : applicative_transformation F G) {α β : Type u} (x : α → β) :

The identity applicative transformation from an applicative functor to itself.

Equations
def applicative_transformation.comp {F : Type uType v} [applicative F] [is_lawful_applicative F] {G : Type uType w} [applicative G] [is_lawful_applicative G] {H : Type uType s} [applicative H] [is_lawful_applicative H] (η' : applicative_transformation G H) (η : applicative_transformation F G) :

The composition of applicative transformations.

Equations
@[simp]
theorem applicative_transformation.comp_apply {F : Type uType v} [applicative F] [is_lawful_applicative F] {G : Type uType w} [applicative G] [is_lawful_applicative G] {H : Type uType s} [applicative H] [is_lawful_applicative H] (η' : applicative_transformation G H) (η : applicative_transformation F G) {α : Type u} (x : F α) :
(η'.comp η) x = η' (η x)
theorem applicative_transformation.comp_assoc {F : Type uType v} [applicative F] [is_lawful_applicative F] {G : Type uType w} [applicative G] [is_lawful_applicative G] {H : Type uType s} [applicative H] [is_lawful_applicative H] {I : Type uType t} [applicative I] [is_lawful_applicative I] (η'' : applicative_transformation H I) (η' : applicative_transformation G H) (η : applicative_transformation F G) :
(η''.comp η').comp η = η''.comp (η'.comp η)
@[class]
structure traversable (t : Type uType u) :
Type (u+1)
  • to_functor : functor t
  • traverse : Π {m : Type ?Type ?} [_inst_1 : applicative m] {α β : Type ?}, (α → m β)t αm (t β)

A traversable functor is a functor along with a way to commute with all applicative functors (see sequence). For example, if t is the traversable functor list and m is the applicative functor io, then given a function f : α → io β, the function functor.map f is list α → list (io β), but traverse f is list α → io (list β).

Instances
def sequence {t : Type uType u} {α : Type u} {f : Type uType u} [applicative f] [traversable t] :
t (f α)f (t α)

A traversable functor commutes with all applicative functors.

Equations
@[class]
structure is_lawful_traversable (t : Type uType u) [traversable t] :
Type (u+1)

A traversable functor is lawful if its traverse satisfies a number of additional properties. It must send id.mk to id.mk, send the composition of applicative functors to the composition of the traverse of each, send each function f to λ x, f <$> x, and satisfy a naturality condition with respect to applicative transformations.

Instances
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected]
def sum.traverse {σ : Type u} {F : Type uType u} [applicative F] {α : Type u_1} {β : Type u} (f : α → F β) :
σ αF β)

Defines a traverse function on the second component of a sum type. This is used to give a traversable instance for the functor σ ⊕ -.

Equations