Bitraversable type class
Type class for traversing bifunctors. The concepts and laws are taken from https://hackage.haskell.org/package/base-4.12.0.0/docs/Data-Bitraversable.html
Simple examples of bitraversable are prod and sum. A more elaborate example is
to define an a-list as:
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 - exposes the
bitraversefunction - is_lawful_bitraversable - laws similar to is_lawful_traversable
Tags
traversable bitraversable iterator functor bifunctor applicative
@[class]
- to_bifunctor : bifunctor t
- bitraverse : Π {m : Type ? → Type ?} [_inst_1 : applicative m] {α α' β β' : Type ?}, (α → 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} :
t (m α) (m β) → m (t α β)
Equations
@[class]
- to_is_lawful_bifunctor : is_lawful_bifunctor t
- id_bitraverse : ∀ {α β : Type ?} (x : t α β), bitraversable.bitraverse id.mk id.mk x = id.mk x
- comp_bitraverse : ∀ {F G : Type ? → Type ?} [_inst_1_1 : applicative F] [_inst_2 : applicative G] [_inst_3 : is_lawful_applicative F] [_inst_4 : is_lawful_applicative G] {α α' β β' γ γ' : Type ?} (f : β → F γ) (f' : β' → F γ') (g : α → G β) (g' : α' → G β') (x : t α α'), bitraversable.bitraverse (functor.comp.mk ∘ functor.map f ∘ g) (functor.comp.mk ∘ functor.map f' ∘ g') x = functor.comp.mk (bitraversable.bitraverse f f' <$> bitraversable.bitraverse g g' x)
- bitraverse_eq_bimap_id : ∀ {α α' β β' : Type ?} (f : α → β) (f' : α' → β') (x : t α α'), bitraversable.bitraverse (id.mk ∘ f) (id.mk ∘ f') x = id.mk (bifunctor.bimap f f' x)
- binaturality : ∀ {F G : Type ? → Type ?} [_inst_1_1 : applicative F] [_inst_2 : applicative G] [_inst_3 : is_lawful_applicative F] [_inst_4 : is_lawful_applicative G] (η : applicative_transformation F G) {α α' β β' : Type ?} (f : α → F β) (f' : α' → F β') (x : t α α'), ⇑η (bitraversable.bitraverse f f' x) = bitraversable.bitraverse (⇑η ∘ f) (⇑η ∘ f') x