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

[Conor McBride]

Hi Dan

On 25 Mar 2008, at 03:46, Dan Licata wrote:

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

[..]

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

That's certainly a good question to ask. I'd certainly like
the IDE to offer me the available constructor forms when
I'm building an element of a datatype. I can also imagine
a symbol other than _ meaning "choose the unique *constructor*
solution": James McKinna wanted such a thing back in the
Lego days.


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

So I imagine, but perhaps Ulf can enlighten us. It's certainly
a desirable property, but I can imagine dropping it if I had a
clear idea of what the default behaviour would be (as is the
case with your proposal). For the most part, though, I think
it's better if choices (even those which only affect intensional
properties) are made with a nonzero amount of text. But as you
say, if there's a manual override, it's a matter of taste. I
guess it's a question of minimizing confusion.


> (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)?

Indeed (1) is what I had in mind. Please do bear in mind that
(2) is not so far from (1). Consider

foo : true == true -> true == true
foo x = ?

moo : foo == id
moo = ?

How you fill in the foo hole will determine *whether* you can
fill in the moo hole.

>
>
> 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?)

Quite.

> but the run-time behavior will not.

It's often important in practice to take care with the
partial evaluation behaviour of programs as well. It can
make a big difference.

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

I guess I'm worried about those maddening mismatches that
you get in intensional type theory becoming even more
subtle and hard to trace.

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

Extensionality gremlins aside, I guess this question comes
down to "when is silence a sensible way to indicate the
default intensional choice?". It's a matter of taste, but
the key thing to bear in mind is that the program is the
evidence and should read as such: clutter is bad, but so
is voodoo. People already have a hard time predicting
the result of implicit argument synthesis. I think your
proposal is one of the more predictable mechanisms, but
it still has potential for scary weirdness. It could be a
good thing to try, but caution is certainly appropriate.


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

Let's be careful about "or": Prop codes for sets which
have at most one inhabitant, up to observation.

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

If we like (and we do), we can have the inhabitation
predicate

   Inh : Set -> Prop

but crucially, this eliminates only over Prop.

A key design criterion is to ensure that proofs are
really erasable at run time. You *don't* get

(X : Set) -> Prf (all x y : X -> x == y) -> Prf (Inh X) -> X

because we're going to erase the middle two arguments
and it isn't going to work. Even if we did keep the proofs
around, the above would force us sometimes to compute strictly
in proofs of true statements, which is shocking! We carefully
get away with a remarkably liberal property:

   Consistent propositional postulates preserve canonicity
   of closed computation in sets.

>
> 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)
> ...

So we can certainly go from Prf . Inh . Prf  to  Prf without any hassle.

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

We can also define squashing

Squash : Set -> Set

as a quotient, and then we do have

(X : Set) -> Prf (all x y : X -> x == y) -> Squash X -> X

but the element of Squash X is really represented by an actual
element of X, so there's no magic.


>
>> 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?)

Mostly, but there are some booby traps.


> Not that I'm
> arguing for doing propositionally what can be done definitionally  
> in the
> long run, just in the here now.

I wish I knew when we're going to get to make this
happen.

All the best

Conor