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

• Bitraversable: Bare typeclass to hold the Bitraverse function.
• LawfulBitraversable: Typeclass for the laws of the Bitraverse function. Similar to LawfulTraversable.

References

The concepts and laws are taken from https://hackage.haskell.org/package/base-4.12.0.0/docs/Data-Bitraversable.html

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 α' β')

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

• bisequence = bitraverse id id

class LawfulBitraversable (t : Type u → Type u → Type u) [Bitraversable t] extends LawfulBifunctor : Prop

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

• id_bimap : ∀ {α β : Type u} (x : t α β), bimap id id x = x
• bimap_bimap : ∀ {α₀ α₁ α₂ β₀ β₁ β₂ : Type u} (f : α₀ → α₁) (f' : α₁ → α₂) (g : β₀ → β₁) (g' : β₁ → β₂) (x : t α₀ β₀), bimap f' g' (bimap f g x) = bimap (f' ∘ f) (g' ∘ g) x
• id_bitraverse : ∀ {α β : Type u} (x : t α β), bitraverse pure pure x = pure x
• comp_bitraverse : ∀ {F G : Type u → Type u} [inst : Applicative F] [inst_1 : Applicative G] [inst_2 : LawfulApplicative F] [inst_3 : LawfulApplicative G] {α α' β β' γ γ' : 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)
• bitraverse_eq_bimap_id : ∀ {α α' β β' : Type u} (f : α → β) (f' : α' → β') (x : t α α'), bitraverse (pure ∘ f) (pure ∘ f') x = pure (bimap f f' x)
• binaturality : ∀ {F G : Type u → Type u} [inst : Applicative F] [inst_1 : Applicative G] [inst_2 : LawfulApplicative F] [inst_3 : LawfulApplicative G] (η : ApplicativeTransformation F G) {α α' β β' : 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.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'