[Agda] Records and irrelevant fields

[Dan Doel]

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

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.

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

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

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.

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

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.

-- Dan