The Coq mailing list

[Thorsten Altenkirch <Thorsten.Altenkirch AT nottingham.ac.uk>]

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-request AT inria.fr> on behalf of roux cody <cody.roux AT gmail.com>
Reply-To: "coq-club AT inria.fr" <coq-club AT inria.fr>
Date: Tuesday, 3 July 2018 at 22:37
To: "coq-club AT inria.fr" <coq-club AT 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 <xlk AT 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 <Ralph.Matthes AT 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.