[Agda] Records and irrelevant fields

[Andreas Abel]

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.

For now, we have to use data instead.

data Pos : Set where
   mkPos : (n : Nat) -> .(NonNeg n) -> Pos

theNum : Pos -> Nat
theNum (mkPos n p) = n

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/