[Agda] Records and irrelevant fields

[Andreas Abel]

On Sep 22, 2010, at 12:42 AM, Dan Doel wrote:
> On Tuesday 21 September 2010 3:13:18 am Andreas Abel wrote:
>
>> 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.
>
> Having thought about this some more, I came to the conclusion that  
> it is
> indeed just another statement that double-irrelevance is the same as
> irrelevance, or that Squash is a monad. It makes the following  
> equivalent:
>
>  Squash A => B
>  Squash A -> B
>         A => B
>
> at least in the non-dependent cases. And that first case is also the  
> same as
>
>  Squash (Squash A) -> B
>
> I'm willing to bet that this case is sound. The question then  
> becomes: how
> does one decide when it's safe (Squash) and when it isn't  
> (equality)? Or are a
> couple special cases (Squash and Unit alikes) enough?

Well, if you look at the definition of equality (allow me to stick to  
MiniAgda syntax)

data Eq (A : Set)(a : A) : A -> Set
  { refl : Eq A a a
}

then you see that you are dealing with a non-linear pattern inductive  
family (quite a mouthful ;-)).  This is to say that the arguments to  
Eq in the constructor type(s) are all patterns, but non-linear.  If  
you construct an Eq A a b by refl, you are putting the "side  
information" in that a and b are definitionally equal, but this side  
information is not just a component of the structure you are creating  
(in this case the "structure" refl you create carries in fact no  
structure).

How to handle this side information I am not 100% clear.  In MiniAgda,  
I allow also irrelevant matches against refl, but this leads to  
inability to erase at compile-time.  I still have proof irrelevance,  
but from a performance aspect it would be nice to actually throw away  
more during compile-time.

If one retreats to the "safer" EPTS with compile-time erasure, but  
still wants proof irrelevance for equality, the we cannot allow all  
these legal MiniAgda typings for subst, for instance.

0)  subst : [A : Set] -> [P : A -> Set] -> (a, b : A) -> Id A a b -> P  
a -> P b
1)  subst : [A : Set] -> [P : A -> Set] -> [a, b : A] -> Id A a b -> P  
a -> P b
2)  subst : [A : Set] -> [P : A -> Set] -> (a, b : A) -> [Id A a b] ->  
P a -> P b
3)  subst : [A : Set] -> [P : A -> Set] -> [a, b : A] -> [Id A a b] ->  
P a -> P b

   subst A P a .a (refl .A .a) h = h

0 is uncontroversial.  1 is the EPTS one and likewise harmless, but it  
fails proof irrelevance, because

   subst A P a a p h

does not reduce for p != refl.  Note that 0 leaves the option for  
proof irrelevance, because a and b are not erased, thus instead of  
checking p for refl you can check a and b for equality.

2 looks a bit weird at first glance, but it is inessence what is  
described in Benjamin Werner's 2008 paper on proof irr.  Here, we  
never check p for refl, but always compare a and b for equality.  This  
looks like a systematic solution, but in terms of performance it could  
be cheaper to check p for refl.  Who knows?  There might be a lot of  
computation necessary to normalize p to refl, but likewise to  
normalize both a and b to check for equality.

3 does not permit compile-time erasure, that's the current situation  
in MiniAgda.

How can we change the type system to dissallow 1-3?  Forbidding  
irrelevant matching on non-linear pattern inductive families would  
rule out 2 and 3.  Forbidding 1 could be done by saying a and b are  
relevant in Id A a b even on the type level.  This, of course is not  
EPTS, it is more like Pfenning's system, but not quite, ... see below.

> On an unrelated note, I studied a bit more of Pfenning's modal type  
> theory in
> the paper I mentioned earlier. I can find no difference in the  
> context reset
> rules between his proof irrelevant modality and the modality in  
> EPTS. The
> difference between the two theories has to do with some of the type  
> formation
> rules. For instance, Pfenning gives pi formation as:
>
>  G |- A * Type   G , x * A |- B : Type
>  --------------------------------------
>        G |- (Pi x * A. B) : Type
>
> where * stands in for any particular modality. In an EPTS, it's:
>
>  G |- A :r Type  G , x :r A |- B :r Type
>  ---------------------------------------
>         G |- (Pi x * A. B) :r Type
>
> * again standing in for either :r or :c, to similarize the notation.

This is THE difference. ;-)

> I don't actually know how different this makes the two theories, but  
> the
> irrelevant modalities in either are going to be pretty similar. The  
> EPTS
> thesis states that the difference between the two is their desire to  
> treat
> erasability as extrinsic to to the type, while Pfenning's models  
> intrinsic
> erasability---for instance, x must be erasable from the type of B in
> Pfenning's system (and the judgment of the type of A has a  
> corresponding
> modality), whereas it's relevant in the EPTS.

The difference become apparent in the standard example for dependent  
types ;-).

   vcons : [n : Nat] -> A -> Vec A n -> Vec A (suc n)

is not well-typed in Pfenning's System unless n is irrelevant in Vec

   Vec : (A : Set) -> [n : Nat] -> Set

but this means that Vec A zero = Vec A (suc n) which is not desirable.

Pfennings system is good for *proof* irrelevance only, since he has

   (x : Squash A) -> B x   isomorphic to    [x : A] -> B x

not only

   Squash A -> B   isomorphic to [A] -> B

as in EPTS.
This is why I said Pfenning's system was "boring" (maybe it I should  
say "not good enough").

> I guess that might mean that EPTSes are quite close to the LiCS  
> stuff you
> mentioned earlier.

By "LiCS" I meant exactly Pfenning's paper you just studied.

> I've also come to a tentative conclusion that weakness of  
> elimination is kind
> of important to the abstraction guarantees of, say, modules. We  
> might have a
> signature like:
>
>  mod : exists T : Set.
>          T * (T -> T) * (forall R. R -> (R -> R) -> T -> R)
>
> and a key aspect of the abstraction is that T must always be opaque  
> outside of
> the definition of 'mod', even if we happen to know what the  
> definition of mod
> is, I think (that is, mod is some particular definition, not some  
> variable
> we've quantified over). Even if we are only able to project out T at  
> compile
> time, if (proj1 mod) isn't opaque, then we are no longer required to  
> program
> to the interface exposed by the module.

You mean that if you had the projections (mod.T is not exactly right,  
but in essence)

   Z : mod -> mod.T
   S : mod -> mod.T -> mod.T
   iter : ...

Then

   Z nat_mod : Nat
   S nat_mod : Nat -> Nat

I see, then compile-time erasure is again not possible.

Thanks, this shows that my idea of first-class irrefutable patterns  
and erasure is flawed.
Indeed, it does not work:

   snd : (exist a b : Exists A B) -> B a

is illtyped.  We have to show

   (exists a b : Exists A B) |- B a : Set

which simplifies to

   [a : A], b : B a |- B a : Set

which gives a type error since a is irrelevant and cannot appear in B  
a.  (Also the context is ill-formed).
So I should drop this idea, at least for compile-time erasure.

> In this sense, inductives with irrelevant fields are kind of like  
> units of
> erasure. We can't project the A out of an Exists A P, except as a  
> Squash A,
> because it's already been erased, to enforce the abstraction above.  
> Of course,
> I can see this not necessarily being what is always desired. You may  
> sometimes
> want a compile/runtime devide where compile time things are always  
> transparent
> at compile time. Perhaps it's possible to incorporate both.

Cheers,
Andreas

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/