## Stream: general

### Topic: erased

#### Mario Carneiro (Apr 05 2018 at 17:56):

@Gabriel Ebner What would be the best way to define the following type:

• erased A is a type with a computable function A -> erased A and a noncomputable function erased A -> A
• A and erased A are (noncomputably) equivalent with those functions
• erased A is VM-erased, meaning elements of this type are stored as the "proof object" / "neutral element"

#### Mario Carneiro (Apr 05 2018 at 17:56):

Attempt 1:

import data.set.basic data.equiv

def erased (α : Type*) : Type* := set.range (singleton : α → set α)

namespace erased

@[inline] def mk {α} (a : α) : erased α := ⟨_, a, rfl⟩

noncomputable def out {α} (a : erased α) : α :=
classical.some a.2

theorem mk_out {α} (a : α) : (mk a).out = a :=
eq.symm $set.mem_singleton_iff.1$
by unfold out; rw [classical.some_spec (mk a).2]; simp [mk]

theorem out_mk {α} (a : erased α) : mk (out a) = a :=
subtype.eq $set.ext$ λ b,
by simp [out, mk, classical.some_spec a.2]

noncomputable def equiv (α) : erased α ≃ α :=
⟨out, mk, out_mk, mk_out⟩

end erased


#### Mario Carneiro (Apr 05 2018 at 18:05):

The problem with this encoding is that erased A is essentially a set A, which is a A -> Prop, which is stored as a closure returning a proof object. Thus it isn't fully erased, so it still causes its arguments to be evaluated:

#eval erased.mk (2+2) -- (erased.mk 4)


Do you know why type families aren't erased like types are?

#### Simon Hudon (Apr 05 2018 at 18:06):

Why not use nonempty?

#### Mario Carneiro (Apr 05 2018 at 18:07):

it's not noncomputably equivalent to A

#### Simon Hudon (Apr 05 2018 at 18:07):

I withdraw my question, I get it

#### Mario Carneiro (Apr 05 2018 at 18:08):

The goal is to have a piece of "data" that is actually erased but still exists from the lean modeling POV

I see

#### Gabriel Ebner (Apr 05 2018 at 18:10):

Wait, this no longer works? Let me check.

#### Gabriel Ebner (Apr 05 2018 at 18:16):

Mmmh, I can't reproduce this here. The 2+2 computation is completely erased. Let me upgrade Lean.

#### Gabriel Ebner (Apr 05 2018 at 18:19):

Still can't reproduce.

#### Mario Carneiro (Apr 05 2018 at 18:20):

Actually that #eval doesn't work, lean complains about too few arguments since it's a closure which is waiting for an argument. This shows the closure creation:

set_option trace.compiler.code_gen true
def f := let x := erased.mk (2+2) in x
-- [compiler.code_gen]  f._lambda_1 1
-- 0: scnstr #0
-- 1: ret
-- [compiler.code_gen]  f 0
-- 0: closure f._lambda_1 0
-- 1: localinfo x @ 0
-- 2: push 0
-- 3: drop 1
-- 4: ret


#### Gabriel Ebner (Apr 05 2018 at 18:20):

What do you get with these changes (added has_repr and the set_option):

set_option trace.compiler.optimize_bytecode true

def erased (α : Type*) : Type* := set.range (singleton : α → set α)

namespace erased

@[inline] def mk {α} (a : α) : erased α := ⟨_, a, rfl⟩

noncomputable def out {α} (a : erased α) : α :=
classical.some a.2

theorem mk_out {α} (a : α) : (mk a).out = a :=
eq.symm $(set.mem_singleton_iff _ _).1$
by unfold out; rw [classical.some_spec (mk a).2]; simp [mk]

theorem out_mk {α} (a : erased α) : mk (out a) = a :=
subtype.eq $set.ext$ λ b,
by simp [out, mk, classical.some_spec a.2]

noncomputable def equiv (α) : erased α ≃ α :=
⟨out, mk, out_mk, mk_out⟩

instance (α): has_repr (erased α) := ⟨λ _, "erased"⟩

end erased

#eval (erased.mk (2+2)) -- (erased.mk 4)


#### Gabriel Ebner (Apr 05 2018 at 18:21):

Hmm, as a workaround you can use have ..., from ..., ... instead of let.

#### Mario Carneiro (Apr 05 2018 at 18:22):

Well, the let was just to force the closure creation out of tail call position

#### Mario Carneiro (Apr 05 2018 at 18:23):

if you use have instead it just adds an additional argument to the main function

#### Gabriel Ebner (Apr 05 2018 at 18:25):

I think the problem is just that prop-erasure is not implemented for let, because nobody ever uses lets except for data.

#### Mario Carneiro (Apr 05 2018 at 18:41):

Hm, you can still clearly tell the difference between these two pieces of code:

set_option trace.compiler.code_gen true
#eval let x := 2 + 2 = 4 in x
#eval let x := erased.mk (2+2) in x


I'm glad to see that 2+2 is not evaluated anywhere in the generated code, but it is still creating a closure returning #0 rather than #0 itself

#### Gabriel Ebner (Apr 05 2018 at 18:55):

Now I remember: we can't erase type families to #0. We need to erase them to a function type, but I don't think such an erasure is implemented. If mk is not inlined, then we actually compute 2+2 here.

#### Mario Carneiro (Apr 05 2018 at 18:57):

Here's attempt number 2, which tries to encode each element of erased A as a straight type:

import set_theory.ordinal

universe u
def erased (α : Type u) : Type (u+1) :=
{o // o < cardinal.ord (cardinal.mk α)}

namespace erased
open cardinal ordinal

noncomputable def wo' (α : Type u) :
{r : α → α → Prop // ∃ [wo : is_well_order α r],
ord (mk α) = @ordinal.type α r wo} :=
classical.choice $let ⟨r, wo⟩ := cardinal.ord_eq α in ⟨⟨r, wo⟩⟩ def wo (α : Type u) (x y) := (wo' α).1 x y instance {α} : is_well_order α (wo α) := (wo' α).2.fst theorem wo_eq (α : Type u) : ord (mk α) = type (wo α) := (wo' α).2.snd @[inline] def type {α} (r : α → α → Prop) [wo : is_well_order α r] : ordinal := quot.mk _ ⟨α, r, wo⟩ @[inline] def typein {α} (r : α → α → Prop) [is_well_order α r] (a : α) : ordinal := type (subrel r {b | r b a}) @[inline] def mk {α} (a : α) : erased α := ⟨typein (wo α) a, (wo_eq α).symm ▸ typein_lt_type (wo α) a⟩ noncomputable def out {α} (a : erased α) : α := enum (wo α) a.1 (wo_eq α ▸ a.2) theorem out_mk {α} (a : α) : (mk a).out = a := enum_typein _ _ theorem mk_out {α} (a : erased α) : mk (out a) = a := subtype.eq$ typein_enum _ _

noncomputable def equiv (α) : erased α ≃ α :=
⟨out, mk, mk_out, out_mk⟩

end erased


#### Mario Carneiro (Apr 05 2018 at 18:58):

Since you can't really (provably) distinguish types except by their cardinality, this approach is rather more involved

#### Mario Carneiro (Apr 05 2018 at 18:59):

It also requires a lot of inlining; I had to restate the definitions of ordinal.type and ordinal.typein so they would be inlined

#### Gabriel Ebner (Apr 05 2018 at 19:02):

Anything that relies on inlining will have the closure problem.

#### Mario Carneiro (Apr 05 2018 at 19:06):

Not true:

set_option trace.compiler.code_gen true
def f := @erased.mk ℕ
#eval let x := f (2+2) in x


Note that even though f is not inlined 2+2 is not evaluated

#### Gabriel Ebner (Apr 05 2018 at 19:06):

If you're okay with a bit of extra ugliness, you can define an erase function in both versions:

@[inline]
def erase {α} (a : erased α) : erased α :=
⟨λ x, a.1 x, a.2⟩

-- 👌
def f' := let x := erased.mk (2+2) in x.erase


#### Gabriel Ebner (Apr 05 2018 at 19:08):

Mmh, I still get a call to erased.mk and 2+2, but no call to f since it is (of course) inlined.

#### Gabriel Ebner (Apr 05 2018 at 19:10):

You should set the optimize_bytecode option instead of code_gen, otherwise you miss out on all the optimizations.

#### Mario Carneiro (Apr 05 2018 at 19:15):

I'm confused: why does erase work? The argument count goes down, but it still returns #0. I thought you said type/proof lambdas can't be implemented as #0?

#### Mario Carneiro (Apr 05 2018 at 19:15):

set_option trace.compiler.optimize_bytecode true
def f1 : erased ℕ := (erased.mk (2+2))
def f2 : erased ℕ := (erased.mk (2+2)).erase


#### Gabriel Ebner (Apr 05 2018 at 19:32):

I'm a bit lost as well. Apparently the apply operation is special-cased to also work on #0.

#### Mario Carneiro (Apr 05 2018 at 19:35):

That's why I would expect that type families should also compile as #0 rather than lam x, #0

#### Gabriel Ebner (Apr 05 2018 at 19:38):

You know, type families are actually erased, it's just that subtypes aren't because they haven't been erased yet....:

def f (x : set ℕ) := x
def g (x : { s : set ℕ // true }) := x


Last updated: May 08 2021 at 03:17 UTC