The Coq mailing list

[Matthieu Sozeau <mattam AT mattam.org>]

Hi Jonathan,

  you are right that having only the equality type as indexed

gives you theoretically the same expressivity.

This has been explored for example in the following two papers on the 

construction of indexed inductive types:

Peter Morris and Thorsten Altenkirch. Constructing strictly positive families. CATS ’07 Proceedings of the thirteenth Australasian symposium on Theory of computing, pages 111– 121, 2007. 10 

Peter Morris, Thorsten Altenkirch, and Neil Ghani. A universe of strictly positive families. IInternational journal of foundations of computer science, pages 83–107, 2009.

For a variation on these ideas to present Coq, see Spiwack and Herbelin's

"The Rooster and the Syntactic Bracket":

http://arxiv.org/abs/1309.5767

So, you're in good company.

-- Matthieu

On Wed, Mar 23, 2016 at 3:47 AM Jonathan Leivent <jonikelee AT gmail.com> wrote:

On 03/22/2016 02:37 PM, Cedric Auger wrote:
>
> 2016-03-21 20:03 GMT+01:00 Jonathan Leivent <jonikelee AT gmail.com
> <mailto:jonikelee AT gmail.com>>:
>
>      Is it true in Coq that any index on an inductive type could *always* be
>      replaced by a type parameter with an extra equality-typed field added to
>      each constructor tying the type parameter to that constructor's value for it?
>
> ...
>
>
> ​I think it is always the case. One cannot prove it directly in Coq as we would
> have to use "meta"functions taking a type as argument, and inspect its ​
> construction to build an other one which would be isomorphic.

Thanks.  I did not expect it to be provable in Coq.  I was just
wondering if, by avoiding type indexes, I'd eventually find a good
reason to have kept them.

> ...
>
>
> ​Now I tend to avoid that kind of annoyance with an other approach:
>
> Inductive finS(X:Set) : Set :=
> | Fin1
> | FinS : X -> finS X.
>
> Fixpoint fin(m:nat) : Set :=
>     match m with​
> ​  | O => emptySet​
>     | S n => finS (fin m)
>     end.
>
> I find this kind of type quite convenient to use. "inversion f." becomes
> "destruct n; destruct f." with no weirdness to deal with.
> Induction is done on the parameter rather than the type, and all basic operation
> have their counterparts in a not too artificial way.
>
> I find it nice to have the ability to "reduce" the type to only those which are
> possible in a given context.
>
> I am conscious on the fact that such a transcription of type is not always
> trivially existent, but in many cases, there is a strong relation between the
> constructor of the type and the constructors of the index, leading to a natural
> way to make it.
> Cases which do not apply still, are those where the index is not a constructed
> type (and I don’t pretend this to be the only case).
> Example: Inductive is_identity {A:Type} : (A->A)->Prop := Id : is_identity (fun
> x => x).
>

This construction is interesting, but not useful in most of my cases.
The issue is that I want the type parameters and indexes to vanish via
Extraction along with all trace of their trails through the code, and
incorporating one as a match discriminee will likely prevent that.

-- Jonathan