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

[Conor McBride]

Hi Dan

On 27 Mar 2008, at 15:07, Dan Licata wrote:
> Hi Conor,
>
> On Mar25, Conor McBride wrote:
>> 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.
>
> That's only because ==/Refl is the wrong notion of propositional
> equality for negative types, though.

Indeed.

>   Which is a valid complaint given
> that I was asking about adding a feature to agda today.  But with the
> right notion of propositional equality, making the "wrong"
> propositionally equal choice during inference would never change
> provability, I think.

Yes. And even better, the technique we've used to get an
equality which has the right behaviour also makes it easy
to have proof irrelevance in the definitional equality.


>
>>>> 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,
>
> Thanks for the detailed reply!  These insights into the design of
> epigram are always interesting and enlightening.  I think I understand
> what's going on a little better now.
>
> One high-level question:
>
>> A key design criterion is to ensure that proofs are
>> really erasable at run time.
>
> Is there a reason irrelevance should be related to erasability?
> Irrelevance isn't a necessary condition for erasability (e.g., if you
> have a Vec and you don't compute with the length, you might erase it,
> but you don't want the Vec to be indexed by an irrelevant Nat!).

Right. I think there are several different ways in which
erasure can usefully come about. We certainly want to
erase types at run time (and we can, because the only
operation which inspects types is the coercion between
provably equal types, which we also erase). We also
want to erase data which is only present for static
purposes. The stuff that the two Brunos are doing and
the "lightning" thing that Edwin and I once sketched
have something to offer here. It would be great to
have a uniform framework for erasure schemes,
distinguishing mild erasure for open computation from
violent erasure for run time. But we should expect
"nothing to see" erasure and "we never look" erasure
to be different.

>
> And an example like
>
>  (X : Set) -> ((x y : X) -> x == y) -> Squash X -> X
>
> shows that you might want an irrelevant type (all elements of Squash X
> are definitionally equal) that is not erasable (just because  
> they're all
> equal, doesn't mean I can come up with one out of thin air).

Yes. Squash shows up as a rather extreme quotient: we
certainly want to support forms of information-hiding
which don't go all the way to erasure.

>
> So why bundle the two concepts together?  I believe that it's a useful
> thing to do, because you
>
>> get away with a remarkably liberal property:
>>
>>   Consistent propositional postulates preserve canonicity
>>   of closed computation in sets.
>
> which gives you the freedom to add whatever axioms you want to Prf,
> without giving them computational behavior.

As Randy often says, "the best thing about working in
a strongly normalizing system is not having to
normalize things". In this setting, we don't need to
compute proofs, which somehow turns into a way of
characterizing what sort of program a proof is.

>
>
> But is there a deeper reason why irrelevance (there is at most one  
> term
> of a type definitionally) and erasability (not needing to pass the
> term at run-time) are intertwined?  This aspect of prop/set  
> distinctions
> has always puzzled me.

It seems to me that this Prop universe is really
capturing the purely negative "nothing to see"
fragment, which naturally induces both erasability
and irrelevance. We should also expect "we never
look" and "we may look statically, but we never
look dynamically" to show up in the positive
world.

Proofs are wine and data is potato: it is
correspondingly useful to be able to tell Sweden
from France.

In vino veritas

Conor