[TYPES] Erasure and equality proofs

[Andreas Abel]

Hi Stefan,

Alan Jeffrey used Agda's irrelevance and added an axiom that one can 
still substitute with irrelevant equality proof.  He might be able to 
tell you more.

I am also very much interested in the interaction between irrelevance 
and case distinction/recursion and equality, so if you get some answers, 
please keep me in the loop!

Best,
Andreas

On 25.08.2016 06:40, Stefan Monnier wrote:
> [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
>
> I'm trying to get my head around the practical use of
> erasure/irrelevant/implicit arguments, as discussed in papers such as
>
>     The Implicit Calculus of Constructions as a Programming Language
>     with Dependent Types
>     Bruno Barras and Bruno Bernardo, fossacs08
>
>     Erasure and polymorphism in pure type systems
>     Nathan Mishra-Linger and Tim Sheard
>
>     On the strength of proof-irrelevant type theories
>     Benjamin Werner, IJCAR06
>
> One of the desired benefits is to erase equality proofs, but those can't
> be erased naively, since they're not only used in type annotations but
> they're fundamentally passed to the corresponding elimination function
> (or "match" expression).  Eliminating them naively could introduce
> inconsistencies (if we remove them in those cases where the equality
> proposition is actually an uninhabited type).
>
> Benjamin suggests we can erase those equality proofs under one
> condition: if the elimination rule is adjusted so that it checks
> equality before performing the reduction.
> But this, in turn requires that the 2 equal terms are not erasable.
>
> Bruno Barras et al. suggests other restrictions: basically he suggests
> to add a new elimination "eq_ind2" with all args erasable but without
> reduction rule (i.e. as a mere axiom).
>
> So I'm looking for some further info/work on actual uses of such
> systems, where the practical impact of such restrictions are
> investigated.  I'm especially interested in this, because I have the
> impression (just gut feeling) that equality is not really special in
> this respect and that many/most other places where proofs are passed end
> up needing special treatment as well in order for those proofs to
> be erasable.
>
> IOW while I see that erasable arguments work fine for System-F style
> parametric type arguments, most of the times when I try to make
> a proof "erasable", I end up bumping into some place in the code where
> I need the proof to appear in a non-erasable part of the code (unless
> I add ad-hoc special rules along the lines suggested above for the
> equality type).
>
> I get the impression that we'd need erasability to be extended along the
> lines of Coq's special treatment of single-constructor elimination from
> Prop to Set, but such an extension doesn't seem to be consistent with
> the use of "convertibility modulo erasure".
>
>
>         Stefan
>


-- 
Andreas Abel  <><      Du bist der geliebte Mensch.

Department of Computer Science and Engineering
Chalmers and Gothenburg University, Sweden

andreas.abel at gu.se
http://www2.tcs.ifi.lmu.de/~abel/