[Agda] Records and irrelevant fields

[Dan Doel]

On Thursday 23 September 2010 11:37:46 am Andreas Abel wrote:
> Yes, and you need it to get a consistent theory with proof-irrelevant
> equality, i.e., where
> 
>    p, q : Id A a b
>   ------------------
>   p = q : Id A a b
> 
> holds definitionally everywhere.

Okay.

> Making all types compile-time would enforce type arguments to be
> declared irrelevant as well, e.g.,
> 
>    id : (A :r Set) -> A -> A
> 
> would have to be replaced by
> 
>    id : (A :c Set) -> A -> A

I'd expect id to be typed this way anyway. Even the EPTS erasure inference 
does. :)

> in order to be usable at data type T.  However, with dependent types
> that's probably not a good idea, e.g.
> 
>    Bla : Bool -> Set
>    Bla true = Set
>    Bla false = Bool   -
> 
>    bla : (x : Bool) -> Bla x
>    bla true = Bool -- problem here
>    bla false = true

Yeah, this could be a problem, I guess. Although, it's conceivable that any 
reasonable code written like this would also be compile-time only. I haven't 
rigorously worked out the idea, but I think:

  Bla :c Bool -> Set
  Bla true = Set
  Bla false = Bool

  bla :c (x : Bool) -> Bla x
  bla true = Bool
  bla false = true

would be acceptable.

I suppose annotating all datatypes as compile time based just on my inability 
to imagine them needing to be otherwise (barring type case of some sort) is a 
bad idea, though. :)

-- Dan