[Agda] Positive but not strictly positive types

[Frédéric Blanqui]

Hello.

Le 10/04/2015 17:19, Aaron Stump a écrit :
> Hello, Frédéric.  Thanks for this interesting information about Coq.  
> I have a couple follow-up questions if you don't mind:
>
> -- So are you saying that Coq could allow nonstrictly positive small 
> inductive types?
Yes. You can have a look at:
http://iospress.metapress.com/content/tf54nwg673hvgk5d/
or https://who.rocq.inria.fr/Frederic.Blanqui/fi05-pdf.html

>   It seems it currently does not, as this one is rejected, for example:
>
> Inductive Cont (A:Prop) : Prop :=
>   D : Cont A
> | C : ((Cont A -> A) -> A) -> Cont A.
>
Unfortunately, yes, mainly for technical reasons I guess. This would 
require to restrict pattern-matching definitions so that they can be 
encoded into recursors, or upgrade the Coq termination checker to 
size-based termination since the structural subterm ordering is defined 
for strictly positive types only and cannot handle non-strictly positive 
types...

> -- is it necessary to forbid large eliminations with big inductive 
> types due to the Coquand-Paulin example we have been discussing (in 
> addition to forbidding nonstrictly positive big inductive types)?
> Or is there another example that shows the problem with large 
> eliminations and big inductive types?
> Sorry if these things are already explained somewhere in 
> theories/Logic/ in the Coq library...
>
I know no other counter-example but current (sufficient) termination 
conditions require so.

Frédéric.

> Thanks,
> Aaron
>
> On 04/10/2015 01:40 AM, Frédéric Blanqui wrote:
>> 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
>>
>> _______________________________________________
>> Agda mailing list
>> Agda at lists.chalmers.se
>> https://lists.chalmers.se/mailman/listinfo/agda
>