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

[Jean-Philippe Bernardy]

On Mon, Sep 20, 2010 at 12:07 AM, Dan Doel <dan.doel at gmail.com> wrote:
> On Sunday 19 September 2010 10:13:04 am Jean-Philippe Bernardy wrote:
>> On Fri, Sep 17, 2010 at 9:28 AM, Dan Doel <dan.doel at gmail.com> wrote:
>> >  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.
>
> The first of these is (in a sense) a special case of the type I gave.

Yes.

>> And, yes, you can have:
>>
>> data Nat : Prop where
>>   ...
>>
>> data Vec (A : Set) : Nat -> Set where
>>  ...
>>
>> (Because Vec does not analyse Nat indices)
>
> I don't think I believe this explanation given your explanation of the conv
> type. The reason conv was safe was that P itself was irrelevant in its Prop
> parameter, which I presume means that P x is the same type regardless of what
> x is.

It seems that much of the confusion comes from the multiple meanings
of the phrase
"are the same". In this case P x and P y 'are the same' only after
projection to their
computational interpretation (the one where x and y are erased -- not
a big surprise).

>> So, you can use conv to convert from Vec m to Vec n if m == n.
>
> this is suspect given the rules for proof irrelevant equality: if this Nat :
> Prop is analogous to Sq Nat in an EPTS, then all elements of it are equal. But
> this would be bad, because if 5 == 7 via proof irrelevence, we should be able
> to cast from Vec A 5 to Vec A 7, which isn't what we'd expect.

The _==_ you use in the above is the one from the type of conv.
It lives in Prop, thus its arguments are relevant for that equality (because
everything is i Prop). So, 5 == 7 is false. We're safe :)

>> 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.
>
> I don't see what is ad-hoc about EPTS. They are related to modal logics via
> Curry-Howard.

I guess I'm biased against modal logics :). "My" system is just a usual
PTS+data, only with more sorts.

> One might equally argue that tying the erasability of terms to their type
> (which even a parameterized Prop/Set distinction does) is ad-hoc. For
> instance, suppose we have x : Nat : Set, and we need to fill a hole that
> expects a Nat : Prop. An EPTS would allow this due to the modal rules (in
> modal logic, you'd get P -> <>P). What do we do in a type-based solution?
> Introduce a subtyping relation, Nat : Set < Nat : Prop? Or is this just not
> allowed?

There is elimination in the Set ~> Prop direction. Therefore there is
a (trivial) conversion function from Nat : Set to Nat : Prop.

> No problem. I'm pretty interested in this stuff.

Thanks again,
JP.