[Agda] Positive but not strictly positive types
Aaron Stump
aaron-stump at uiowa.edu
Fri Apr 10 17:19:23 CEST 2015
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? 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.
-- 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...
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
More information about the Agda
mailing list