[Agda] It feels like there isn't a way to do a partial subtraction nicely ... and a feature suggestion :)

[Dan Licata]

Hi Conor,

On Mar24, Conor McBride wrote:
> >I've sometimes wished term inference would exploit a similar eta-like
> >rule for identity types.  I.e., if you see a goal (a == a), fill it in
> >with Refl {a}.  Here's a stab at a more general way of phrasing this,
> >which stops short of having the type checker do arbitrary logic
> >programming: if you have a goal whose type is an inductive family
> >instance that can be satisfied by exactly one constructor, all of  
> >whose
> >arguments are determined by the goal type, then fill it in.   
> >Because any
> >term of the goal type will be eta-equivalent to what the type checker
> >guesses, the guess is irrelevant to the execution behavior of the
> >program.
> 
> ...takes a lot of care. Remember that we need to be able to
> compute in non-empty contexts. If you want an eta-rule for
> equality, you have to make sure you treat non-canonical proofs
> of (a == a) just the same as Refl, so you can't have
> 
>   subst {A} {a} {.a} Refl P p = p
> 
> with the usual strict semantics and expect the definitional
> equality to be a congruence. It's not enough to add a kind
> of proof irrelevance to the type-directed conversion: you
> need to make sure evaluation respects equality too. (You
> can find this mistake in Epigram 1, if you look hard
> enough.)

I think I had a weaker correctness criterion in mind.  I think of the
implicit argument mechanism as being an IDE issue---it helps me write
code, but the official program is the one with all the implicit args
filled in.  So my question is what makes for a useful IDE.  I could ask:

(1) Everything it fills in for me is uniquely determined up to
definitional equality (is this the case for Agda today?)

(2) Everything it fills in for me is uniquely determined up to
propositional equality

I had in mind (2), but I think your comments pertain to (1)?  

I'd be skeptical of anything that doesn't satisfy (2), because then the
run-time behavior of my program might be influenced by what choices the
IDE makes.  With (2), the type-checkability of my program will be
sensitive to the tactics the IDE uses (does it guess Refl or x if 
x : Id a a is in scope?) but the run-time behavior will not.  And if the type
checker guesses an inconvenient term, I can provide the argument
explicitly (so I'm no worse off than I am today) or do some
propositional equality wrangling myself.  That doesn't seem too bad,
unless there are some consequences I'm not foreseeing.

For my suggestion about equality above, all I had in mind was making the
IDE guess Refl or other propositionally unique terms, without changing
definitional equality at all.  I agree with your more-general story
about needing to have your dentures glued in tight before biting off
eta-equivalence for positive types (whose eta rules are really about
continuations, not about values).

> >Most of the time, I'm happy to just write the Refl myself.  Where this
> >bit of proof search would be nice is when you have an equality
> >constraint in the syntax of a DSEL, so writing the Refl's all over the
> >place clutters things up relative to the concrete syntax you have in
> >mind.  A minor issue, I know, but I thought I'd bring it up and see if
> >it's on anyone else's wish lists.
> 
> I think it's becoming a more important issue. That
> lump of code I wrote the other week (that made the
> stack overflow) was full of tedious explicit proof
> manipulation.
> 
> Achieving proof irrelevance in the definitional
> equality opens the door to more automation in
> proof search. In the Epigram 2 core, we've done
> it by separating Prop and Set explicitly, as a
> universe a la Tarski with an explicit decoder
> 
>   Prf : Prop -> Set

Actually, I'm curious about this setup.  Does Prop only give codes for
Sets that already have 0 or 1 inhabitants, or can I put anything I want
in Prop (e.g., Somewhere : (Elt -> Set) -> List Elt -> Prop defined
inductively) but have it be treated irrelevantly?  Also, is there an
inclusion from Set to Prop, or do I have to pick relevance
vs. irrelevance when I define a type?

My first instinct for handling irrelevance would be to add a Set
Irrel(A) whose inhabitants are inhabitants of A (an arbitrary Set) but
treated irrelevantly defintionally. (I think these were called "squash
types" in NuPRL, and I'm also thinking of things along the lines of
Pfenning's 2001 LICS paper, or the Awodey-Bauer paper on Props as
[Types]).  This would squeeze the balloon to justifying

runirrel_False : Irrel False -> False
runirrel_True  : Irrel True  -> True
runirrel_Id    : {M N A B} -> Irrel (M:A == N:B) -> M:A == N:B
 (even for observational equality, there are still 0 or 1 inhabitants
 for any given M,N,A,B)
...

that allow you to escape the irrelevance modality for any type that is
actually irrelevant.  This approach, if it works in this setting, would
allow me to define a Set like Somewhere once and use it relevantly (when
I want to compute based on the index into the list) and irrelevantly
(when I don't want the proof of a side condition to influence equality)
in different parts of the program.  I'm curious whether you guys tried
this, and how it relates to what you described above.
  
> So, to sum up
> 
>   (1) more proof search would be useful;
>   (2) proof search requires proof irrelevance;
>   (3) proof irrelevance doesn't grow on trees;
>   (4) you can get it if you really want, but
>         you must try.

But does proof search require definitional proof irrelevance, or can we
exploit the propositional irrelevance we already have?  (If you try
sometime, might you just find, you have what you need?)  Not that I'm
arguing for doing propositionally what can be done definitionally in the
long run, just in the here now.  

-Dan