6
$\begingroup$

I'm wondering, are there small dependent calculi that can simulate a language with inductive families (that is, has a type isomorphic to each inductive family, at least as powerful of induction principles).

For example, I'm thinking:

  • You can use propositional equality to turn an inductive family into an inductive type with equality constraints on the indices
  • You can use Sigma types to encode sums-of-products
  • You can get inductive types with a fixed-point type:

    data Fix : (Type -> Type) -> Type where Fold : (f : Type -> Type) -> f (Fix f) -> Fix f

    which is fine as long as f is strictly positive.

But I'm not certain that these give you the full power of inductive families, particularly whether Fix gives you the full power of eliminators/structural recursion for inductive families.

Are there any references on what is sufficient to model inductive families?

I'm aware of:

  • W-types, which don't work well in an intensional setting.
  • Church-encodings, which aren't powerful enough to prove that (0 != 1), and also don't work well in a predicative setting
  • Levitation/datatype-generic-programming, which seems to give you all of inductive families, but at the expense of having to keep a runtime representation of every type, with a lot of complexity related to this representation. This seems like a chainsaw where I need a knife.
$\endgroup$
  • 2
    $\begingroup$ Not sure what are your constraints (e.g. what you'd consider as minimal, and also your Fix breaks consistency), but my calculus of united constructions might give you some ideas (it's likely not "minimal" in your sense). $\endgroup$ – Stefan Sep 30 at 19:47
  • 2
    $\begingroup$ Unless you make your requirement for a "minimal" type system more precise, the answer is "the minimal necessary type theory to model inductive families is type theory with inductive families". $\endgroup$ – Andrej Bauer Oct 1 at 7:08
  • $\begingroup$ @AndrejBauer I guess what I really mean is "finite" or "fixed" i.e. is there a fixed set of type constructors I can have in my theory that will give me a language equivalent to one where I can define my own inductive families. Minimal really is just "smaller is better" i.e. levitation seems to fit what I'm doing, but it's rather large and complex, and I'm wondering if it can be done smaller. $\endgroup$ – jmite Oct 1 at 16:48
  • 1
    $\begingroup$ And I suppose you do not consider a formalization which allows the user to specify new inductive families to be a "fixed set of type constructors"? $\endgroup$ – Andrej Bauer Oct 1 at 20:54
  • $\begingroup$ @AndrejBauer exactly. Basically, I'm looking to have a closed theory I can reason about on paper, and then say "and this is equivalent to a theory in which users can define their own families" $\endgroup$ – jmite Oct 1 at 22:05
4
$\begingroup$

I am not 100% sure this is what you want, but assuming you are looking for a type theory with a closed set of type constructors, which can model inductive families, then what you want are indexed containers or dependent polynomial functors. What you should look at first is:

  1. Thorsten Altenkirch, Neil Ghani, Peter Hancock, Conor McBride and Peter Morris's 2014 draft Indexed Containers.

    This paper is an expanded version of Altenkirch and Morris's 2009 LICS paper. It is all formalized in Agda, and gives a set of codes for defining all the strictly positive families. If you need it, it also gives an interpretation of them into W-types (and M-types for coinductive families). This is probably what you want to look at first.

    It may also be worth looking at Containers: Constructing Strictly Positive Types by Michael Abbott, Thorsten Altenkirch and Neil Ghani for the non-dependent case.

Category theorists also invented this concept, which they dubbed dependent polynomial functors. The original paper, and some I found helpful for reading it are:

  1. Wellfounded trees and dependent polynomial functors by Nicola Gambino and Martin Hyland. TYPES 2003.

  2. Generalized Polynomial Functors Marcelo Fiore, ICALP 2012. There is a bit more logical intuition in this paper.

  3. A foundation for GADTs and inductive families: dependent polynomial functor approach. Makoto Hamana and Marcelo Fiore, WGP 2011. This paper shows how to interpret indexed families as polynomial functors.

Now, you might also ask whether or not inductive families are "the morally correct" syntax for indexed containers. The answer is: probably not, but this is because containers/polynomials are too rich to have an obvious syntax.

  • Tamara von Glehn's PhD thesis, Polynomials and Models of Dependent Type Theory, builds models of dependent type theory out of polynomial functors. This implies that the correct syntax for datatypes in type theory is type theory itself, and I just don't know how to connect that to language design. Someone should give it a try, though!

  • Pierre Hyvernat has an LMCS 2014 paper, A Linear Category of Polynomial Functors, which uses a different notion of morphism to give polynomials a monoidal closed structure. So perhaps datatype declarations should be written in a linear type theory?

$\endgroup$
  • $\begingroup$ I haven't gone through them exhaustively, but I think the problem with all these citations is that they are basically W-types. For instance, containers are a way of packaging/manipulating the parameters of a W-type. Those let you represent 'the right' trees, but they don't generally let you derive the induction principle for the inductive family you're representing without function extensionality, because 'first order' stuff from the family is represented as higher-order stuff in the (indexed) W-type. $\endgroup$ – Dan Doel Oct 7 at 23:57
  • $\begingroup$ So, one solution that I've seen (related to OTT work, I think) is to have a more complicated language that retains the first-orderness of the right pieces of an inductive family definition. But I think that's what's being rejected as "levitation/datatype-generic-programming," so I don't know what else to suggest. :) $\endgroup$ – Dan Doel Oct 7 at 23:58
  • $\begingroup$ I suppose the obvious other suggestion is to realize that the lack of function extensionality in intensional type theory is a defect that we know how to overcome without losing its nice properties, not a moral principle to hold to. $\endgroup$ – Dan Doel Oct 8 at 0:07

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.