Finite types, historical question

Miscellaneous
1

I have a historical question: When did indexed finite types

Inductive fin : nat -> Type :=
| Zero: forall n, fin (S n)
| Succ: forall n, fin n -> fin (S n).

appear first in Coq or elsewhere?

I checked Martin-Löf, but there finite types are obtained with n constructors, not just 2. The above definition appears in Chlipala’s CPDT. I did not find it in Coq’Art.

Related: When did the recursive version with option types appear first?

Fixpoint Fin (n: nat) : Type :=
  match n with
  | 0 => False
  | S n' => option (Fin n')
  end.

Thanks in advance. Gert

2

I am not sure it was the first time, but I remember seeing Conor McBride use them for one of his talks on epigram (it may have been at a Types meeting in Durham). It may be useful to ask him personally what was his inspiration.

Yves

3

Meanwhile I found the interesting paper

McBride C. (2005) Epigram: Practical Programming with Dependent Types. In: Vene V., Uustalu T. (eds) Advanced Functional Programming. Springer LNCS, vol 3622.

where Conor McBride describes indexed finite types together with vectors, among other interesting things. The related Coq library Coq.Vectors.Fin dates back to 2010 (which is 5 years later). Giménez and Castéran A Tutorial on [Co-]Inductive Types in Coq doesn’t mention general finite types.