[Agda] Terminology: inductive family

[Peter Dybjer]

Peter and Nisse,

I have also noted the way the terminology "inductive family" has evolved,
and reacted to this in a similar way as you.

I used the term for the title of my FACS 1994 paper, because I needed a
short form for "inductively defined indexed family of sets" which is quite
a mouthful. Although my aim was to delineate a class of definitions which
is both natural and general, it was clear from the beginning that there
were a number of choices that needed to be made. It was important to make
sure that the class of definitions was constructive in the sense of Per
Martin-Löf. One of the main arguments for the choice of definition was
that it was essentially a Curry-Howard interpretation of the definition of
inductive predicate that Per had in his "Hauptsatz for the intuitionistic
theory of iterated inductive definitions" 1971.

> Am I right in thinking that the term "inductive family"
> covers cases like the following T : A -> Set, defined in a context
>
> A : Set
> B : A -> Set
> C : (a : A)-> B a -> Set
> d : (a : A, b : B a)-> C a b -> A
>
> T (a : A) = data sup (b : B a) (f : (C a b)-> T (d a b c))
>
> ?

Yes, this is covered by the schema.

> After all, it is a family (set-valued function), and it
> is defined inductively (or more precisely, its values are
> defined by simultaneous induction).
>
> I used the word "covers" to suggest that there may be other
> definitions of things that one wishes to call inductive
> families, such as those in which each constructor is
> targeted on a particular "section" of the function domain,
> given as the range of a (vector of) function(s).
> In the above case, there happens to be one constructor "sup",
> but what is important is that it targets the whole function domain.
>
> I had thought that the qualifications "restricted" and
> "general" were invented (by Peter Dybjer and/or Anton?)
> to be used when one needs to be specific about the two
> forms of inductive family.  The distinction is
> important, in my opinion.

This distinction seemed important to us too. The "general" inductive
families are the ones of the original schema, whereas the "restriced"
inductive families correspond to what Thierry called "recursive" families
in Half and Agda. In the paper "Indexed induction-recursion" Anton and
suggested a way to make these two classes of inductive-recursive
definitions precise.

> I should not like to discourage anyone from thinking
> about the more liberal kind of inductive family, at least
> anyone who is prepared to acquire some mental scar tissue.
> But I *would* like to heavily discourage anyone from
> using the term "inductive family" as if it meant only
> the general form -- because it damages words, and words
> are all we have to communicate with.

I agree.

The above discussion started by the feeling that maybe the original schema
was too general. But there is also reason to believe that it is not
sufficiently general. For example, the definition of categorically
inspired internal syntax for type theory (cf my 1996 Internal Type Theory
paper) uses a definition not covered by the schema. We simultaneosly
define

Context : Set
Type : Context -> Set
Term : (G : Context) -> Type G -> Set
Subst : Context -> Context -> Set

etc.

I tacitly assumed that this is a constructively valid inductive definition
although it is not covered by the original schema. Other people have used
similar definitions, but as far as I know nobody has sorted out the
precise
syntax and semantics underlying such definitions. Is anyone aware of any
work in this direction?

It seems natural to use the term "inductive families" also for such
potential extensions.

Peter