Bitraversable instances

This file provides Bitraversable instances for concrete bifunctors:

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

References

• Hackage:

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 = match x with | (x, y) => Seq.seq (Prod.mk <$> f x) fun (x : Unit) => f' y

instance instBitraversableProd : Bitraversable Prod

Equations

• instBitraversableProd = Bitraversable.mk @Prod.bitraverse

instance instLawfulBitraversableProdInstBitraversableProd : LawfulBitraversable Prod

Equations

• instLawfulBitraversableProdInstBitraversableProd = ⋯

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' x = match x with | Sum.inl x => Sum.inl <$> f x | Sum.inr x => Sum.inr <$> f' x

instance instBitraversableSum : Bitraversable Sum

Equations

• instBitraversableSum = Bitraversable.mk @Sum.bitraverse

instance instLawfulBitraversableSumInstBitraversableSum : LawfulBitraversable Sum

Equations

• instLawfulBitraversableSumInstBitraversableSum = ⋯

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 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 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 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)

Equations

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

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)

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 instBitraversableBicomprType {t : Type u → Type u → Type u} [Bitraversable t] (F : Type u → Type u) [Traversable F] : Bitraversable (Function.bicompr F t)

Equations

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

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)

Equations

• ⋯ = ⋯