A type for VM-erased data #
This file defines a type Erased α
which is classically isomorphic to α
,
but erased in the VM. That is, at runtime every value of Erased α
is
represented as 0
, just like types and proofs.
Extracts the erased value, noncomputably.
Equations
- Erased.out x = match x with | { fst := fst, snd := h } => Classical.choose h
Extracts the erased value, if it is a type.
Note: (mk a).OutType
is not definitionally equal to a
.
Equations
Extracts the erased value, if it is a proof.
Equivalence between Erased α
and α
.
Equations
- Erased.equiv α = { toFun := Erased.out, invFun := Erased.mk, left_inv := (_ : ∀ (a : Erased α), Erased.mk (Erased.out a) = a), right_inv := (_ : ∀ (a : α), Erased.out (Erased.mk a) = a) }
Equations
- Erased.instReprErased α = { reprPrec := fun x x => Std.Format.text "Erased" }
Equations
- Erased.instToStringErased α = { toString := fun x => "Erased" }
Computably produce an erased value from a proof of nonemptiness.
Equations
Equations
- Erased.instInhabitedErased = { default := Erased.choice h }
(>>=)
operation on Erased
.
This is a separate definition because α
and β
can live in different
universes (the universe is fixed in Monad
).
Equations
- Erased.bind a f = { fst := fun b => PSigma.fst (f (Erased.out a)) b, snd := (_ : ∃ a, (fun b => a = b) = (f (Erased.out a)).fst) }
Collapses two levels of erasure.
Equations
- Erased.join a = Erased.bind a id
(<$>)
operation on Erased
.
This is a separate definition because α
and β
can live in different
universes (the universe is fixed in Functor
).
Equations
- Erased.map f a = Erased.bind a (Erased.mk ∘ f)