[Agda] Records and irrelevant fields
Andreas Abel
andreas.abel at ifi.lmu.de
Fri Sep 17 14:23:04 CEST 2010
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/
More information about the Agda
mailing list