[TYPES] Do erasable boxes form a monad?
Jesper at sikanda.be
Fri Oct 26 04:05:21 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):
data Squash (A : Set) : Prop where
squash : A → Squash A
record Box (B : Prop) : Set where
field unbox : B
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.
On Fri, Oct 26, 2018 at 8:31 AM Stefan Monnier <monnier at iro.umontreal.ca>
> [ 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?
More information about the Types-list