[Agda] Records and irrelevant fields

[Dan Doel]

On Friday 17 September 2010 8:23:04 am Andreas Abel wrote:

> I thought about the Squash type, but my gut feeling was it won't
> provide a nice solution to the problem.

Yeah, probably not.

> Well, but is not the whole point of EPTS's that types can depend on
> irrelevant stuff where programs cannot? If both cannot, we can go back
> to Pfenning's 2001 LiCS system where things work smoothly (but imho,
> boringly).

Yes. And perhaps modifying the erasure within terms is the right way to go.

Currently, it seems to be doing a little more than that. For instance, there's 
nothing to say we can't do irrelevant quantification when producing types. So

  .(x : T) -> Set

is a family of types parametric in its index. But, that's probably pretty 
boring. One isomorphism that holds is:

  .(_ : T) -> U ~ Squash T -> U

so the above family of types is constant. Typically, I wouldn't expect people 
to write such animals.

*But*, inductive types package up the relevance modalities. So, when you write 
someting with type:

  F : ∃ A T -> Set

you are (currently) roughly writing:

  F : .(x : A) -> T x -> Set

so irrelevance does show up in types over inductives. I think the most general 
type for the eliminator we can give for ∃ is as follows:

  elim :  (A : Set) -> (T : A -> Set) -> (P : ∃ A T -> Set)
       -> (f : .(x : A) -> (w : T x) -> P (x , w))
       -> (p : ∃ A T) -> P p

which, while it looks strong, will never allow us to write both projections, 
because P is forced to be irrelevant in the first component of the tuple, and 
\(x, _) -> T x is not.

If we look closely, we can see that we are throwing away an opportunity in the 
above type. In

  f : .(x : A) -> (w : T x) -> P (x , w)

the x appears in a type, and so is relevant there. So, that (x , w) could be a 
normal sigma type, instead of ∃. But then p doesn't have that type. So we have 
two options: weaken the rule, as above, or go inside types making more things 
relevant when we're inside irrelevent contexts. The EPTS stuff chooses the 
former, but I can't say that hte latter is wrong (just a lot more 
complicated).

> With first-class irrefutable patterns, we could write
> 
>    snd : forall {A T} -> ((x , w) : exists A T) -> T x
>    snd (x , w) = w
> 
> Seems harmless to me, since it is merely the uncurrying of
> 
>    snd' : forall {A T} -> .(x : A) -> T x -> T x
>    snd' x w = w
> 
> We could analyze the situation as follows: Currently the system is too
> weak to allow free uncurrying (the situation was similar with the Set
> \omega issue in one of your recent mails, but there you could not
> write down the necessary tuple type).

Hmm, yes, this is true, and suspicious.

> > having weak sums is (if you ask me) part of the interest of this stuff.

I thought about this a little, and it occurred to me that weak sums may not 
necessarily be interesting. What is interesting is *abstraction*. That is why 
people working on module systems are intereseted in weak (and translucent) 
sums: they want to enforce abstraction, and weak sums do, by not allowing you 
to project out the first pair of the sum and inspect it.

But, while weak sums are sufficient, I don't know for a fact that they're 
necessary. Perhaps modalities enforcing parametricity are sufficient, even if 
you can program with them similar to strong sums. I'm going to have to ponder 
what exactly 'abstraction' is trying to achieve before I have an answer to 
this, though.

> Yeah, this sounds hacky.
> 
> The problem is that in
> 
> >  p :r ∃ A P
> >  fst p :c A
> >  snd p :r P (fst p)
> 
> p is relevant, but one of its components not, and only after the match
> the irrelevant components surface, so the context reset should happen
> after the matching.

Maybe, but I think it's worse than that, even. Higher-order irrelevant 
function spaces have the same issue. With

  f : (.(x : A) -> P x -> R) -> R

we can envision:

  f konst :c A

for something like 'konst : .(x : A) -> P x -> .A'. Squash actually achieves a 
limited form of this:

  f (const . squash) :r Squash A

Then we've moved the question of higher-order reset to whether Squash A resets 
to (essentially) A, or whether we can match on a Squash and then reset.

> Maybe the problem requires us to introduce modalities.  I have seen
> approaches with an infinite set of binding-times, not just compile,
> and runtime, but I do not know how they relate here.

I think the EPTS stuff may well be viewed as having multiple binding times 
when you take higher-order and inductive stuff into account. I'm not sure if 
that's a good thing or a bad thing.

Inductive types, and Squash in particular, allow you to package up the 
modality as a unary operator. I think that means that introducing them 
primitively should not be necessary, as long as we can figure out how they 
should behave, and make inductive (and higher-order) types behave that way 
instead.

Perhaps Squash isn't even the right name for said data type, and assuming that 
it is is misleading us. For instance, we expect Squash A to have at most one 
element, and so for functions out of it to be constant. But perhaps they 
should only be constant in dynamic contexts, for instance.

As an additional weirdness point, Mishra-Linger notes in his thesis that the 
EPTS Squash is not a monad in the basic theory:

  data Squash (A : Set) : Set where
    squash : .A -> Squash A

  elim :  (A : Set) (P : Squash A -> Set)
       -> (.(x : A) -> P (squash x)) -> (b : Squash A) -> P b

  join : (A : Set) -> Squash (Squash A) -> Squash A
  join = elim (Squash A) (\_ -> Squash A) ?

What to fill in the hole is the issue. It needs to have type

  .(Squash A) -> Squash A

But \x -> x fails for this. We also cannot do tricks with elim, because (at 
best) it will reduce down to writing .A -> A. So, in the default system, 
Squash A is not interchangeable with Squash (Squash A), and so on. He fixes 
this in an extended system, which only checks equality after erasure, by 
adding squashed axioms. For instance:

  flat : Squash (.(A : Set) -> Squash A -> A)

After erasure, all inhabitants of Squash A look like 'squash', so you can add 
axioms of the above form by asserting that 'squash' has the relevant type. The 
above allows you to write join.

*However*, if context reset modifies types, I believe Squash will naturally be 
a monad (even if it may not exactly be a squash type anymore):

  join = elim (Squash A) (\_ -> Squash A)
          (/\sq -> squash (elim A A (\x -> x) sq))

Above, our first elimination gets passed an irrelevant Squash A. Then, we use 
the squash constructor, and need an A. But, the argument to squash is 
irrelevant, so sq should both reset to being relevant *and* being something 
like Id A rather than Squash A. This allows us to eliminate into A 
successfully. This all erases down to:

  join = elim squash

which is approximately (exactly?) what Mishra-Linger's does, as well, without 
the axiom intermediary.

Perhaps this is on the right track?

-- Dan