Bitraversable instances

This file provides Bitraversable instances for concrete bifunctors:

• Prod
• Sum
• Functor.Const
• flip
• Function.bicompl
• Function.bicompr

References

• Hackage: https://hackage.haskell.org/package/base-4.12.0.0/docs/Data-Bitraversable.html

Tags

traversable bitraversable functor bifunctor applicative

def Prod.bitraverse {F : Type u → Type u} [Applicative F] {α : Type u_1} {α' : Type u} {β : Type u_2} {β' : Type u} (f : α → F α') (f' : β → F β') : α × β → F (α' × β')

The bitraverse function for α × β.

instance instBitraversableProd : Bitraversable Prod

instance instLawfulBitraversableProd : LawfulBitraversable Prod

def Sum.bitraverse {F : Type u → Type u} [Applicative F] {α : Type u_1} {α' : Type u} {β : Type u_2} {β' : Type u} (f : α → F α') (f' : β → F β') : α ⊕ β → F (α' ⊕ β')

The bitraverse function for α ⊕ β.

instance instBitraversableSum : Bitraversable Sum

instance instLawfulBitraversableSum : LawfulBitraversable Sum

def Const.bitraverse {F : Type u → Type u} [Applicative F] {α : Type u_1} {α' : Type u} {β : Type u_2} {β' : Type u} (f : α → F α') (f' : β → F β') : Functor.Const α β → F (Functor.Const α' β')

The bitraverse function for Const. It throws away the second map.

instance Bitraversable.const : Bitraversable Functor.Const

instance LawfulBitraversable.const : LawfulBitraversable Functor.Const

def flip.bitraverse {t : Type u → Type u → Type u} [Bitraversable t] {F : Type u → Type u} [Applicative F] {α α' β β' : Type u} (f : α → F α') (f' : β → F β') : flip t α β → F (flip t α' β')

The bitraverse function for flip.

instance Bitraversable.flip {t : Type u → Type u → Type u} [Bitraversable t] : Bitraversable (_root_.flip t)

instance LawfulBitraversable.flip {t : Type u → Type u → Type u} [Bitraversable t] [LawfulBitraversable t] : LawfulBitraversable (_root_.flip t)

@[instance 10]

instance Bitraversable.traversable {t : Type u → Type u → Type u} [Bitraversable t] {α : Type u} : Traversable (t α)

@[instance 10]

instance Bitraversable.isLawfulTraversable {t : Type u → Type u → Type u} [Bitraversable t] [LawfulBitraversable t] {α : Type u} : LawfulTraversable (t α)

def Bicompl.bitraverse {t : Type u → Type u → Type u} [Bitraversable t] (F G : Type u → Type u) [Traversable F] [Traversable G] {m : Type u → Type u} [Applicative m] {α β α' β' : Type u} (f : α → m β) (f' : α' → m β') : Function.bicompl t F G α α' → m (Function.bicompl t F G β β')

The bitraverse function for bicompl.

instance instBitraversableBicompl {t : Type u → Type u → Type u} [Bitraversable t] (F G : Type u → Type u) [Traversable F] [Traversable G] : Bitraversable (Function.bicompl t F G)

instance instLawfulBitraversableBicomplOfLawfulTraversable {t : Type u → Type u → Type u} [Bitraversable t] (F G : Type u → Type u) [Traversable F] [Traversable G] [LawfulTraversable F] [LawfulTraversable G] [LawfulBitraversable t] : LawfulBitraversable (Function.bicompl t F G)

def Bicompr.bitraverse {t : Type u → Type u → Type u} [Bitraversable t] (F : Type u → Type u) [Traversable F] {m : Type u → Type u} [Applicative m] {α β α' β' : Type u} (f : α → m β) (f' : α' → m β') : Function.bicompr F t α α' → m (Function.bicompr F t β β')

The bitraverse function for bicompr.

instance instBitraversableBicompr {t : Type u → Type u → Type u} [Bitraversable t] (F : Type u → Type u) [Traversable F] : Bitraversable (Function.bicompr F t)

instance instLawfulBitraversableBicomprOfLawfulTraversable {t : Type u → Type u → Type u} [Bitraversable t] (F : Type u → Type u) [Traversable F] [LawfulTraversable F] [LawfulBitraversable t] : LawfulBitraversable (Function.bicompr F t)