[Coq-Club] Proposition for strictly positive occurrence

[Yixuan Chen]

Dear Coq users,

I met a situation where I need to define an inductive type like,

Context (f: Type -> Type).
Inductive foobar: Type :=
| something_of: (f foobar) -> foobar
| nothing: foobar.

This does not pass the positive occurrence check, and it shouldn’t. However, the actual definition that would be passed as f should always guarantee to generate only legitimate types. Is there a way to write “strictly positive occurrence” as an proposition in Coq and make it as an hypothesis for f in the client and proved by the provider(s) of f? Thanks.

Best Regards,
Yixuan (Luke) Chen

[Yixuan Chen]

Dear Ralph and Dan,

Thanks for your suggestions. It seems like the problem is much more complicated than I expected to be :( I might just take a detour to avoid the problem for now, but I will take a look into your suggestions later. Anyway, thanks a lot!

Dear Yixuan Chen,
Your question refers to a very old problem of Coq. It is just not possible to do categorical datatypes there in a generic fashion. One would like to speak about an arbitrary "functor" f and later use the generic construction in concrete instances that would even mostly be strictly positive. But this is not supported by Coq.
I have written papers where I suggested other recursion schemes that would work - even in Coq - for a class of f that is far more liberal than strict positivity (see my papers in JFP and SCP). The requirement for that class can be encapsulated logically, as you described in your post.
You can also switch off the checks, see the benefits of it in my TYPES'18 talk (in particular the second last slide of it), available at https://types2018.projj.eu/conference-programme/#session8 - move two lines up there and click on the title of the talk.
Kind regards,    Ralph Matthes

Post by Yixuan Chen
Dear Coq users,
I met a situation where I need to define an inductive type like,

Context (f: Type -> Type).
Inductive foobar: Type :=
| something_of: (f foobar) -> foobar
| nothing: foobar.

This does not pass the positive occurrence check, and it shouldn’t. However, the actual definition that would be passed as f should always guarantee to generate only legitimate types. Is there a way to write “strictly positive occurrence” as an proposition in Coq and make it as an hypothesis for f in the client and proved by the provider(s) of f? Thanks.
Best Regards,
Yixuan (Luke) Chen

[roux cody]

Ralph is a black belt at this kind of thing, so I suspect his advice is
very valuable.

There are a couple of cheap tricks that may work in certain circumstances,
though. Here is one:

Context (f : Type -> Type).

Fixpoint foobar_n (n : nat) : Type :=
match n return Type with
| 0 => False
| S m => f (foobar_n m)
end

Definition foobar := { n : nat & foobar_n n}.

If the type function f is very well behaved, you may be able to do
something with (foobar f). I've used it successfully in the case where f is
a monotone functional with reasonable properties.

Best,
Cody

Post by Yixuan Chen
Dear Ralph and Dan,
Thanks for your suggestions. It seems like the problem is much more
complicated than I expected to be :( I might just take a detour to avoid
the problem for now, but I will take a look into your suggestions later.
Anyway, thanks a lot!
Dear Yixuan Chen,
Your question refers to a very old problem of Coq. It is just not possible
to do categorical datatypes there in a generic fashion. One would like to
speak about an arbitrary "functor" f and later use the generic construction
in concrete instances that would even mostly be strictly positive. But this
is not supported by Coq.
I have written papers where I suggested other recursion schemes that would
work - even in Coq - for a class of f that is far more liberal than strict
positivity (see my papers in JFP and SCP). The requirement for that class
can be encapsulated logically, as you described in your post.
You can also switch off the checks, see the benefits of it in my TYPES'18
talk (in particular the second last slide of it), available at
https://types2018.projj.eu/conference-programme/#session8 - move two
lines up there and click on the title of the talk.
Kind regards, Ralph Matthes
Dear Coq users,
I met a situation where I need to define an inductive type like,
Context (f: Type -> Type).
Inductive foobar: Type :=
| something_of: (f foobar) -> foobar
| nothing: foobar.
This does not pass the positive occurrence check, and it shouldn’t.
However, the actual definition that would be passed as f should always
guarantee to generate only legitimate types. Is there a way to write
“strictly positive occurrence” as an proposition in Coq and make it as an
hypothesis for f in the client and proved by the provider(s) of f? Thanks.
Best Regards,
Yixuan (Luke) Chen

[Thorsten Altenkirch]

A strictly positive datatype is given by a container, I.e.
S : Type
P : S -> Type
It's initial algebra is the W-type.

There is no point quantifying over all functors because functors don't always have initial algebras.

Thorsten

From: <coq-club-***@inria.fr<mailto:coq-club-***@inria.fr>> on behalf of roux cody <***@gmail.com<mailto:***@gmail.com>>
Reply-To: "coq-***@inria.fr<mailto:coq-***@inria.fr>" <coq-***@inria.fr<mailto:coq-***@inria.fr>>
Date: Tuesday, 3 July 2018 at 22:37
To: "coq-***@inria.fr<mailto:coq-***@inria.fr>" <coq-***@inria.fr<mailto:coq-***@inria.fr>>
Subject: Re: [Coq-Club] Proposition for strictly positive occurrence

Ralph is a black belt at this kind of thing, so I suspect his advice is very valuable.

There are a couple of cheap tricks that may work in certain circumstances, though. Here is one:

Context (f : Type -> Type).

Fixpoint foobar_n (n : nat) : Type :=
match n return Type with
| 0 => False
| S m => f (foobar_n m)
end

Definition foobar := { n : nat & foobar_n n}.

If the type function f is very well behaved, you may be able to do something with (foobar f). I've used it successfully in the case where f is a monotone functional with reasonable properties.

Best,
Cody


On Tue, Jul 3, 2018 at 5:06 PM, Yixuan Chen <***@umich.edu<mailto:***@umich.edu>> wrote:
Dear Ralph and Dan,

Thanks for your suggestions. It seems like the problem is much more complicated than I expected to be :( I might just take a detour to avoid the problem for now, but I will take a look into your suggestions later. Anyway, thanks a lot!
On Jul 3, 2018, 9:19 AM -0400, Ralph Matthes <***@irit.fr<mailto:***@irit.fr>>, wrote:

Dear Yixuan Chen,

Your question refers to a very old problem of Coq. It is just not possible to do categorical datatypes there in a generic fashion. One would like to speak about an arbitrary "functor" f and later use the generic construction in concrete instances that would even mostly be strictly positive. But this is not supported by Coq.

I have written papers where I suggested other recursion schemes that would work - even in Coq - for a class of f that is far more liberal than strict positivity (see my papers in JFP and SCP). The requirement for that class can be encapsulated logically, as you described in your post.

You can also switch off the checks, see the benefits of it in my TYPES'18 talk (in particular the second last slide of it), available at https://types2018.projj.eu/conference-programme/#session8 - move two lines up there and click on the title of the talk.

Kind regards, Ralph Matthes


Le 03/07/2018 à 02:20, Yixuan Chen a écrit :
Dear Coq users,

I met a situation where I need to define an inductive type like,

Context (f: Type -> Type).

Inductive foobar: Type :=
| something_of: (f foobar) -> foobar
| nothing: foobar.

This does not pass the positive occurrence check, and it shouldn’t. However, the actual definition that would be passed as f should always guarantee to generate only legitimate types. Is there a way to write “strictly positive occurrence” as an proposition in Coq and make it as an hypothesis for f in the client and proved by the provider(s) of f? Thanks.

Best Regards,
Yixuan (Luke) Chen






This message and any attachment are intended solely for the addressee
and may contain confidential information. If you have received this
message in error, please contact the sender and delete the email and
attachment.

Any views or opinions expressed by the author of this email do not
necessarily reflect the views of the University of Nottingham. Email
communications with the University of Nottingham may be monitored
where permitted by law.