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

[Conor McBride]

Hi Dan

Mixed news. You're right that...

On 24 Mar 2008, at 15:08, Dan Licata wrote:

> On Mar23, Ulf Norell wrote:
>> Defining True to be the record type with no fields is what's going  
>> to make
>> this possible. Records support eta equality, which means that any  
>> record
>> element "r" is equal to the record build by projecting the fields  
>> of "r". In
>> the case of True this means that any element of True is equal to  
>> any other
>> element of True. In particular, if the type checker is trying to find
>> something of type True there's only one choice.

...the spirit of proof irrelevance which drives Ulf's trick
might usefully be extended, but this...

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

The reason this stuff works so sweetly for functions,
records and units is that they're smooth negative formulae
you can drink through a straw. Inductive data is kind of
on the crunchy side. Evaluating open terms from inductive
types whilst respecting eta-laws is rather like eating raw
carrots without using your teeth.

That's not to say it's impossible: with an appropriate
mechanical contrivance, you can juice your carrots;
similarly you can replace (or better, supplement) matching
on Refl with a test of the definitional equality on the
values which are alleged to be equal, thus determining if
the proof is eta-equivalent to Refl. (You can find an
implementation of this variant by rewinding the Epigram 2
darcs repo to about January 2007. It was really ugly.
Maybe that's not a good enough reason not to do it. We'd
still be managing equality that way if we hadn't had a
better idea...)

To follow your suggestion for inductive families in
general, not just a hard-wired weird equality, you
need to build your eta-inspired proof search into the
operational semantics of evaluation, because it's
really the same question that comes up: could there
be a unique canonical proof?

But there are other options...

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

The easy bit is then to add proof-irrelevance for
Prf P to the type-directed definitional equality.
The hard bit is to make sure that all the
proof-driven operations over sets actually
respect that rather generous relation. The easy
bit of the hard bit is to postulate

   nonsense : Prf False -> {A : Set} -> A

with no computational behaviour. It's ok (it's
better than ok) for that guy to get stuck,
because no proof of False is eta-equivalent to
a constructor-proof of False.

The hard bit of the hard bit is to make sure
that

   coerce : (S T : Set) ->
            Prf (S == T) -> S -> T

computes lazily enough in the proof. But
everything's relative: this just dropped out
neatly from the stuff we were doing to make
== extensional anyway.

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.

I guess it's a bit down the line, but I think
it's a good way to go.

All the best

Conor