[TYPES] Do erasable boxes form a monad?

Stefan Monnier monnier at IRO.UMontreal.CA
Thu Oct 25 17:46:47 EDT 2018

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?


More information about the Types-list mailing list