[Agda] Records and irrelevant fields

[Andreas Abel]

Hi Dan,

On Sep 17, 2010, at 12:16 PM, Dan Doel wrote:
> There may be partial solutions to this. One important irrelevant  
> inductive
> type is:
>
>  data Squash (A : Set) : Set where
>    squash : .A -> Squash A
>
> which throws away all information about what element of A you have.  
> You can
> project out irrelevant fields using this type:

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

> Although in general, I don't think you can. For instance:
>
>  data ∃ (A : Set) (T : A → Set) : Set where
>    _,_ : .(x : A) → (w : T x) → ∃ A T
>
>  fst : ∀{A T} → ∃ A T → Squash A
>  fst (x , _) = squash x
>
>  snd : ∀{A T} → (p : ∃ A T) → T ?
>
> I'm not sure there's anything to fill in for the hole there. T  
> doesn't take a
> Squash A, and we can't eliminate the squash in the type correctly.  
> This is
> actually probably a good thing, though, as it ensures that ∃ is a  
> weak sum,
> and enforces the abstraction guarantees we want. I suppose this  
> example is
> another nail in the coffin, though, as even though we can project  
> out the
> irrelevant field using squash, we cannot project out the relevant  
> field,
> because its type depends on the irrelevant field, which we can't  
> access
> normally.

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

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

Even a partial record match could be useful

   snd : forall {A T} -> (record { x = x } : exists A T) -> T x
   ...

> I thought about this a fair amount a while back, considering just  
> things like
> ∃ above, with elimination by projections. I had been thinking  
> something like:
>
>  p :r ∃ A P
>  fst p :c A
>  snd p :r P (fst p)
>
> That doesn't work, but it will if you change context reset to be:
>
>  reset (G , p :? ∃ A P) = reset G , p :r Σ A P
>
> which isn't totally crazy, since those contexts are essentially:
>
>  reset (G , fst p :c A , snd p :r P (fst p)) = reset g , fst p :r  
> A , ...
>
> But if we do that, what about higher-order encodings of those? Do we  
> reset
>
>  G , f : (R : Set) -> (.(x : A) -> P x -> R) -> R
>
> to
>
>  G , f : (R : Set) -> ((x : A) -> P x -> R) -> R
>
> Sheard/Mishra-Linger say no. If we do stuff like this, it also means  
> that ∃ is
> again a strong sum, I believe, and having weak sums is (if you ask  
> me) part of
> the interest of this stuff.

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

Meanwhile, I have asked Bruno Barras if he allows "snd" in his  
implementation Coq*.

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/