[Agda] Terminology: inductive family

[Peter Dybjer]

Hi Conor,

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

The idea to implement "restricted" inductive families in Half and the
first version of Agda is due to Thierry, as far as I remember. ALF's
pattern matching was powerful, but never completely specified, and
therefore subject to possible abuse. It was in response to this situation
that Half's more protestant recursive families were introduced.

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

There were a number of concerns. Pattern matching with restricted families
was easier to implement and describe. They have simpler metatheory. The
connection with initial algebras is more direct. (Categorical principles
tend to be good guidelines, cf Anton's remark about final coalgebras and
codata.)

In those days (late 80s and early 90s) we (I guess I should speak for
myself) were very concerned about extending Martin-Löf type theory only in
ways which were in the spirit of Martin-Löf. The somewhat elusive notion
of "constructive validity" and adherence to his "meaning explanations" was
more present in the discussions than today. Such thoughts pushed in the
"protestant" direction.

Today it seems more and more difficult to reconcile the wish for a small
very clean system which is suitable as a foundation of constructive
mathematics, and a dependently typed programming language such as Agda
which is convenient for programmers. It should be possible to reconcile
the two, but it remains to be done.

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

I'm not sure I have that much to say. There are some ideas that are
written down in the papers on inductive and inductive-recursive
definitions, and there are other versions which were implemented in
various proof-assistants. Apart from that there are a number of
possibilities which were only given a fleeting thought, but neither
implemented nor analyzed theoretically. For example, a possible middle
way, between "general" and "restricted", is to allow only inductive
families where indices range over "constructor patterns". Maybe we should
call these families "Anglican".

We should also not forget "John Major equality" as another possible
extension not covered by the original schema for inductive familes.

It may be worth-while asking ourselves what are the underlying concerns
which make us choose a particular definition of "inductive family"?

I think the prevailing attitude in the "Agda-community" is to allow as
general as possible class of inductive families. It should of course be
correct, firstly in the sense of Martin-Löf style meaning explanations,
and secondly, in the sense that decidability of type-checking is
preserved. But otherwise, anything goes. Or?

>From a theoretical-foundational point of view this is not a viable
attitude however. A foundation for constructive mathematics must be simple
and clear, and possible to subject to full metamathematical analysis.

Thierry often maintains that clarity and simplicity is important for the
system implemented by a proof assistant too. But it is worth-while asking
exactly what it a suitable balance between the simplicity of a system and
convenience for programmers. Exactly when is it worth-while giving up a
perfectly correct principle for the benefit of such overall simplicity?

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

This sounds somewhat along the lines of what you would do if you wanted to
give semantics for these definitions in terms of classical set-theoretic
monotone inductive definitions. This is another worth-while project.

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

I agree.

Cheers,
Peter