structure Data.Proxy (α : Type u) : Type

The proxy type $\text{Proxy}(\alpha)$ carries a phantom type parameter $\alpha$ but contains no data. It is the terminal object in the category of types: every type has exactly one function into $\text{Proxy}(\alpha)$.

$$\text{Proxy} : \text{Type}\; u \to \text{Type}$$

def Data.instInhabitedProxy.default {a✝ : Type u_1} : Proxy a✝

Equations

• Data.instInhabitedProxy.default = { }

@[implicit_reducible]

instance Data.instInhabitedProxy {a✝ : Type u_1} : Inhabited (Proxy a✝)

Equations

• Data.instInhabitedProxy = { default := Data.instInhabitedProxy.default }

@[implicit_reducible]

instance Data.Proxy.instBEq {α : Type u_1} : BEq (Proxy α)

BEq instance for $\text{Proxy}(\alpha)$ — always true since there is only one value.

Equations

• Data.Proxy.instBEq = { beq := fun (x x_1 : Data.Proxy α) => true }

@[implicit_reducible]

instance Data.Proxy.instOrd {α : Type u_1} : Ord (Proxy α)

Ord instance for $\text{Proxy}(\alpha)$ — always Ordering.eq since all values are equal.

Equations

• Data.Proxy.instOrd = { compare := fun (x x_1 : Data.Proxy α) => Ordering.eq }

@[implicit_reducible]

instance Data.Proxy.instRepr {α : Type u_1} : Repr (Proxy α)

Repr instance for $\text{Proxy}(\alpha)$, displaying as Proxy.mk.

Equations

• Data.Proxy.instRepr = { reprPrec := fun (x : Data.Proxy α) (x_1 : Nat) => Std.Format.text "Proxy.mk" }

@[implicit_reducible]

instance Data.Proxy.instHashable {α : Type u_1} : Hashable (Proxy α)

Hashable instance for $\text{Proxy}(\alpha)$ — always hashes to $0$.

Equations

• Data.Proxy.instHashable = { hash := fun (x : Data.Proxy α) => 0 }

@[implicit_reducible]

instance Data.Proxy.instToString {α : Type u_1} : ToString (Proxy α)

ToString instance for $\text{Proxy}(\alpha)$.

Equations

• Data.Proxy.instToString = { toString := fun (x : Data.Proxy α) => "Proxy" }

@[implicit_reducible]

instance Data.Proxy.instFunctor : Functor Proxy

Functor instance for $\text{Proxy}$. Since $\text{Proxy}$ carries no data, map is the identity on the structure:

$$\text{map}\; f\; \text{Proxy.mk} = \text{Proxy.mk}$$

Equations

• Data.Proxy.instFunctor = { map := fun {α β : Type ?u.13} (x : α → β) (x_1 : Data.Proxy α) => { } }

@[implicit_reducible]

instance Data.Proxy.instPure : Pure Proxy

Pure instance for $\text{Proxy}$:

$$\text{pure}\; a = \text{Proxy.mk}$$

Equations

• Data.Proxy.instPure = { pure := fun {α : Type ?u.6} (x : α) => { } }

@[implicit_reducible]

instance Data.Proxy.instBind : Bind Proxy

Bind instance for $\text{Proxy}$:

$$\text{bind}\; \text{Proxy.mk}\; f = \text{Proxy.mk}$$

Equations

• Data.Proxy.instBind = { bind := fun {α β : Type ?u.9} (x : Data.Proxy α) (x_1 : α → Data.Proxy β) => { } }

@[implicit_reducible]

instance Data.Proxy.instSeq : Seq Proxy

Seq instance for $\text{Proxy}$:

$$\text{seq}\; \text{Proxy.mk}\; f = \text{Proxy.mk}$$

Equations

• Data.Proxy.instSeq = { seq := fun {α β : Type ?u.10} (x : Data.Proxy (α → β)) (x_1 : Unit → Data.Proxy α) => { } }

@[implicit_reducible]

instance Data.Proxy.instSeqLeft : SeqLeft Proxy

SeqLeft instance for $\text{Proxy}$.

Equations

• Data.Proxy.instSeqLeft = { seqLeft := fun {α β : Type ?u.9} (x : Data.Proxy α) (x_1 : Unit → Data.Proxy β) => { } }

@[implicit_reducible]

instance Data.Proxy.instSeqRight : SeqRight Proxy

SeqRight instance for $\text{Proxy}$.

Equations

• Data.Proxy.instSeqRight = { seqRight := fun {α β : Type ?u.9} (x : Data.Proxy α) (x_1 : Unit → Data.Proxy β) => { } }

@[implicit_reducible]

instance Data.Proxy.instApplicative : Applicative Proxy

Applicative instance for $\text{Proxy}$.

Equations

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

@[implicit_reducible]

instance Data.Proxy.instMonad : Monad Proxy

Monad instance for $\text{Proxy}$.

Equations

• Data.Proxy.instMonad = { toApplicative := Data.Proxy.instApplicative, toBind := Data.Proxy.instBind }

theorem Data.Proxy.map_id {α : Type u_1} (p : Proxy α) : id <$> p = p

Functor identity law: $\text{map}\;\text{id} = \text{id}$.

$$\text{map}\;\text{id}\;(\text{Proxy.mk}) = \text{Proxy.mk}$$

theorem Data.Proxy.map_comp {β γ α : Type u_1} (f : β → γ) (g : α → β) (p : Proxy α) : (f ∘ g) <$> p = f <$> g <$> p

Functor composition law: $\text{map}\;(f \circ g) = \text{map}\;f \circ \text{map}\;g$.

$$\text{map}\;(f \circ g)\;\text{Proxy.mk} = \text{map}\;f\;(\text{map}\;g\;\text{Proxy.mk})$$

theorem Data.Proxy.pure_bind {α β : Type u_1} (a : α) (f : α → Proxy β) : pure a >>= f = f a

Left identity (pure/bind): $\text{bind}\;(\text{pure}\;a)\;f = f\;a$.

For $\text{Proxy}$, both sides reduce to $\text{Proxy.mk}$.

theorem Data.Proxy.bind_pure {α : Type u_1} (p : Proxy α) : p >>= pure = p

Right identity (bind/pure): $\text{bind}\;m\;\text{pure} = m$.

$$\text{bind}\;\text{Proxy.mk}\;\text{pure} = \text{Proxy.mk}$$

theorem Data.Proxy.bind_assoc {α β γ : Type u_1} (p : Proxy α) (f : α → Proxy β) (g : β → Proxy γ) : p >>= f >>= g = p >>= fun (x : α) => f x >>= g

Associativity: $\text{bind}\;(\text{bind}\;m\;f)\;g = \text{bind}\;m\;(\lambda x.\;\text{bind}\;(f\;x)\;g)$.

For $\text{Proxy}$, all sides reduce to $\text{Proxy.mk}$.