[Agda] Positive but not strictly positive types

[Frédéric Blanqui]

Hello.

Speaking of Coq: because Prop is impredicative, one usually 
distinguishes between:
1. small inductive types where Type-level constructor arguments are 
parameters
2. big inductive types

Coquand's counter-example is a big inductive type.

For this reason, strong elimination on big inductive types is forbidden 
in Coq.

Adding small inductive types preserves termination and logical 
consistency in system F or Fomega. A reference to Mendler's work has 
already been given. For some more recent works, see Abel et al. More 
generally, you can consider monotone types (positivity is a syntactic 
condition ensuring monotony): see Matthes and Uustalu works. Adding 
dependent types doesn't change anything.

So, there should be no problem in Agda.

Frédéric.


Le 09/04/2015 18:07, Vilhelm Sjöberg a écrit :
> 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