[Agda] question about a form of irrelevance elimination

[Neelakantan Krishnaswami]

Hi Thorsten,

Yes, I made a mistake. I didn't realize that Agda's irrelevance had
a *definitional* equality: I just looked at the type signature of the
postulate that Andy wrote.

That said, I think HoTT-style truncation (where elements are
propositionally equal, but we don't put it in the definitional
equality) is incompatible with computational erasure, because the
eliminator for it lets you use a truncated value to compute an element
of a truncated singleton type, and then un-truncate it. So it
seems to me that you have to pass it around.


Best,
Neel



On 14/07/15 10:48, Thorsten Altenkirch wrote:
> Hi Neel & Andy,
>
> I too think that Andy’s proposal is problematic at least if we add the
> definitional equality to the eliminator
>
> !-elim p [ a ] == a
>
> Because this would destroy decidability and termination in an inconsistent
> context. That is if we assume that all types are equal we can type check
> and reduce untyped programs.
>
> I don’t understand your argument, because surely we should be allowed to
> ignore values in closed propositions.
>
> Btw, I do think that Andy’s rule even with the equation above is logically
> sound and that it isn’t such a problem if you have divergent programs
> after you have assumed that pigs can fly.
>
> Thorsten
>
> On 14/07/2015 10:07, "Neelakantan Krishnaswami"
> <n.krishnaswami at cs.bham.ac.uk> wrote:
>
>> Dear Andy,
>>
>> It looks like the escape property you describe is equivalent to the
>> universal property of truncation in HoTT. Adding it means that
>> irrelevance is basically the same as quotienting by the full relation.
>> (See Kraus et al's "Notions of Anonymous Existence in Martin-Loef Type
>> Theory".)
>>
>> However, this has the effect that irrelevant arguments cannot be
>> erased at runtime; you still need to pass them around in case you
>> use an irrelevant argument to construct an escaping value.
>>
>> So, it's consistent to add, but if you care about running dependently
>> typed programs (as opposed to typechecking them), you might not want to
>> add it. :)
>>
>> Best,
>> Neel
>>
>>
>> On 14/07/15 09:48, Andrew Pitts wrote:
>>> Since version 2.2.8, Agda supports irrelevancy annotations
>>>
>>> (http://wiki.portal.chalmers.se/agda/agda.php?n=ReferenceManual.Irrelevan
>>> ce).
>>> Among other things this allows one to define a form of truncation:
>>>
>>> record ! {ℓ : Level}(A : Set ℓ) : Set ℓ where
>>>     constructor ![_]
>>>     field
>>>       .prf : A
>>> open ! public
>>>
>>> Since the elements of ! A are definitionally irrelevant, they are also
>>> propositionally irrelevant, i.e. ! A is a proposition in the sense of
>>> Homotopy Type Theory:
>>>
>>> isProp : {ℓ : Level}(A : Set ℓ) → Set ℓ
>>> isProp A = (x y : A) → x ≡ y
>>> !isprop : {ℓ : Level}{A : Set ℓ} → isProp (! A)
>>> !isprop _ _ = refl
>>>
>>> I would like to be able to escape from an irrelevant context in the
>>> case of propositions:
>>>
>>> postulate
>>>     !elim : {ℓ : Level}{A : Set ℓ}.(_ : isProp A) → (! A) → A
>>>
>>> Does adding such a postulate destroy logical consistency?
>>>
>>> Andy Pitts
>>> _______________________________________________
>>> Agda mailing list
>>> Agda at lists.chalmers.se
>>> https://lists.chalmers.se/mailman/listinfo/agda
>>>
>> _______________________________________________
>> Agda mailing list
>> Agda at lists.chalmers.se
>> https://lists.chalmers.se/mailman/listinfo/agda
>
>
>
>
>
> This message and any attachment are intended solely for the addressee
> and may contain confidential information. If you have received this
> message in error, please send it back to me, and immediately delete it.
>
> Please do not use, copy or disclose the information contained in this
> message or in any attachment.  Any views or opinions expressed by the
> author of this email do not necessarily reflect the views of the
> University of Nottingham.
>
> This message has been checked for viruses but the contents of an
> attachment may still contain software viruses which could damage your
> computer system, you are advised to perform your own checks. Email
> communications with the University of Nottingham may be monitored as
> permitted by UK legislation.
>
>
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>