structure Data.Functor.Const (α : Type u) (β : Type v) : Type u

The constant functor $\text{Const}\;\alpha\;\beta$: carries a value of type $\alpha$, with a phantom type parameter $\beta$.

$$\text{Const}\;\alpha\;\beta \;\cong\; \alpha$$

As a functor in $\beta$, mapping is a no-op (the $\beta$ is phantom). As an applicative (when $\alpha$ has Append), <*> accumulates the $\alpha$ values. This makes Const the key ingredient for implementing foldMap via traverse.

• getConst : α

  Extract the wrapped value.

@[implicit_reducible]

instance Data.Functor.Const.instBEq {α : Type u_1} {β : Type u_2} [BEq α] : BEq (Const α β)

BEq instance for Const α β: compares the underlying $\alpha$ values, ignoring the phantom $\beta$.

Equations

• Data.Functor.Const.instBEq = { beq := fun (a b : Data.Functor.Const α β) => a.getConst == b.getConst }

@[implicit_reducible]

instance Data.Functor.Const.instOrd {α : Type u_1} {β : Type u_2} [Ord α] : Ord (Const α β)

Ord instance for Const α β: orders by the underlying $\alpha$ values.

Equations

• Data.Functor.Const.instOrd = { compare := fun (a b : Data.Functor.Const α β) => compare a.getConst b.getConst }

@[implicit_reducible]

instance Data.Functor.Const.instRepr {α : Type u_1} {β : Type u_2} [Repr α] : Repr (Const α β)

Repr instance for Const α β: delegates to the underlying $\alpha$ representation.

Equations

• Data.Functor.Const.instRepr = { reprPrec := fun (c : Data.Functor.Const α β) (p : Nat) => reprPrec c.getConst p }

@[implicit_reducible]

instance Data.Functor.Const.instToString {α : Type u_1} {β : Type u_2} [ToString α] : ToString (Const α β)

ToString instance for Const α β: delegates to ToString α.

Equations

• Data.Functor.Const.instToString = { toString := fun (c : Data.Functor.Const α β) => toString c.getConst }

@[implicit_reducible]

instance Data.Functor.Const.instFunctor {α : Type u_1} : Functor (Const α)

Functor instance for Const α: mapping over the phantom parameter is a no-op.

$$\text{fmap}\;f\;(\text{Const}\;a) = \text{Const}\;a$$

The function $f : \beta \to \gamma$ is discarded since no $\beta$ value exists to apply it to.

Equations

• Data.Functor.Const.instFunctor = { map := fun {α_1 β : Type ?u.18} (x : α_1 → β) (c : Data.Functor.Const α α_1) => { getConst := c.getConst } }

theorem Data.Functor.Const.map_val {β γ : Type u_1} {α : Type u_2} (f : β → γ) (c : Const α β) : (f <$> c).getConst = c.getConst

Mapping preserves the underlying value: $(\text{fmap}\;f\;c).\text{getConst} = c.\text{getConst}$.

theorem Data.Functor.Const.map_id {α : Type u_1} {β : Type u_2} (c : Const α β) : id <$> c = c

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

theorem Data.Functor.Const.map_comp {γ δ β : Type u_1} {α : Type u_2} (f : γ → δ) (g : β → γ) (c : Const α β) : (f ∘ g) <$> c = f <$> g <$> c

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

@[implicit_reducible]

instance Data.Functor.Const.instPureOfAppendOfInhabited {α : Type u_1} [Append α] [Inhabited α] : Pure (Const α)

Pure instance for Const α (requires Append α and Inhabited α): $\text{pure}\;\_= \text{Const}(\text{default})$.

The value is the monoidal identity (default), since pure should be the identity element for applicative combination.

Equations

• Data.Functor.Const.instPureOfAppendOfInhabited = { pure := fun {α_1 : Type ?u.19} (x : α_1) => { getConst := default } }