[TYPES] Do erasable boxes form a monad?
monnier at iro.umontreal.ca
Fri Oct 26 15:55:16 EDT 2018
> 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):
That's the thing: with Coq-style Prop's erasability I can define those
operations, indeed. But in the context of ICC's erasability (which is
not tied to Prop and is used to strengthen the conversion rule by
checking beta-equivalence on the erased version of the code), it seems
that those properties don't hold any more.
> _>>=_ : Erase A → (A → Erase B) → Erase B
> (box (squash x) >>= f) .unbox = f x .unbox
In ICC this definition is rejected because the erasure of this code is
>>= f = f x
where `x` is a "dangling" free variable, because the left hand side
argument is erased, but `f` takes a non-erasable argument so its
argument is not erased.
More information about the Types-list