[Agda] Re: [Coq-Club] Re: Universe Polymorphism

[Jean-Philippe Bernardy]

On Fri, Sep 17, 2010 at 9:28 AM, Dan Doel <dan.doel at gmail.com> wrote:
> On Friday 17 September 2010 1:52:43 am Jean-Philippe Bernardy wrote:
>> > Including extending the erasure/irrelevance stuff to inductive types,
>> > erasability analysis (which may or may not be what you asked for later in
>> > your mail), and thoughts on proof irrelevance (although, I'm personally
>> > not convinced that this sort of erasability captures that notion
>> > precisely).
>>
>> Can I ask you to elaborate on why you think that erasability does not
>> mean irrelevance?
>
> Because that is not the type of irrelevance modeled by erasure pure type
> systems. Rather, they model parametricity, or a divide between static and
> dynamic portions of a program. For this particular form of erasure, it is not
> enough that there be only one canonical value for the dynamic portions of the
> program to look at. Rather, the dynamic portion must not look at the value at
> all.
>
> For instance, the standard intensional equality type:
>
>  data _==_ {A : Set} (x : A) : A -> Set where
>    refl : x == x
>
> the type of substitution given in the thesis is ((x : T) => U) is erasable
> quantification):
>
>  subst : (A : Set) => (P : A -> Set) => (x y : A) => x == y -> P x -> P y

To me subst should live in the area of Propositions:

subst : (A : Set) -> (P : A -> Prop) -> (x y : A) -> x == y -> P x -> P y

In that case there is no issue of relevance (the target is in Prop).

You may want a "converter" though:

>  conv : (A : Prop) -> (P : A -> Set) -> (x y : A) -> x == y -> P x -> P y

(_==_ is in Prop)

In that case I believe that there is no issue of parametricity;
because P is "irrelevant"
in A.

And, yes, you can have:

data Nat : Prop where
  ...

data Vec (A : Set) : Nat -> Set where
 ...

(Because Vec does not analyse Nat indices)

So, you can use conv to convert from Vec m to Vec n if m == n.

>> To make sure, even in Coq, Props are NOT intrinsically relevant. Consider

> But, the point is that for something to be proof irrelevant with respect to
> Set in Coq, that something must have type Prop. The point of an EPTS is to be
> able to treat the same type as either relevant or irrelevant in diffrent
> places, depending on how you quantify over it.

My point is the following: the chief benefit of the EPTS is to avoid
duplication of code
in Prop/Set. There is a time-tried solution to avoid duplication:
parametrization. In this instance,
it means to extend universe polymorphism to parameterize also on the
"relevant/irrelevant" aspect.
I believe that this solution is to be attempted before adding
seemingly ad-hoc constructs.

>> > So, I thought it would be similarly nice if one could make universe
>> > polymorphism always parametric while not making any types intrinsically
>> > irrelevant.
>>
>> Why would that be? The intention for Levels is that they are /always/
>> irrelevant with respect to programs.
>
> Because it could conceivably be useful to write normal functions involving
> Levels, while ensuring that its use in universe polymorphism is parametric.
> For instance, consider:
>
>  module M (a b c : Level) (T : Set (a ⊔ b ⊔ c)) where
>    up : Level → Level
>    up d = a ⊔ b ⊔ c ⊔ d
>
>    U : ∀{i} → Set i → Set (up i)
>    U A = A × T
>
> We can avoid writing the big lub expression several times by writing a
> function targeting Level, but we may not be able to write such a function if
> we're adamant about restricting functions in and out of Level. I suppose there
> is a PTS scheme for allowing Level -> Level but not Nat -> Level, but why not
> also allow Nat -> Level if we have tools for ensuring proper parametricity
> even while doing so.

You may have Nat -> Level. That would remain in the
Level/Irrelevant/Prop-like area.
Parametricity would not break as long as there is no elimination Nat ~> Level.

> Or, if you want to get even more radical (not that I'm suggesting this), Level
> isn't necessary at all if you have parametric quantification. It is, after
> all, just a natural numbers type that has been split off so that it can be
> given special, more restrictive rules. It is a perfect example of the kind of
> duplication that EPTSes are trying to avoid by not tying erasure to particular
> types. You could make Set indexed by Nat, and allow:

Indeed, Levels are just another copy of Nats in another irrelevance area.
They are not necessary if you can parameterize by irrelevance area.

Thanks for you thoughtful answer!
-- JP.