# 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 #

- `Traversable` type class - exposes the `traverse` function
- `sequence` - based on `traverse`, turns a collection of effects into an effect returning a collection
- `LawfulTraversable` - laws for a traversable functor
- `ApplicativeTransformation` - the notion of a natural transformation for applicative functors

## Tags #

traversable iterator functor applicative

## References #

- "Applicative Programming with Effects", by Conor McBride and Ross Paterson, Journal of Functional Programming 18:1 (2008) 1-13, online at http://www.soi.city.ac.uk/~ross/papers/Applicative.html
- "The Essence of the Iterator Pattern", by Jeremy Gibbons and Bruno Oliveira, in Mathematically-Structured Functional Programming, 2006, online at http://web.comlab.ox.ac.uk/oucl/work/jeremy.gibbons/publications/#iterator
- "An Investigation of the Laws of Traversals", by Mauro Jaskelioff and Ondrej Rypacek, in Mathematically-Structured Functional Programming, 2012, online at http://arxiv.org/pdf/1202.2919

source
structure ApplicativeTransformation (F : Type u → Type v) [Applicative F] (G : Type u → Type w) [Applicative G] :
Type (max (u + 1) v w)

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

- app (α : Type u) : F α → G α

  The function on objects defined by an `ApplicativeTransformation`.

- preserves_pure' {α : Type u} (x : α) : self.app α (pure x) = pure x

  An `ApplicativeTransformation` preserves `pure`.

- preserves_seq' {α β : Type u} (x : F (α → β)) (y : F α) : self.app β (x <*> y) = self.app (α → β) x <*> self.app α y

  An `ApplicativeTransformation` intertwines `seq`.

Instances For

source
instance ApplicativeTransformation.instCoeFunForallForall (F : Type u → Type v) [Applicative F] (G : Type u → Type w) [Applicative G] :
CoeFun (ApplicativeTransformation F G) fun (x : ApplicativeTransformation F G) => {α : Type u} → F α → G α
Equations

- ApplicativeTransformation.instCoeFunForallForall F G = { coe := fun (η : ApplicativeTransformation F G) {α : Type ?u.31} => η.app α }

source
theorem ApplicativeTransformation.app_eq_coe {F : Type u → Type v} [Applicative F] {G : Type u → Type w} [Applicative G] (η : ApplicativeTransformation F G) :
η.app = fun {α : Type u} => η.app α
source
@[simp]
theorem ApplicativeTransformation.coe_mk {F : Type u → Type v} [Applicative F] {G : Type u → Type w} [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) :
(fun {α : Type u} => { app := f, preserves_pure' := pp, preserves_seq' := ps }.app α) = f
source
theorem ApplicativeTransformation.congr_fun {F : Type u → Type v} [Applicative F] {G : Type u → Type w} [Applicative G] (η η' : ApplicativeTransformation F G) (h : η = η') {α : Type u} (x : F α) :
(fun {α : Type u} => η.app α) x = (fun {α : Type u} => η'.app α) x
source
theorem ApplicativeTransformation.congr_arg {F : Type u → Type v} [Applicative F] {G : Type u → Type w} [Applicative G] (η : ApplicativeTransformation F G) {α : Type u} {x y : F α} (h : x = y) :
(fun {α : Type u} => η.app α) x = (fun {α : Type u} => η.app α) y
source
theorem ApplicativeTransformation.coe_inj {F : Type u → Type v} [Applicative F] {G : Type u → Type w} [Applicative G] ⦃η η' : ApplicativeTransformation F G⦄ (h : (fun {α : Type u} => η.app α) = fun {α : Type u} => η'.app α) :
η = η'
source
theorem ApplicativeTransformation.ext {F : Type u → Type v} [Applicative F] {G : Type u → Type w} [Applicative G] ⦃η η' : ApplicativeTransformation F G⦄ (h : ∀ (α : Type u) (x : F α), (fun {α : Type u} => η.app α) x = (fun {α : Type u} => η'.app α) x) :
η = η'
source
theorem ApplicativeTransformation.ext_iff {F : Type u → Type v} [Applicative F] {G : Type u → Type w} [Applicative G] {η η' : ApplicativeTransformation F G} :
η = η' ↔ ∀ (α : Type u) (x : F α), (fun {α : Type u} => η.app α) x = (fun {α : Type u} => η'.app α) x
source
theorem ApplicativeTransformation.preserves_pure {F : Type u → Type v} [Applicative F] {G : Type u → Type w} [Applicative G] (η : ApplicativeTransformation F G) {α : Type u} (x : α) :
(fun {α : Type u} => η.app α) (pure x) = pure x
source
theorem ApplicativeTransformation.preserves_seq {F : Type u → Type v} [Applicative F] {G : Type u → Type w} [Applicative G] (η : ApplicativeTransformation F G) {α β : Type u} (x : F (α → β)) (y : F α) :
(fun {α : Type u} => η.app α) (x <*> y) = (fun {α : Type u} => η.app α) x <*> (fun {α : Type u} => η.app α) y
source
theorem ApplicativeTransformation.preserves_map {F : Type u → Type v} [Applicative F] {G : Type u → Type w} [Applicative G] (η : ApplicativeTransformation F G) [LawfulApplicative F] [LawfulApplicative G] {α β : Type u} (x : α → β) (y : F α) :
(fun {α : Type u} => η.app α) (x <$> y) = x <$> (fun {α : Type u} => η.app α) y
source
theorem ApplicativeTransformation.preserves_map' {F : Type u → Type v} [Applicative F] {G : Type u → Type w} [Applicative G] (η : ApplicativeTransformation F G) [LawfulApplicative F] [LawfulApplicative G] {α β : Type u} (x : α → β) :
(fun {α : Type u} => η.app α) ∘ Functor.map x = Functor.map x ∘ fun {α : Type u} => η.app α
source
def ApplicativeTransformation.idTransformation {F : Type u → Type v} [Applicative F] :
ApplicativeTransformation F F

The identity applicative transformation from an applicative functor to itself.

Equations

- ApplicativeTransformation.idTransformation = { app := fun (x : Type ?u.13) => id, preserves_pure' := ⋯, preserves_seq' := ⋯ }

Instances For

source
instance ApplicativeTransformation.instInhabited {F : Type u → Type v} [Applicative F] :
Inhabited (ApplicativeTransformation F F)
Equations

- ApplicativeTransformation.instInhabited = { default := ApplicativeTransformation.idTransformation }

source
def ApplicativeTransformation.comp {F : Type u → Type v} [Applicative F] {G : Type u → Type w} [Applicative G] {H : Type u → Type s} [Applicative H] (η' : ApplicativeTransformation G H) (η : ApplicativeTransformation F G) :
ApplicativeTransformation F H

The composition of applicative transformations.

Equations

- η'.comp η = { app := fun (x : Type ?u.44) (x_1 : F x) => (fun {α : Type ?u.44} => η'.app α) ((fun {α : Type ?u.44} => η.app α) x_1), preserves_pure' := ⋯, preserves_seq' := ⋯ }

Instances For

source
@[simp]
theorem ApplicativeTransformation.comp_apply {F : Type u → Type v} [Applicative F] {G : Type u → Type w} [Applicative G] {H : Type u → Type s} [Applicative H] (η' : ApplicativeTransformation G H) (η : ApplicativeTransformation F G) {α : Type u} (x : F α) :
(fun {α : Type u} => (η'.comp η).app α) x = (fun {α : Type u} => η'.app α) ((fun {α : Type u} => η.app α) x)
source
theorem ApplicativeTransformation.comp_assoc {F : Type u → Type v} [Applicative F] {G : Type u → Type w} [Applicative G] {H : Type u → Type s} [Applicative H] {I : Type u → Type t} [Applicative I] (η'' : ApplicativeTransformation H I) (η' : ApplicativeTransformation G H) (η : ApplicativeTransformation F G) :
(η''.comp η').comp η = η''.comp (η'.comp η)
source
@[simp]
theorem ApplicativeTransformation.comp_id {F : Type u → Type v} [Applicative F] {G : Type u → Type w} [Applicative G] (η : ApplicativeTransformation F G) :
η.comp idTransformation = η
source
@[simp]
theorem ApplicativeTransformation.id_comp {F : Type u → Type v} [Applicative F] {G : Type u → Type w} [Applicative G] (η : ApplicativeTransformation F G) :
idTransformation.comp η = η
source
class Traversable (t : Type u → Type u) extends Functor t :
Type (u + 1)

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 β)`.

- map {α β : Type u} : (α → β) → t α → t β
- mapConst {α β : Type u} : α → t β → t α
- traverse {m : Type u → Type u} [Applicative m] {α β : Type u} : (α → m β) → t α → m (t β)

  The function commuting a traversable functor `t` with an arbitrary applicative functor `m`.

Instances

source
def sequence {t : Type u → Type u} {α : Type u} {f : Type u → Type u} [Applicative f] [Traversable t] :
t (f α) → f (t α)

A traversable functor commutes with all applicative functors.

Equations

- sequence = traverse id

Instances For

source
class LawfulTraversable (t : Type u → Type u) [Traversable t] extends LawfulFunctor t :
Prop

A traversable functor is lawful if its `traverse` satisfies a number of additional properties. It must send `pure : α → Id α` to `pure`, send the composition of applicative functors to the composition of the `traverse` of each, send each function `f` to `fun x ↦ f <$> x`, and satisfy a naturality condition with respect to applicative transformations.

- map_const {α β : Type u} : Functor.mapConst = Functor.map ∘ Function.const β
- id_map {α : Type u} (x : t α) : id <$> x = x
- comp_map {α β γ : Type u} (g : α → β) (h : β → γ) (x : t α) : (h ∘ g) <$> x = h <$> g <$> x
- id_traverse {α : Type u} (x : t α) : traverse pure x = pure x

  `traverse` plays well with `pure` of the identity monad

- comp_traverse {F G : Type u → Type u} [Applicative F] [Applicative G] [LawfulApplicative F] [LawfulApplicative G] {α β γ : Type u} (f : β → F γ) (g : α → G β) (x : t α) : traverse (Functor.Comp.mk ∘ Functor.map f ∘ g) x = Functor.Comp.mk (traverse f <$> traverse g x)

  `traverse` plays well with composition of applicative functors.

- traverse_eq_map_id {α β : Type u} (f : α → β) (x : t α) : traverse (pure ∘ f) x = pure (f <$> x)

  An axiom for `traverse` involving `pure : β → Id β`.

- naturality {F G : Type u → Type u} [Applicative F] [Applicative G] [LawfulApplicative F] [LawfulApplicative G] (η : ApplicativeTransformation F G) {α β : Type u} (f : α → F β) (x : t α) : (fun {α : Type u} => η.app α) (traverse f x) = traverse ((fun {α : Type u} => η.app α) ∘ f) x

  The naturality axiom explaining how lawful traversable functors should play with lawful applicative functors.

Instances

source
instance instTraversableId :
Traversable Id
Equations

- instTraversableId = { toFunctor := Id.instMonad.toFunctor, traverse := fun {m : Type ?u.9 → Type ?u.9} [Applicative m] {α β : Type ?u.9} => id }

source
instance instLawfulTraversableId :
LawfulTraversable Id
source
instance instTraversableOption :
Traversable Option
Equations

- instTraversableOption = { toFunctor := instFunctorOption, traverse := fun {m : Type ?u.8 → Type ?u.8} [Applicative m] {α β : Type ?u.8} => Option.traverse }

source
instance instTraversableList :
Traversable List
Equations

- instTraversableList = { toFunctor := List.instFunctor, traverse := fun {m : Type ?u.8 → Type ?u.8} [Applicative m] {α β : Type ?u.8} => List.traverse }

source
def Sum.traverse {σ : Type u} {F : Type u → Type 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

- Sum.traverse f (Sum.inl x_1) = pure (Sum.inl x_1)
- Sum.traverse f (Sum.inr x_1) = Sum.inr <$> f x_1

Instances For

source
instance instTraversableSum {σ : Type u} :
Traversable (Sum σ)
Equations

- instTraversableSum = { toFunctor := Sum.instMonad_mathlib.toFunctor, traverse := @Sum.traverse σ }