[TYPES] Erasure and equality proofs

[Stefan Monnier]

> 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!

No other answer so far :-(

In Benjamin Werner's article, he proposes as crucial the property that
erasure and reduction commute, but I think that a way out may be to relax
this requirement.  Instead of having

    e ↝ e'   <=>   [e] ↝ [e']

I think intuitively it should be sufficient to have something like

    e ↝ e'   <=   [e] ↝ [e']

maybe combined with

    e ↝ e'   =>  [e] ↝ [e']       *in an empty context*

That would allow us to have more reduction rules (e.g. reduction of
eq_ind2 when applied to eq_refl) on the non-erased side of the world.

I think this should be safe in the sense that the lack of corresponding
reductions in the erased world could simply cause the convertibility
check to fail (i.e. it will reject code which it could/should accept),
but it should not introduce inconsistencies.

This is similar to adding eq_ind2 as an axiom, except that we can still
have a reduction rule for it in the non-erased world.  It does bring
unexpected behaviors, tho: code may be accepted or rejected depending on
the order in which erasure and reduction take place.

Of course, the question remains whether adding eq_ind2 as an axiom
is safe, and/or how it might interact with other axioms.  E.g. as
mentioned in Benjamin's article erasable equality proofs make the
K axiom unnecessary (although I was too weak to actually prove the
K axiom itself.  I wonder if it's just because of my being feeble
minded, or if it's really that such erasability does not really entail
the K axiom).


        Stefan


> 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/