[Agda] Positive but not strictly positive types

[Aaron Stump]

Hi, Vilhelm.

It's really great you wrote this up in Coq and put up the blog post 
about it.  I think that is quite valuable.  One small point, though, 
that does not come through clearly (to me): the example from the Coquand 
and Paulin Colog '88 paper is given in Luo's ECC extended with inductive 
types.  That is, the type theory needed for the example has a sort for 
impredicative quantifications, and then a hierarchy of sorts allowing 
only predicative quantification above that.  So the example would not 
type-check (unmodified) in CIC as defined in Werner's dissertation 
(which, if I make my way through the French correctly, extends CC with 
inductive types, not ECC).

So it is really the interaction of non-strictly positive types, an 
impredicative sort, and a predicative hierarchy above that which leads 
to the inconsistency.  One might be free to reject one of those and keep 
the other two.  For example, I have a proof of consistency for a system 
which drops the predicative hierarchy but retains non-strictly positive 
types and an impredicative sort (I believe this is along the lines 
Thierry Coquand suggested on this mailing list some time back).

One might also be interested in whether non-strictly positive types and 
the predicative hierarchy (but no impredicative sort) would be 
susceptible to the Coquand-Paulin example.  If not, then maybe Agda 
could allow non-strictly positive types.  I don't know if more is known 
on this option -- but would love to hear if someone does.

Cheers,
Aaron

On 04/09/2015 11:07 AM, Vilhelm Sjöberg wrote:
> On 2015-04-09 11:49, Andrés Sicard-Ramírez wrote:
>> Retaking the discussion in
>> http://thread.gmane.org/gmane.comp.lang.agda/6008, it's known that
>> using *negative* types it's possible
>>
>> a) to prove absurdity or
>> b) to write non-terminating terms.
>>
>> Is there some example in *Agda* of a positive but not strictly
>> positive type which allows a) or b)?
> I'm interested in the answer to this question also. If I correctly 
> understand what Thierry Coquand wrote in the thread you mention, the 
> answer is no; because Agda is predicative allowing positive datatypes 
> would be sound. But it would be interesting to see this fleshed out more.
>
> I wrote up a blog post about using non-strictly positive datatypes to 
> get a paradox in Coq: 
> http://vilhelms.github.io/posts/why-must-inductive-types-be-strictly-positive/
>
> Vilhelm
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda