[Agda] Records and irrelevant fields

[Dan Doel]

On Friday 17 September 2010 4:52:54 am Andreas Abel wrote:
> It seems that we cannot have records with irrelevant fields, like e.g.
> 
> postulate NonNeg : Nat -> Set
> 
> record Pos : Set where
>    constructor mkPos
>    field
>      theNum : Nat
>      .theProof : NonNeg theNum
> 
> because the second projection is not definable
> 
> Pos.theProof : (r : Pos) -> NonNeg (Pos.theNum r)
> Pos.theProof (mkPos n p) = p
> 
> Since p is irrelevant, it cannot be returned.
> 
> Consequently, eta-expansion for Pos does not work either, nor
> replacing the match against mkPos by projections (new feature of 2.2.8).
> 
> The theory of irrelevance (Barras/Bernardo, Sheard/Mishra-Linger) does
> not account for definitions which can only be used in irrelevant
> context, such as Pos.theProof.

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:

> For now, we have to use data instead.
>
> data Pos : Set where
>    mkPos : (n : Nat) -> .(NonNeg n) -> Pos

  elim : {P : Pos -> Set} -> ((n : Nat) -> .(p : NonNeg n) -> P (mkpos n p))
       -> (p : Pos) -> P p
  elim f (mkPos n p) = f n p

  theNum : Pos -> Nat
  theNum = elim (\n -> /\_ -> n)

  theProof : (p : Pos) -> Squash (NonNeg (theNum p))
  theProof = elim (\n -> /\p -> squash at p)

I don't know how feasible it would be, but it's conceivable that record 
projections could automatically project to a squashed type, possibly declared 
with a BUILTIN pragma.

In this case, you should also be able to go back:

  construct : (n : Nat) -> Squash (NonNeg n) -> Pos
  construct n sp = elimSquash (mkPos n) sp

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.

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.

I don't have any firm answers on the subject.

-- Dan