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_reducible]

instance instBitraversableProd : Bitraversable Prod

Equations

• instBitraversableProd = { toBifunctor := Prod.bifunctor, bitraverse := @Prod.bitraverse }

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

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_reducible]

instance instBitraversableSum : Bitraversable Sum

Equations

• instBitraversableSum = { toBifunctor := Sum.bifunctor, bitraverse := @Sum.bitraverse }

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.

Equations

• Const.bitraverse f f' = f

@[instance_reducible]

instance Bitraversable.const : Bitraversable Functor.Const

Equations

• Bitraversable.const = { toBifunctor := Bifunctor.const, bitraverse := @Const.bitraverse }

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.

Equations

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

@[instance_reducible]

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

Equations

• Bitraversable.flip = { toBifunctor := Bifunctor.flip, bitraverse := @flip.bitraverse t inst✝ }

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

@[instance_reducible, instance 10]

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

Equations

• Bitraversable.traversable = { toFunctor := Bifunctor.functor, traverse := @Bitraversable.tsnd t inst✝ α }

@[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.

Equations

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

@[instance_reducible]

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)

Equations

• instBitraversableBicompl F G = { toBifunctor := Function.bicompl.bifunctor F G, bitraverse := @Bicompl.bitraverse t inst✝² F G inst✝¹ inst✝ }

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.

Equations

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

@[instance_reducible]

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 = { toBifunctor := Function.bicompr.bifunctor F, bitraverse := @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)