I'm playing around with the type `Erased t` and am having trouble implementing some things which seem like they should be definable.

`Erased t` is defined in Typer as:

type Erased t | erased (_ ::: t)

I.e. a box which contains an erased element for some arbitrary type.

Without inductive types (e.g. in the Implicit Calculus of Construction (ICC) and Tim Sheard's lambda calculus with erasable arguments), we could encode that box using an impredicative encoding:

Erased t = ∀r, (t ≡> r) -> r; erased = λ x ≡> λ f -> f x;

[ where, as usual `≡>` is used for functions whose argument is erasable. ]

Now the funny part about it, is that I can't seem to implement some operations which seem quite reasonable. For example, while I can implement

erased_liftfun : Erased (?t₁ -> ?t₂) -> (Erased ?t₁ -> Erased ?t₂); erased_liftfun f x = case f | erased f' => case x | erased x' => erased (f' x');

I can't seem to be able to implement its inverse:

erased_funlift : (Erased ?t₁ -> Erased ?t₂) -> Erased (?t₁ -> ?t₂);

Similarly, I can't implement

erased_bind : (Erased t₁) -> (t₁ -> Erased t₂) -> Erased t₂;

To be honest, I'm not 100% sure that it should be safe to have `erased_funlift`, but `erased_bind` seems eminently safe.

Another thing is that I can't seem to be able to implement `erased_bind` from `erased_funlift` nor the reverse, so if I wanted them, I'd have to provide them *both* as axioms.

Of course, I'd rather come up with another axiom from which I could define those two, but I'm not sure what that axiom would be like.

In the same area, is the question of the safety of `erased_join`:

erased_join : (Erased (Erase t)) -> Erased t;

I suspect having `erased_join` would be unsafe, but I'm not sure.

Anyway, I just wanted to vent my frustration here.

You can now return to your regular hacking,

Stefan