[Agda] Records and irrelevant fields

[Andreas Abel]

On Sep 21, 2010, at 2:34 AM, Dan Doel wrote:
> On Monday 20 September 2010 6:31:56 pm Andreas Abel wrote:
>> my take on making Squash a monad was to allow matching on irrelevant
>> things if there is at most one match.  There is no theoretical
>> foundation for this yet, so maybe it is unsound, but it seems to be
>> consistent with erasure semantics.
>>
>>   join : {A : Set} -> Squash (Squash A) -> Squash A
>>   join (squash (squash a)) = squash a
>>
>> Well, that in essence says you cannot get more irrelevant than
>> irrelevant.
>
> I believe this is equivalent to what the thesis refers to as token  
> type target
> erasure. It would make the Squash eliminator:
>
>  elimSq : (A : Set) => (P : Squash A -> Set) =>
>           (f : (x : A) => P (squash x)) ->
>           (s : Squash A) => P s
>  elimSq A P f (squash x) = f x

That's programmable in MiniAgda using pattern matching.  And for the  
identity type it is, as you say:

data Id ++[A : Set](a : A) : A -> Set
{ refl : Id A a a
}

fun elimId : [A : Set] -> [P : A -> Set] -> [a, b : A] -> [Id A a b] - 
 > P a -> P b
{ elimId A P a .a (refl .A .a) h = h
}

> and in general, it would improve the eliminator of any singleton  
> type in the
> same way. However, the problem is that equality types are in this  
> class, and
> if you make those erasable, you get bad meta-theoretic properties.

Yeah, with the equality type there is an issue.  You cannot erase  
equality proofs at compile time because you still have to match  
against refl to prevent the bad stuff outlined below.  Also, if you  
want proof irrelevance for the identity type you need to eta-expand  
h : t == t  to refl : t == t, otherwise it is not true that the proof  
of t == t does not matter.

However, I think there is no problem with Squash, because there is  
always exactly one match, whereas with equality types there is at most  
one match, and it has a side information that two things are  
declaratively equal.

> One useful property of the EPTS stuff is that if a term is strongly
> normalizing in the EPTS, then its erasure is strongly normalizing in  
> the
> corresponding IPTS. But, with the above optimization, this is no  
> longer true,
> because stuff like:
>
>  /\(eq : Top == (Top -> Top)) -> \(x : Top) -> cast eq x x
>
> erases down to:
>
>  \x -> cast x x  where  cast M reduces to M
>    =
>  \x -> x x
>
> So you can no longer trust well-typedness in the source language to  
> ensure
> strong normalization in the erased language.

Not for open terms, no.

> And that kills, for instance, the
> 'proof irrelevant' CONV rule, where you get to aggressively erase  
> things
> during type checking (which could, at the least, give a nice  
> performance
> boost).

There are two things.  I found I cannot erase irrelevant terms,  
because of the issue with equality with I solve with eta-expansion.   
And you cannot eta-expand at type a == b if you cannot check whether a  
and b are the same, because you have erased them.

However, I ignore terms marked for erasure during equality checking  
(CONV).  Should do my homework and try to write a paper why this is  
correct.

> I've chatted with Conor McBride on this a bit in the past, and I  
> think the
> crux is this:
>
>  1) The EPTS irrelevant function space tracks what is acceptable to  
> erase
>     in *open* terms (and so, during type checking, even).

Indeed.

>  2) For some proofs, it is acceptable to *equate* them in open  
> terms, but
>     only *erase* them in *closed* terms (and so, only in a final,  
> compiled
>     program).

Yes.

> In the last paragraph of the thesis, it actually talks about  
> extending the
> system to three modalities, one of which tracks the second type of  
> proof. This
> would ensure that you don't do equality casts in compiled programs,  
> say, but
> wouldn't have the bad meta-theoretic properties above. It doesn't  
> get into
> what the right rules for the third modality would be at all, though.

Mmh, that would be the interesting thing.  And what the model is for  
that.  And why you can also equate stuff at compile-time you only  
erase for run-time.

>> Interestingly, the bind operation cannot be defined directly,
>>
>>   bind : {A B : Set} -> Squash A -> (A -> Squash B) -> Squash B
>>   bind (squash a) f = f a -- a cannot be used here!
>>
>> but in terms of map and join (as in the textbooks).
>>
>>   bind sa f = join (map f sa)
>>
>> That's a bit weird.  (Not the first weirdness, as we have seen.)
>
> I looked at the elimination principle that Coq generates for Pf, and  
> it's:
>
>  (A : Set) -> (P : Prop) -> (A -> P) -> Pf A -> P
>
> If this is translated into EPTS style, it's:
>
>  (A P : Set) => (A -> Squash P) -> Squash A -> Squash P
>
> which is precisely the desired bind function for the monad. It  
> cannot be
> proved using just the eliminator given by the thesis, but I'd  
> tentatively say
> that it *could* be given as an alternate eliminator. The reduction  
> behavior
> would be weird, though, since:
>
>  elim at A@P f (squash at x) ==> f x
>
> would use a potentially irrelevant x in a relevant position, and f  
> isn't
> required to use x irrelevantly, *except* that whatever f returns  
> must have the
> form 'squash at M', which can't be relevant in x (I think). I'm not  
> sure if this
> is enough to make it safe, but it might be an option to look into.

This seems to be a different principle, namely that types themselves  
are irrelevant, meaning they contain at most one inhabitant (after  
erasure).  Along this kind of reasoning you could have

   g : (A -> Unit) -> Squash A -> Unit
   g f (squash a) = f a

although in this kind one could argue that it is ok since the r.h.s.  
can be eta-exanded to the empty tuple

   g f (squash a) = ()

Maybe more interesting would be the typing

   g : (A -> Empty) -> Squash A -> Empty

> Other types could get similar eliminators:
>
>  data Ex (A : Set) (T : A -> Set) : Set where
>    _,_ : (x : A) => T x -> Ex A T
>
>  elimS : (A : Set) => (T : A -> Set) => (P : Ex A T -> Set) =>
>          ((x : A) => (w : T x) -> P (x , w)) ->
>          (e : Ex A T) -> P e
>
>  elimP : (A P : Set) => (T : A -> Set) =>
>          ((x : A) -> T x -> Squash P) -> Ex A T -> Squash P
>
> I do admit that it's weird that Squash is used in these, but the  
> alternative
> would be to introduce built-in modal operators (which is essentially  
> what
> Squash is), and Agda doesn't seem to adverse to having declared  
> types serve as
> built-ins via some pragmas.


Cheers,

Andreas Abel  <><      Du bist der geliebte Mensch.

Theoretical Computer Science, University of Munich
Oettingenstr. 67, D-80538 Munich, GERMANY

andreas.abel at ifi.lmu.de
http://www2.tcs.ifi.lmu.de/~abel/