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 instLawfulBitraversableProdInstBitraversableProd : 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 instLawfulBitraversableSumInstBitraversableSum : 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} {α' : Type u} {β : Type u} {β' : 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 (flip t)

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

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

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 : Type u → Type u) (G : Type u → Type u) [Traversable F] [Traversable G] {m : Type u → Type u} [Applicative m] {α : Type u} {β : Type u} {α' : Type u} {β' : Type u} (f : α → m β) (f' : α' → m β') : Function.bicompl t F G α α' → m (Function.bicompl t F G β β')

The bitraverse function for bicompl.

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

instance instLawfulBitraversableBicomplTypeInstBitraversableBicomplType {t : Type u → Type u → Type u} [Bitraversable t] (F : Type u → Type u) (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} {β : Type u} {α' : Type u} {β' : Type u} (f : α → m β) (f' : α' → m β') : Function.bicompr F t α α' → m (Function.bicompr F t β β')

The bitraverse function for bicompr.

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

instance instLawfulBitraversableBicomprTypeInstBitraversableBicomprType {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)