The Coq mailing list

["J. Ian Johnson" <ianj AT ccs.neu.edu>]

No, you're talking about negative occurrences always being bad. I'm talking 
about a new dimension to types that would safely allow use in a negative 
position. Some restriction to parametricity might make this legal. Really 
this is a pipe dream from my frustrations with splitting out specification 
and implementation only to learn that the type system doesn't have the 
facilities for the kind of abstraction I need. Unfortunately I don't have a 
completely formal solution yet, since this area of research is fairly 
tangential to my current work.
-Ian
----- Original Message -----
From: "Arthur Azevedo de Amorim" 
<arthur.aa AT gmail.com>
To: "J. Ian Johnson" 
<ianj AT ccs.neu.edu>
Cc: "gallais @ ensl.org" 
<guillaume.allais AT ens-lyon.org>,
 
coq-club AT inria.fr
Sent: Sunday, October 7, 2012 4:51:08 PM GMT -05:00 US/Canada Eastern
Subject: Re: [Coq-Club] Indices in mutual inductives

Yeah, the example wasn't very good; I just wanted to get the simplest
example that would work out.

On Fri, Oct 5, 2012 at 11:21 AM, J. Ian Johnson 
<ianj AT ccs.neu.edu>
 wrote:
> True, I had meant to say that the type was empty.
> Generally, I think that think kind of definition should be okay, since the 
> non-strictly positive occurrence is "treated positively" in the same way 
> that the recursive structure of a closure might have a non-strictly 
> positive occurrence for the type of the dictionary's values, but due to the 
> treatment by the dictionary, this circularity must always bottom out.
>
> concretely:
> Inductive Value : Type :=
> | closure : lambda-expr -> (dictionary Variable Value) -> Value
>
> To make the metatheory work out, there need to be positivity annotations on 
> type arguments, but I haven't given much thought into the deeper meaning of 
> this (gotta graduate).

Doesn't this happen already? If a type parameter has a negative
occurrence, then Coq will forbid some uses of the inductive, like this

Inductive foo T := Foo : (T -> bool) -> foo T.
Inductive bar := Bar : foo bar -> bar.

This definition will correctly be rejected because T occurs negatively in foo.

> My high level feeling is that it should work, but it could make recursion 
> very hard to prove terminating (though would make many programming patterns 
> I use in daily life actually possible).
>
> -Ian
>
> ----- Original Message -----
> From: "gallais @ ensl.org" 
> <guillaume.allais AT ens-lyon.org>
> To: "J. Ian Johnson" 
> <ianj AT ccs.neu.edu>
> Cc: "Arthur Azevedo de Amorim" 
> <arthur.aa AT gmail.com>,
>  
> coq-club AT inria.fr
> Sent: Friday, October 5, 2012 11:10:49 AM GMT -05:00 US/Canada Eastern
> Subject: Re: [Coq-Club] Indices in mutual inductives
>
> Well, this is just saying that B is empty. But it's usually ok to
> define empty sets!
>
> Inductive B : Set :=
>   BIntro : B -> B.
> Fixpoint omega (b : B) : False := match b with
>   BIntro b' => omega b'
> end.
>
> --
> gallais
>
>
> On 5 October 2012 16:00, J. Ian Johnson 
> <ianj AT ccs.neu.edu>
>  wrote:
>> Fixpoint omega (b : B) (a : A b) : False :=
>>  match a with
>>  | AIntro (BIntro b'' a') => omega b'' a'
>>  end.
>>
>> ----- Original Message -----
>> From: "Arthur Azevedo de Amorim" 
>> <arthur.aa AT gmail.com>
>> To: 
>> coq-club AT inria.fr
>> Sent: Friday, October 5, 2012 10:42:20 AM GMT -05:00 US/Canada Eastern
>> Subject: [Coq-Club] Indices in mutual inductives
>>
>> Dear list,
>>
>> Coq rejects the following definition
>>
>> Inductive A : B -> Type :=
>> | AIntro : forall b, A b
>>
>> with B : Type :=
>> | BIntro : forall b (a : A b), B
>> | Base : forall b, B.
>>
>> Is there any metatheoretical reason for this? Does anyone have an
>> example showing that it would make the logic inconsistent?
>>
>> Thanks
>>
>> --
>> Arthur Azevedo de Amorim



-- 
Arthur Azevedo de Amorim