[Agda] Records and irrelevant fields

[Andreas Abel]

On Sep 23, 2010, at 4:58 PM, Dan Doel wrote:
>> 2 looks a bit weird at first glance, but it is inessence what is
>> described in Benjamin Werner's 2008 paper on proof irr.  Here, we
>> never check p for refl, but always compare a and b for equality.   
>> This
>> looks like a systematic solution, but in terms of performance it  
>> could
>> be cheaper to check p for refl.  Who knows?  There might be a lot of
>> computation necessary to normalize p to refl, but likewise to
>> normalize both a and b to check for equality.
>
> What is the motivation for this? Is it to make
>
>  subst P a b eq Pa = Pa
>
> hold definitionally when a and b are definitionally equal?

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.

> I should mention, I have thought that it might be useful to be able  
> to make
> compile-time definitions. Something like:
>
>  module Foo where
>    size :c Nat
>    size = 10
>
>    vec :r Vec Nat size
>    vec = ...
>
>    Abbr :c Set -> Set
>    Abbr T = ...
>
> which sort of corresponds to extension of some global context in the  
> obvious
> way. 'size' and 'Abbr' would only be able to appear in types or other
> irrelevant positions (which would include other compile-time  
> definitions), and
> so, ultimately, a compiler would not have to generate any run-time  
> code for
> them. (As another example, I suspect that for any declaration 'data  
> T : Srt',
> we could treat T :c Srt, although I doubt that'll be a great boon to  
> any
> compiler.)

MiniAgda has local compile-time definitions in the form

   let [x : A] = s
   in t

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

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

> If we were to try to translate modules with definitions like these  
> to terms in
> a type theory, I think they would work like you were thinking. They're
> compile-time only, but they're transparent. Higher-order irrelevant  
> terms and
> inductive types in an EPTS, by contrast, are opaque, and enforce  
> abstraction.
> It would be the difference between:
>
>  module Bar where
>    open import Foo
>
>    vec' :r Vec Nat size
>    vec' = [1..10]
>
> where we can, in Bar, know that size = 10, and:
>
>  module Baz where
>    open import Foo
>
>    vec' :r Vec Nat size
>    vec' = ? -- we can't hope to put anything here but Foo.vec

OK.

> I believe a lot of thought has been put into these distinctions by  
> people
> working in ML variants, and the ultimate aim there is to allow you  
> to do
> *both*, because both are useful (and insasmuch as Agda's dependent  
> records are
> used as first-class modules, they'd probably both be useful in  
> Agda). But
> they're definitely different animals, and I'm not certain how to  
> make them
> coexist in this type of framework. It may be as simple as an  
> intermediate
> modality, though.


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/