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 theBitraverse
function.LawfulBitraversable
: Typeclass for the laws of theBitraverse
function. Similar toLawfulTraversable
.
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
- bimap : {α α' β β' : Type u} → (α → α') → (β → β') → t α β → t α' β'
- bitraverse : {m : Type u → Type u} → [inst : Applicative m] → {α α' β β' : Type u} → (α → m α') → (β → m β') → t α β → m (t α' β')
Lawless bitraversable bifunctor. This only holds data for the bimap and bitraverse.
Instances
A bitraversable functor commutes with all applicative functors.
Instances For
- 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)
- 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 {α} => ApplicativeTransformation.app η α) (bitraverse f f' x) = bitraverse ((fun {α} => ApplicativeTransformation.app η α) ∘ f) ((fun {α} => ApplicativeTransformation.app η α) ∘ f') x
Bifunctor. This typeclass asserts that a lawless bitraversable bifunctor is lawful.