structure Data.Functor.Compose (F : Type u → Type v) (G : Type w → Type u) (α : Type w) : Type v

Functor/applicative composition: $(\text{Compose}\;F\;G)\;\alpha = F\,(G\;\alpha)$.

This witnesses the classical result that the composition of two functors is a functor, and the composition of two applicatives is an applicative.

Use cases:

• Combining effects: Compose IO Option α represents an IO action that may fail
• Nested mapping: map f on Compose F G maps through both layers

• getCompose : F (G α)

  Unwrap the composed value: $F\,(G\;\alpha)$.

@[implicit_reducible]

instance Data.Functor.Compose.instFunctor {F : Type u_1 → Type u_2} {G : Type u_3 → Type u_1} [Functor F] [Functor G] : Functor (Compose F G)

Functor instance for Compose F G: maps through both layers.

$$\text{fmap}\;f\;(\text{Compose}\;x) = \text{Compose}\;(\text{fmap}\;(\text{fmap}\;f)\;x)$$

Equations

• Data.Functor.Compose.instFunctor = { map := fun {α β : Type ?u.34} (f : α → β) (c : Data.Functor.Compose F G α) => { getCompose := (fun (x : G α) => f <$> x) <$> c.getCompose } }

theorem Data.Functor.Compose.map_id {F : Type u_1 → Type u_2} {G : Type u_3 → Type u_1} {α : Type u_3} [Functor F] [Functor G] [LawfulFunctor F] [LawfulFunctor G] (x : Compose F G α) : id <$> x = x

Identity law for composed functors: $\text{fmap}\;\text{id} = \text{id}$.

If $F$ and $G$ are both lawful functors, their composition is also lawful.

theorem Data.Functor.Compose.map_comp {F : Type u_1 → Type u_2} {G : Type u_3 → Type u_1} {β γ α : Type u_3} [Functor F] [Functor G] [LawfulFunctor F] [LawfulFunctor G] (f : β → γ) (g : α → β) (x : Compose F G α) : (f ∘ g) <$> x = f <$> g <$> x

Composition law for composed functors: $\text{fmap}\;(f \circ g) = \text{fmap}\;f \circ \text{fmap}\;g$.

Follows from the composition laws of $F$ and $G$ individually.

@[implicit_reducible]

instance Data.Functor.Compose.instPureOfApplicative {F : Type u_1 → Type u_2} {G : Type u_3 → Type u_1} [Applicative F] [Applicative G] : Pure (Compose F G)

Pure instance for Compose F G: wraps a value in both layers.

$$\text{pure}\;a = \text{Compose}\;(\text{pure}\;(\text{pure}\;a))$$

Equations

• Data.Functor.Compose.instPureOfApplicative = { pure := fun {α : Type ?u.26} (a : α) => { getCompose := pure (pure a) } }

@[implicit_reducible]

instance Data.Functor.Compose.instSeqOfApplicative {F : Type u_1 → Type u_2} {G : Type u_3 → Type u_1} [Applicative F] [Applicative G] : Seq (Compose F G)

Seq instance for Compose F G: applies through both layers using the applicative structure of $F$ and $G$.

$$\text{Compose}\;f \mathbin{<*>} \text{Compose}\;x = \text{Compose}\;((\mathbin{<*>}) \mathbin{<\$>} f \mathbin{<*>} x)$$

Equations

• One or more equations did not get rendered due to their size.

@[implicit_reducible]

instance Data.Functor.Compose.instApplicative {F : Type u_1 → Type u_2} {G : Type u_3 → Type u_1} [Applicative F] [Applicative G] : Applicative (Compose F G)

Applicative instance for Compose F G: the composition of two applicatives is an applicative.

Equations

• One or more equations did not get rendered due to their size.