Documentation

Mathlib.Control.Bitraversable.Basic

Bitraversable type class #

Type class for traversing bifunctors.

Simple examples of Bitraversable are Prod and Sum. A more elaborate example is to define an a-list as:

def AList (key val : Type) := List (key × val)

Then we can use f : key → IO key' and g : val → IO val' to manipulate the AList's key and value respectively with Bitraverse f g : AList key val → IO (AList key' val').

Main definitions #

References #

The concepts and laws are taken from

Tags #

traversable bitraversable iterator functor bifunctor applicative

class Bitraversable (t : Type u → Type u → Type u) extends Bifunctor :
Type (u + 1)

Lawless bitraversable bifunctor. This only holds data for the bimap and bitraverse.

  • bimap : {α α' β β' : Type u} → (αα')(ββ')t α βt α' β'
  • bitraverse : {m : Type u → Type u} → [inst : Applicative m] → {α α' β β' : Type u} → (αm α')(βm β')t α βm (t α' β')
Instances
    def bisequence {t : Type u_1 → Type u_1 → Type u_1} {m : Type u_1 → Type u_1} [Bitraversable t] [Applicative m] {α : Type u_1} {β : Type u_1} :
    t (m α) (m β)m (t α β)

    A bitraversable functor commutes with all applicative functors.

    Equations
    Instances For
      class LawfulBitraversable (t : Type u → Type u → Type u) [Bitraversable t] extends LawfulBifunctor :

      Bifunctor. This typeclass asserts that a lawless bitraversable bifunctor is lawful.

      Instances
        theorem LawfulBitraversable.id_bitraverse {t : Type u → Type u → Type u} [Bitraversable t] [self : LawfulBitraversable t] {α : Type u} {β : Type u} (x : t α β) :
        bitraverse pure pure x = pure x
        theorem LawfulBitraversable.comp_bitraverse {t : Type u → Type u → Type u} [Bitraversable t] [self : LawfulBitraversable t] {F : Type u → Type u} {G : Type u → Type u} [Applicative F] [Applicative G] [LawfulApplicative F] [LawfulApplicative G] {α : Type u} {α' : Type u} {β : Type u} {β' : Type u} {γ : Type u} {γ' : Type u} (f : βF γ) (f' : β'F γ') (g : αG β) (g' : α'G β') (x : t α α') :
        bitraverse (Functor.Comp.mk Functor.map f g) (Functor.Comp.mk Functor.map f' g') x = Functor.Comp.mk (bitraverse f f' <$> bitraverse g g' x)
        theorem LawfulBitraversable.bitraverse_eq_bimap_id {t : Type u → Type u → Type u} [Bitraversable t] [self : LawfulBitraversable t] {α : Type u} {α' : Type u} {β : Type u} {β' : Type u} (f : αβ) (f' : α'β') (x : t α α') :
        bitraverse (pure f) (pure f') x = pure (bimap f f' x)
        theorem LawfulBitraversable.binaturality {t : Type u → Type u → Type u} [Bitraversable t] [self : LawfulBitraversable t] {F : Type u → Type u} {G : Type u → Type u} [Applicative F] [Applicative G] [LawfulApplicative F] [LawfulApplicative G] (η : ApplicativeTransformation F G) {α : Type u} {α' : Type u} {β : Type u} {β' : Type u} (f : αF β) (f' : α'F β') (x : t α α') :
        (fun {α : Type u} => η.app α) (bitraverse f f' x) = bitraverse ((fun {α : Type u} => η.app α) f) ((fun {α : Type u} => η.app α) f') x
        theorem LawfulBitraversable.bitraverse_id_id {t : Type u → Type u → Type u} [Bitraversable t] [self : LawfulBitraversable t] {α : Type u} {β : Type u} :
        bitraverse pure pure = pure
        theorem LawfulBitraversable.bitraverse_comp {t : Type u → Type u → Type u} [Bitraversable t] [self : LawfulBitraversable t] {F : Type u → Type u} {G : Type u → Type u} [Applicative F] [Applicative G] [LawfulApplicative F] [LawfulApplicative G] {α : Type u} {α' : Type u} {β : Type u} {β' : Type u} {γ : Type u} {γ' : Type u} (f : βF γ) (f' : β'F γ') (g : αG β) (g' : α'G β') :
        bitraverse (Functor.Comp.mk Functor.map f g) (Functor.Comp.mk Functor.map f' g') = Functor.Comp.mk Functor.map (bitraverse f f') bitraverse g g'
        theorem LawfulBitraversable.binaturality' {t : Type u → Type u → Type u} [Bitraversable t] [self : LawfulBitraversable t] {F : Type u → Type u} {G : Type u → Type u} [Applicative F] [Applicative G] [LawfulApplicative F] [LawfulApplicative G] (η : ApplicativeTransformation F G) {α : Type u} {α' : Type u} {β : Type u} {β' : Type u} (f : αF β) (f' : α'F β') :
        (fun {α : Type u} => η.app α) bitraverse f f' = bitraverse ((fun {α : Type u} => η.app α) f) ((fun {α : Type u} => η.app α) f')
        theorem LawfulBitraversable.bitraverse_eq_bimap_id' {t : Type u → Type u → Type u} [Bitraversable t] [self : LawfulBitraversable t] {α : Type u} {α' : Type u} {β : Type u} {β' : Type u} (f : αβ) (f' : α'β') :
        bitraverse (pure f) (pure f') = pure bimap f f'