[Agda] Records and irrelevant fields

[Dan Doel]

On Thursday 23 September 2010 8:22:53 am Andreas Abel 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?

> This is THE difference. ;-)

I thought some of the other rules might be different, as well. But of course, 
the systematic difference is that irrelevance in terms requires irrelevance in 
types in Pfenning's theory, and not in EPTS.

> Pfennings system is good for *proof* irrelevance only, since he has
> 
>    (x : Squash A) -> B x   isomorphic to    [x : A] -> B x

Ah, okay.

> You mean that if you had the projections (mod.T is not exactly right,
> but in essence)
> 
>    Z : mod -> mod.T
>    S : mod -> mod.T -> mod.T
>    iter : ...
> 
> Then
> 
>    Z nat_mod : Nat
>    S nat_mod : Nat -> Nat
> 
> I see, then compile-time erasure is again not possible.

Yes, something like this.

> Thanks, this shows that my idea of first-class irrefutable patterns
> and erasure is flawed.
> Indeed, it does not work:
> 
>    snd : (exist a b : Exists A B) -> B a
> 
> is illtyped.  We have to show
> 
>    (exists a b : Exists A B) |- B a : Set
> 
> which simplifies to
> 
>    [a : A], b : B a |- B a : Set
> 
> which gives a type error since a is irrelevant and cannot appear in B
> a.  (Also the context is ill-formed).
> So I should drop this idea, at least for compile-time erasure.

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.)

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

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.

-- Dan