doc-next-gen

Mathlib.Control.Traversable.Basic

Module docstring

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

ApplicativeTransformation structure
Full source 
/-- 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. -/
structure ApplicativeTransformation : Type max (u + 1) v w where
  /-- The function on objects defined by an `ApplicativeTransformation`. -/
  app : ∀ α : Type u, F α → G α
  /-- An `ApplicativeTransformation` preserves `pure`. -/
  preserves_pure' : ∀ {α : Type u} (x : α), app _ (pure x) = pure x
  /-- An `ApplicativeTransformation` intertwines `seq`. -/
  preserves_seq' : ∀ {α β : Type u} (x : F (α → β)) (y : F α), app _ (x <*> y) = app _ x <*> app _ y
Applicative Transformation
Informal description
An applicative transformation is a natural transformation between two applicative functors \( F \) and \( G \) that preserves the `pure` and `<*>` operations. Specifically, for any type \( \alpha \), the transformation \( \eta : F \alpha \to G \alpha \) must satisfy: 1. \( \eta (\text{pure } a) = \text{pure } a \) for any \( a : \alpha \), 2. \( \eta (f <*> x) = \eta f <*> \eta x \) for any \( f : F (\alpha \to \beta) \) and \( x : F \alpha \).
ApplicativeTransformation.instCoeFunForallForall instance
: CoeFun (ApplicativeTransformation F G) fun _ => ∀ {α}, F α → G α
Full source 
instance : CoeFun (ApplicativeTransformation F G) fun _ => ∀ {α}, F α → G α :=
  ⟨fun η ↦ η.app _⟩
Applicative Transformation as Function
Informal description
For any applicative transformation $\eta$ from $F$ to $G$, there is a canonical way to view $\eta$ as a function that maps elements of $F \alpha$ to $G \alpha$ for any type $\alpha$.
ApplicativeTransformation.app_eq_coe theorem
(η : ApplicativeTransformation F G) : η.app = η
Full source 
theorem app_eq_coe (η : ApplicativeTransformation F G) : η.app = η :=
  rfl
Applicative Transformation Application Equals Transformation
Informal description
For any applicative transformation $\eta$ from $F$ to $G$, the application function $\eta.app$ is equal to $\eta$ itself.
ApplicativeTransformation.coe_mk theorem
(f : ∀ α : Type u, F α → G α) (pp ps) : (ApplicativeTransformation.mk f @pp @ps) = f
Full source 
@[simp]
theorem coe_mk (f : ∀ α : Type u, F α → G α) (pp ps) :
    (ApplicativeTransformation.mk f @pp @ps) = f :=
  rfl
Construction of Applicative Transformation Equals Underlying Function
Informal description
For any function $f$ that maps types $\alpha$ to functions from $F \alpha$ to $G \alpha$, and for any proofs `pp` and `ps`, the construction of an applicative transformation using `ApplicativeTransformation.mk` with $f$, `pp`, and `ps` is equal to $f$ itself.
ApplicativeTransformation.congr_fun theorem
(η η' : ApplicativeTransformation F G) (h : η = η') {α : Type u} (x : F α) : η x = η' x
Full source 
protected theorem congr_fun (η η' : ApplicativeTransformation F G) (h : η = η') {α : Type u}
    (x : F α) : η x = η' x :=
  congrArg (fun η'' : ApplicativeTransformation F G => η'' x) h
Congruence of Applicative Transformation Application under Equality
Informal description
For any two applicative transformations $\eta$ and $\eta'$ from $F$ to $G$, if $\eta = \eta'$, then for any type $\alpha$ and any $x \in F \alpha$, we have $\eta(x) = \eta'(x)$.
ApplicativeTransformation.congr_arg theorem
(η : ApplicativeTransformation F G) {α : Type u} {x y : F α} (h : x = y) : η x = η y
Full source 
protected theorem congr_arg (η : ApplicativeTransformation F G) {α : Type u} {x y : F α}
    (h : x = y) : η x = η y :=
  congrArg (fun z : F α => η z) h
Congruence of Applicative Transformation under Equality
Informal description
For any applicative transformation $\eta$ from $F$ to $G$, and for any type $\alpha$, if $x$ and $y$ are equal elements of $F \alpha$, then applying $\eta$ to $x$ and $y$ yields equal results in $G \alpha$, i.e., $\eta(x) = \eta(y)$.
ApplicativeTransformation.coe_inj theorem
⦃η η' : ApplicativeTransformation F G⦄ (h : (η : ∀ α, F α → G α) = η') : η = η'
Full source 
theorem coe_inj ⦃η η' : ApplicativeTransformation F G⦄ (h : (η : ∀ α, F α → G α) = η') :
    η = η' := by
  cases η
  cases η'
  congr
Injectivity of Applicative Transformation Coefficients
Informal description
For any two applicative transformations $\eta$ and $\eta'$ from $F$ to $G$, if their underlying functions are equal (i.e., $\eta = \eta'$ as functions $\forall \alpha, F \alpha \to G \alpha$), then $\eta = \eta'$ as applicative transformations.
ApplicativeTransformation.ext theorem
⦃η η' : ApplicativeTransformation F G⦄ (h : ∀ (α : Type u) (x : F α), η x = η' x) : η = η'
Full source 
@[ext]
theorem ext ⦃η η' : ApplicativeTransformation F G⦄ (h : ∀ (α : Type u) (x : F α), η x = η' x) :
    η = η' := by
  apply coe_inj
  ext1 α
  exact funext (h α)
Extensionality of Applicative Transformations
Informal description
For any two applicative transformations $\eta$ and $\eta'$ from an applicative functor $F$ to an applicative functor $G$, if $\eta$ and $\eta'$ agree on all types $\alpha$ and all elements $x$ of $F \alpha$ (i.e., $\eta x = \eta' x$ for all $x$), then $\eta = \eta'$.
ApplicativeTransformation.preserves_pure theorem
{α} : ∀ x : α, η (pure x) = pure x
Full source 
@[functor_norm]
theorem preserves_pure {α} : ∀ x : α, η (pure x) = pure x :=
  η.preserves_pure'
Preservation of Pure by Applicative Transformation
Informal description
For any applicative transformation $\eta$ between applicative functors $F$ and $G$, and for any element $x$ of type $\alpha$, the transformation preserves the `pure` operation, i.e., $\eta(\text{pure } x) = \text{pure } x$.
ApplicativeTransformation.preserves_seq theorem
{α β : Type u} : ∀ (x : F (α → β)) (y : F α), η (x <*> y) = η x <*> η y
Full source 
@[functor_norm]
theorem preserves_seq {α β : Type u} : ∀ (x : F (α → β)) (y : F α), η (x <*> y) = η x <*> η y :=
  η.preserves_seq'
Preservation of Sequential Application by Applicative Transformation
Informal description
For any applicative transformation $\eta$ between applicative functors $F$ and $G$, and for any types $\alpha$ and $\beta$, the transformation preserves the sequential application operation. Specifically, for any $x : F(\alpha \to \beta)$ and $y : F\alpha$, we have $\eta(x <*> y) = \eta x <*> \eta y$.
ApplicativeTransformation.preserves_map theorem
{α β} (x : α → β) (y : F α) : η (x <$> y) = x <$> η y
Full source 
@[functor_norm]
theorem preserves_map {α β} (x : α → β) (y : F α) : η (x <$> y) = x <$> η y := by
  rw [← pure_seq, η.preserves_seq, preserves_pure, pure_seq]
Preservation of Mapping by Applicative Transformation
Informal description
For any applicative transformation $\eta$ between applicative functors $F$ and $G$, and for any function $f : \alpha \to \beta$ and element $y : F\alpha$, the transformation preserves the mapping operation, i.e., $\eta(f <\$> y) = f <\$> \eta y$.
ApplicativeTransformation.preserves_map' theorem
{α β} (x : α → β) : @η _ ∘ Functor.map x = Functor.map x ∘ @η _
Full source 
theorem preserves_map' {α β} (x : α → β) : @η _ ∘ Functor.map x = Functor.mapFunctor.map x ∘ @η _ := by
  ext y
  exact preserves_map η x y
Naturality of Applicative Transformation with Respect to Mapping
Informal description
For any applicative transformation $\eta$ between applicative functors $F$ and $G$, and for any function $f : \alpha \to \beta$, the transformation commutes with the mapping operation, i.e., $\eta_\beta \circ \text{map}_F f = \text{map}_G f \circ \eta_\alpha$ (where $\eta_\alpha$ denotes the transformation applied at type $\alpha$).
ApplicativeTransformation.idTransformation definition
: ApplicativeTransformation F F
Full source 
/-- The identity applicative transformation from an applicative functor to itself. -/
def idTransformation : ApplicativeTransformation F F where
  app _ := id
  preserves_pure' := by simp
  preserves_seq' x y := by simp
Identity applicative transformation
Informal description
The identity applicative transformation from an applicative functor \( F \) to itself, which maps every element \( x : F \alpha \) to itself, and preserves the `pure` and `<*>` operations.
ApplicativeTransformation.instInhabited instance
: Inhabited (ApplicativeTransformation F F)
Full source 
instance : Inhabited (ApplicativeTransformation F F) :=
  ⟨idTransformation⟩
Existence of Identity Applicative Transformation
Informal description
For any applicative functor $F$, there exists an identity applicative transformation from $F$ to itself.
ApplicativeTransformation.comp definition
(η' : ApplicativeTransformation G H) (η : ApplicativeTransformation F G) : ApplicativeTransformation F H
Full source 
/-- The composition of applicative transformations. -/
def comp (η' : ApplicativeTransformation G H) (η : ApplicativeTransformation F G) :
    ApplicativeTransformation F H where
  app _ x := η' (η x)
  -- Porting note: something has gone wrong with `simp [functor_norm]`,
  -- which should suffice for the next two.
  preserves_pure' x := by simp only [preserves_pure]
  preserves_seq' x y := by simp only [preserves_seq]
Composition of Applicative Transformations
Informal description
The composition of two applicative transformations $\eta' : G \to H$ and $\eta : F \to G$ is an applicative transformation from $F$ to $H$ that applies $\eta$ followed by $\eta'$ to any element $x : F \alpha$. This composition preserves the `pure` and `<*>` operations of the applicative functors.
ApplicativeTransformation.comp_apply theorem
(η' : ApplicativeTransformation G H) (η : ApplicativeTransformation F G) {α : Type u} (x : F α) : η'.comp η x = η' (η x)
Full source 
@[simp]
theorem comp_apply (η' : ApplicativeTransformation G H) (η : ApplicativeTransformation F G)
    {α : Type u} (x : F α) : η'.comp η x = η' (η x) :=
  rfl
Composition of Applicative Transformations Preserves Application
Informal description
For any applicative transformations $\eta : F \to G$ and $\eta' : G \to H$, and for any element $x : F \alpha$, the composition of $\eta'$ and $\eta$ applied to $x$ equals $\eta'$ applied to $\eta$ applied to $x$, i.e., $(\eta' \circ \eta)(x) = \eta'(\eta(x))$.
ApplicativeTransformation.comp_assoc theorem
{I : Type u → Type t} [Applicative I] (η'' : ApplicativeTransformation H I) (η' : ApplicativeTransformation G H) (η : ApplicativeTransformation F G) : (η''.comp η').comp η = η''.comp (η'.comp η)
Full source 
theorem comp_assoc {I : Type u → Type t} [Applicative I]
    (η'' : ApplicativeTransformation H I) (η' : ApplicativeTransformation G H)
    (η : ApplicativeTransformation F G) : (η''.comp η').comp η = η''.comp (η'.comp η) :=
  rfl
Associativity of Applicative Transformation Composition
Informal description
For any applicative functors $F$, $G$, $H$, and $I$, and any applicative transformations $\eta : F \to G$, $\eta' : G \to H$, and $\eta'' : H \to I$, the composition of transformations is associative. That is, $(\eta'' \circ \eta') \circ \eta = \eta'' \circ (\eta' \circ \eta)$.
ApplicativeTransformation.comp_id theorem
(η : ApplicativeTransformation F G) : η.comp idTransformation = η
Full source 
@[simp]
theorem comp_id (η : ApplicativeTransformation F G) : η.comp idTransformation = η :=
  ext fun _ _ => rfl
Right Identity Law for Applicative Transformation Composition
Informal description
For any applicative transformation $\eta$ from an applicative functor $F$ to an applicative functor $G$, the composition of $\eta$ with the identity transformation on $F$ is equal to $\eta$.
ApplicativeTransformation.id_comp theorem
(η : ApplicativeTransformation F G) : idTransformation.comp η = η
Full source 
@[simp]
theorem id_comp (η : ApplicativeTransformation F G) : idTransformation.comp η = η :=
  ext fun _ _ => rfl
Left Identity Law for Applicative Transformation Composition
Informal description
For any applicative transformation $\eta$ from an applicative functor $F$ to an applicative functor $G$, the composition of the identity transformation on $F$ with $\eta$ is equal to $\eta$.
Traversable structure
(t : Type u → Type u) extends Functor t
Full source 
/-- 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 β)`. -/
class Traversable (t : Type u → Type u) extends Functor t where
  /-- The function commuting a traversable functor `t` with an arbitrary applicative functor `m`. -/
  traverse : ∀ {m : Type u → Type u} [Applicative m] {α β}, (α → m β) → t α → m (t β)
Traversable Functor
Informal description
A traversable functor is a functor equipped with a method to commute with all applicative functors. For a traversable functor `t` and an applicative functor `f`, given a function `g : α → f β`, the operation `traverse g` transforms a container `t α` into an effectful computation `f (t β)`, effectively "swapping" the layers of `t` and `f`.
sequence definition
[Traversable t] : t (f α) → f (t α)
Full source 
/-- A traversable functor commutes with all applicative functors. -/
def sequence [Traversable t] : t (f α) → f (t α) :=
  traverse id
Sequence of effectful computations in a traversable functor
Informal description
Given a traversable functor `t` and an applicative functor `f`, the function `sequence` transforms a container `t (f α)` of effectful computations into a single effectful computation `f (t α)` that produces a container of results. This is equivalent to applying `traverse` with the identity function.
LawfulTraversable structure
(t : Type u → Type u) [Traversable t] : Prop extends LawfulFunctor t
Full source 
/-- 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. -/
class LawfulTraversable (t : Type u → Type u) [Traversable t] : Prop extends LawfulFunctor t where
  /-- `traverse` plays well with `pure` of the identity monad -/
  id_traverse : ∀ {α} (x : t α), traverse (pure : α → Id α) x = x
  /-- `traverse` plays well with composition of applicative functors. -/
  comp_traverse :
    ∀ {F G} [Applicative F] [Applicative G] [LawfulApplicative F] [LawfulApplicative G] {α β γ}
      (f : β → F γ) (g : α → G β) (x : t α),
      traverse (Functor.Comp.mkFunctor.Comp.mk ∘ map f ∘ g) x = Comp.mk (map (traverse f) (traverse g x))
  /-- An axiom for `traverse` involving `pure : β → Id β`. -/
  traverse_eq_map_id : ∀ {α β} (f : α → β) (x : t α),
    traverse ((pure : β → Id β) ∘ f) x = id.mk (f <$> x)
  /-- The naturality axiom explaining how lawful traversable functors should play with
  lawful applicative functors. -/
  naturality :
    ∀ {F G} [Applicative F] [Applicative G] [LawfulApplicative F] [LawfulApplicative G]
      (η : ApplicativeTransformation F G) {α β} (f : α → F β) (x : t α),
      η (traverse f x) = traverse (@η _ ∘ f) x
Lawful Traversable Functor
Informal description
A traversable functor `t` is called *lawful* if its `traverse` operation satisfies the following properties: 1. It preserves the identity function: `traverse pure = pure` when applied to the identity monad. 2. It respects the composition of applicative functors: `traverse (f ∘ g) = traverse f ∘ traverse g`. 3. It behaves naturally with respect to applicative transformations. 4. It satisfies the naturality condition: for any applicative transformation `η`, `η ∘ traverse f = traverse (η ∘ f)`.
instTraversableId instance
: Traversable Id
Full source 
instance : Traversable Id :=
  ⟨id⟩
Traversable Identity Functor
Informal description
The identity functor `Id` is traversable. That is, for any applicative functor `f` and function `g : α → f β`, the operation `traverse g` can be applied to a value of type `Id α` to produce a value of type `f (Id β)`.
instLawfulTraversableId instance
: LawfulTraversable Id
Full source 
instance : LawfulTraversable Id where
  id_traverse _ := rfl
  comp_traverse _ _ _ := rfl
  traverse_eq_map_id _ _ := rfl
  naturality _ _ _ _ _ := rfl
Identity Functor is Lawful Traversable
Informal description
The identity functor `Id` satisfies the laws of a traversable functor. Specifically, its `traverse` operation preserves the identity function, respects composition of applicative functors, and behaves naturally with respect to applicative transformations.
instTraversableOption instance
: Traversable Option
Full source 
instance : Traversable Option :=
  ⟨Option.traverse⟩
Traversable Structure on Option Type
Informal description
The option type `Option` is a traversable functor. That is, for any applicative functor `F` and function `f : α → F β`, the operation `traverse f` can be applied to a value of type `Option α` to produce a value of type `F (Option β)`. This operation applies `f` to the contained value (if any) and wraps the result in `Option β` within the applicative context `F`.
instTraversableList instance
: Traversable List
Full source 
instance : Traversable List :=
  ⟨List.traverse⟩
Traversable Structure on Lists
Informal description
The list type constructor is a traversable functor. That is, for any applicative functor $F$ and function $f : \alpha \to F \beta$, the operation $\text{traverse}\, f$ can be applied to a list of type $\text{List}\, \alpha$ to produce a computation of type $F (\text{List}\, \beta)$. This operation applies $f$ to each element of the list and combines the resulting effects using the applicative structure of $F$.
Sum.traverse definition
{α β} (f : α → F β) : σ ⊕ α → F (σ ⊕ β)
Full source 
/-- Defines a `traverse` function on the second component of a sum type.
This is used to give a `Traversable` instance for the functor `σ ⊕ -`. -/
protected def traverse {α β} (f : α → F β) : σ ⊕ α → F (σ ⊕ β)
  | Sum.inl x => pure (Sum.inl x)
  | Sum.inr x => Sum.inr <$> f x
Traversable operation on sum types
Informal description
The function `Sum.traverse` maps a function `f : α → F β` over the second component of a sum type `σ ⊕ α`, where `F` is an applicative functor. Specifically, if the input is `Sum.inl x`, it returns `pure (Sum.inl x)`, and if the input is `Sum.inr x`, it applies `f` to `x` and maps the result to `Sum.inr`.
instTraversableSum instance
{σ : Type u} : Traversable.{u} (Sum σ)
Full source 
instance {σ : Type u} : Traversable.{u} (Sum σ) :=
  ⟨@Sum.traverse _⟩
Traversable Structure on Sum Types
Informal description
For any type $\sigma$, the sum type constructor $\oplus \sigma$ (which maps a type $\alpha$ to $\sigma \oplus \alpha$) is a traversable functor. This means that for any applicative functor $F$ and function $f : \alpha \to F \beta$, there is a natural way to transform a value of type $\sigma \oplus \alpha$ into a computation of type $F (\sigma \oplus \beta)$.