[TYPES] Do erasable boxes form a monad?
Jesper Cockx
Jesper at sikanda.be
Fri Oct 26 04:05:21 EDT 2018
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
>
More information about the Types-list
mailing list