[Agda] Terminology: inductive family

[Conor McBride]

Hi Peter

On 9 Jun 2008, at 08:39, Peter Dybjer wrote:

> 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.

Many of us grew up in a wholly Catholic environment
(I speak only metaphorically): in the Coq and Lego
communities, "inductive family" did just mean the
"general" version. That was then.

[..]

>> 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.

Somehow, post-ALF, there seemed to be a very conscious
stepping away from general inductive families, around
about the same time I was beginning to have fun with
them. I wish I had a better handle on what the thinking
was behind that.

 From my current perspective, general inductive families
are just too intensional to sustain an extensional
propositional equality. Back then, though, it seemed to
me that the Chalmers position was to step away from
equality altogether, apart from those equalites which
could be constructed by computational means. I wish I
understood why this was: I can guess, and certainly
there were issues, but I'd rather ask openly what the
thinking was than project my own prejudice.

I realise that equality is the fourth topic to be
avoided in polite conversation, but one can only hold
it in for so long...

>
>> 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.

I really think it would be helpful to elaborate on
this remark.

[I just deleted a chunk which effectively tried
to second-guess the elaboration.]

I guess what I'm saying is that it would be a
useful community contribution (in which I'm very
happy to participate), to write, probably not for
publication, some sort of article which traces
the evolution of these issues, including the
directions abandoned. I certainly don't know
enough to write such a thing, but I'm keen to
gather the data.

>> 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.

Again, please elaborate!

> 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?

I've thought about them a bit (as Hank has just
said). Anton and I once had a go at constructing
them from types within the schema by the
following entirely traditional method
(I presume mutual definitions are available;
their indexed coding is standard):

  (1) Define mutual, non-indexed datatypes giving
    the raw syntax of your data: PreContext,
    PreType, etc...

  (2) Define mutual inductive families (restricted
    will do, because you can compute with indices)
    indexed by Pre-stuff, coding up the relevant
    syntax-directed "goodness" judgments. Ie,

      GoodContext : PreContext -> Set
      GoodType : PreConext -> PreType -> Set
      ...

  (3) Take

    Context = Sigma PreContext GoodContext
    Type (p, pg) = Sigma PreType (GoodType p)
    ...

  (4) Define the constructors, assembling goodness
    proofs for the whole from those for the parts.
    If you can't, you've messed up stage (2).

  (5) Prove the induction principle (I can think of
    at least two choices for what this should be,
    but it doesn't affect the outcome of this
    story). Here is where the wheel falls off. Why?

    You're given that the induction predicate (if
    that's an appropriate name, which I doubt)
    respects *your* constructors, but you need to
    show that it respects *any* constructors. It's
    strongly reminiscent of building datatypes from
    the W-type, in that respect. You need
    "uniqueness of goodness". If you have an
    entirely first-order definition, I suspect you
    can (a) construct a substitutive equality, even
    without the identity type, and (b) prove
    uniqueness of goodness by sheer hard work.
    Once you have higher-order data, lack of
    extensionality kills you.

[Enter, Observational Type Theory.] My hope is
that, firstly, an extensional propositional
equality will admit uniqueness of goodness
for higher-order definitions by sheer hard
higher-order work. But secondly, given the
variant of OTT with proof-irrelevant propositions,
we can make goodness propositional, obviating
the need for uniqueness by promising not to
look---the PreStuff gives us enough information
for computational purposes anyway.

That's pretty much as far as I've got at the
moment. It's still very sketchy. It does
rather suggest that these things are (1) a
quotient of stuff we have already and (2)
representable in extensional type theory
without too much bother. My guess is that
these...

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

..."inductive-inductive families", or
"telescopic inductive families", or what?,
will turn out to be a more intricate variant
of what we have already, but no bigger,
in terms of well-founded orderings.

There's a lot more work to do here, but it
does seem likely that sense can be made of
these things.

All the best

Conor