[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
I'm playing with erasability in the sense of the Implicit Calculus of
Constructions and bumping into problems:
Say we create a datatype holding an erasable element.
We could define it as follows using the impredicative encoding:
Erased : Type -> Type;
Erased t = (r : Type) -> (t ≡> r) -> r;
erase : (t : Type) ≡> t -> Erased t;
erase t x = λ r -> λ f -> f x;
where I use ≡> to denote the "implicit" abstraction (which I like to
call "erasable", and yet others might favor "irrelevant").
With such a definition, we can implement functions such as:
erased_liftfun : Erased (t₁ -> t₂) -> (Erased t₁ -> Erased t₂);
erased_liftfun f x = case f
| erase f' => case x
| erase x' => erase (f' x');
[ where I write `case e of erase x => ...x...x...` instead of
`e (λ x ≡> ...x...x...)` ]
But I can't seem to write the reverse function.
More puzzlingly, I can't seem to write the monad bind operator.
I.e. the below types seem not to be inhabited:
erased_bind : Erased t₁ -> (t₁ -> Erased t₂) -> Erased t₂;
erased_funlift : (Erased ?t₁ -> Erased ?t₂) -> Erased (?t₁ -> ?t₂);
Am I just not trying hard enough, or is there something deeper?
Would it break the consistency of the logic to add one of those as
an axiom?
Stefan
