[TYPES] Do erasable boxes form a monad?

[Jesper Cockx]

Hi Stefan,

I'm not very sure about your impredicative encoding, but both your examples
work if you define Erased in a more direct way in Agda extended with Prop
(currently in the development version of Agda):

data Squash (A : Set) : Prop where
  squash : A → Squash A

record Box (B : Prop) : Set where
  constructor box
  field unbox : B
open Box

Erase : Set → Set
Erase A = Box (Squash A)

lift-squash : Squash (A → B) → Squash A → Squash B
lift-squash (squash f) (squash x) = squash (f x)

lift-erase : Erase (A → B) → Erase A → Erase B
lift-erase f x = box (lift-squash (unbox f) (unbox x))

return : A → Erase A
return x = box (squash x)

_>>=_ : Erase A → (A → Erase B) → Erase B
(box (squash x) >>= f) .unbox = f x .unbox

left-identity : (a : A) (f : A → Erase B) → return a >>= f ≡ f a
left-identity a f = refl

right-identity : (m : Erase A) → m >>= return ≡ m
right-identity m = refl

associativity : (m : Erase A) (f : A → Erase B) (g : B → Erase C)
              → (m >>= f) >>= g ≡ m >>= (λ x → f x >>= g)
associativity m f g = refl

Since Agda's implementation of Prop is heavily based on the proposed sProp
extension to Coq, I expect it would also work with that. So if you cannot
implement it for your impredicative version, at least adding it as an axiom
should not break consistency.

-- Jesper

On Fri, Oct 26, 2018 at 8:31 AM Stefan Monnier <monnier at iro.umontreal.ca>
wrote:

> [ 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
>