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 α × β.

Equations

• Prod.bitraverse f f' (x_1, y) = Prod.mk <$> f x_1 <*> f' y

instance instBitraversableProd : Bitraversable Prod

Equations

• instBitraversableProd = Bitraversable.mk @Prod.bitraverse

instance instLawfulBitraversableProd : LawfulBitraversable Prod

Equations

• instLawfulBitraversableProd = ⋯

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 α ⊕ β.

Equations

• Sum.bitraverse f f' (Sum.inl x_1) = Sum.inl <$> f x_1
• Sum.bitraverse f f' (Sum.inr x_1) = Sum.inr <$> f' x_1

instance instBitraversableSum : Bitraversable Sum

Equations

• instBitraversableSum = Bitraversable.mk @Sum.bitraverse

instance instLawfulBitraversableSum : LawfulBitraversable Sum

Equations

• instLawfulBitraversableSum = ⋯

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.

Equations

• Const.bitraverse f f' = f

instance Bitraversable.const : Bitraversable Functor.Const

Equations

• Bitraversable.const = Bitraversable.mk @Const.bitraverse

instance LawfulBitraversable.const : LawfulBitraversable Functor.Const

Equations

• LawfulBitraversable.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.

Equations

• flip.bitraverse f f' = bitraverse f' f

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

Equations

• Bitraversable.flip = Bitraversable.mk (@flip.bitraverse t inst)

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

Equations

• ⋯ = ⋯

@[instance 10]

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

Equations

• Bitraversable.traversable = Traversable.mk (@Bitraversable.tsnd t inst α)

@[instance 10]

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

Equations

• ⋯ = ⋯

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.

Equations

• Bicompl.bitraverse F G f f' = bitraverse (traverse f) (traverse f')

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

Equations

• instBitraversableBicompl F G = Bitraversable.mk (@Bicompl.bitraverse t inst✝¹ F G inst✝ inst)

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

Equations

• ⋯ = ⋯

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.

Equations

• Bicompr.bitraverse F f f' = traverse (bitraverse f f')

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

Equations

• instBitraversableBicompr F = Bitraversable.mk (@Bicompr.bitraverse t inst✝ F inst)

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)

Equations

• ⋯ = ⋯