16
$\begingroup$

This question is from @TaliaRinger:

Are mutually inductive types and plain old inductive types equally expressive? (Say, in Coq.)
I assume yes, but the motive for induction will be a huge mess. But I don't know the corresponding transformation, so I may be wrong.

And as followups: Are nested and regular inductives equally expressive? If not, are mutual and nested inductives?

The replies in the Twitter thread suggest that mutual inductives can be encoded using regular inductives; I'm wondering if the induction principles would be the "same".

I also have a suspicion that nested inductives are not encodable as regular inductives since something like nested inductives' deep induction principles seem a lot more complex.

$\endgroup$
3
  • $\begingroup$ Are you asking 'are inductive-inductive types encodable by inductive types'? $\endgroup$
    – ice1000
    Mar 1, 2022 at 20:40
  • $\begingroup$ No, just mutual inductives, where the types of constructors can mutually refer to each other's inductive types, e.g. @pigworker's Even/Odd example down below $\endgroup$
    – ionchy
    Mar 1, 2022 at 20:42
  • $\begingroup$ BTW this question came from a student in my class (not sure if they want credit or not, and FERPA is a thing) $\endgroup$ Mar 1, 2022 at 21:49

3 Answers 3

17
$\begingroup$

Adopting Agda-ish notation, the basic strategy is to turn your bunch of mutually defined inductive types into a single inductively defined universe, indexed over its collection of sorts. Let's do the classic example.

BEFORE

mutual
  data Even : Set where
    zero : Even
    suco : Odd -> Even

  data Odd  : Set where
    suce : Even -> Odd

AFTER

data Sort : Set where
  even odd : Sort

data Stuff : Sort -> Set where
  zero : Stuff even
  suco : Stuff odd -> Stuff even
  suce : Stuff even -> Stuff odd

Even = Stuff even
Odd  = Stuff odd

To do mutual induction over Even and Odd, you need to provide two motives, PE : Even -> Set and PO : Odd -> Set. To do induction over stuff, you need to provide a motive P : (s : Sort) -> Stuff s -> Set, but you can always take

P even = PE
P odd  = PO

It really is the same stuff, differently packaged.

What about more generally? If you have n types mutually defined types Foo_i : Ix_i -> Set, you can define

data Sort : Set where
  foo_1 : Ix_1 -> Sort
  ...
  foo_n : Ix_n -> Sort

(or you can take Sort to be a dependent pair whose first component is a tag) and then

data Foo : Sort -> Set where
  ... -- turn Foo_i x into Foo (foo_i x) wherever you see it

What can't you do this way?

  • mutual induction and coinduction: that hierarchy does not collapse;
  • induction-induction: if any Ix_j mentions some Foo_i, you will struggle to construct Sort; the usual trick is again to echo type systems by defining "raw" things with extra junk, then pick out "good" raw things; if you have enough proof-irrelevance, it's equivalently expressive.

As far as "nested" types (i.e., types with large indices, possibly even invoking themselves in recursive positions), the usual trick to get back to mere indexing is defunctionalisation. The classic example is

BEFORE

data Term (X : Set) : Set where -- X is an *index*, even though left of :
  var : X
  app : Term X -> Term X -> Term X
  lam : Term (Maybe X) -> Term X

AFTER

module _ (X : Set) where -- yes, it really is a *parameter*

  Var : Nat -> Set
  Var zero    = X
  Var (suc n) = Maybe (Var n)

  data Term (n : Nat) : Set where
    var : Var n -> Term n
    app : Term n -> Term n -> Term n
    lam : Term (suc n) -> Term n

Again, the trick is to construct a local small universe closed under all the operations which vary the types in the various index positions of recursive invocations of the original nested type.

Of course, if you encode what is happening in type indices as data, then you acquire a kind of typecase, so there is no guarantee that you get exactly the same expressivity. But you do get the same data.

$\endgroup$
4
  • $\begingroup$ So we can encode 2 mutual inductive types and get mutual induction, but we do not get mutual induction of we encode >2 mutual inductive families? Did I understand that correctly? $\endgroup$ Mar 2, 2022 at 8:11
  • $\begingroup$ I feel it'd also be worth adding an example of an inductive-inductive type which can't be encoded as an inductive type. It's easy to confuse induction-induction with mutual induction. $\endgroup$
    – James Wood
    Mar 5, 2022 at 8:59
  • 1
    $\begingroup$ I believe now you meant that the encoding does not work for mutual inductive and coinductive types (both at the same time). Does a similar encoding work for mutual coinductive types (only) though? $\endgroup$ Mar 31, 2022 at 7:21
  • $\begingroup$ @AlberttenNapel ideally you'd have direct support for indexed record types but I'm not sure why it wouldn't work for mutual coinductive types as long as you use equality to discriminate CoInductive foo A := { fst: forall C D, A = C * D -> C ; .. $\endgroup$ Mar 31, 2022 at 22:44
10
$\begingroup$

There is a fairly general way of turning a mutual inductive into a single inductive which is reminiscent of defunctionalization. This can also be extended to handle nested inductives. A different formal answer can be found in Representing Nested Inductive Types using W-types.

Here's a mutual inductive type for example:

Inductive a : Type :=
| ca : b 0 -> a
with b : nat -> Type :=
| cb : forall n, a -> b n.

First define a sum type with one constructor for each mutually defined type constructor, carrying their indices.

Inductive ix : Type :=
| A : ix  (* a has no parameters *)
| B : nat -> ix.

Then the mutually inductive types can be reexpressed as a type indexed by ix:

Inductive eval : ix -> Type :=
| ca : eval (B 0) -> eval A
| cb : forall n, eval A -> eval (B n).

(* a = eval A *)
(* b n = eval (B n) *)

Induction for that eval type uses a single motive indexed by ix, which is equivalent to having a motive for a and a motive for b.

For a nested inductive type...

Inductive tree :=
| ctree : list tree -> tree.

... you can defunctionalize not only the recursive type itself, but also other types involved in the recursion:

Inductive ix : Type :=
| Tree : ix
| List : ix -> ix.

Inductive eval : ix -> Type :=
| ctree : eval (List Tree) -> eval Tree
| nil : eval (List Tree)
| cons : eval Tree -> eval (List Tree).
```
$\endgroup$
7
  • 1
    $\begingroup$ I took a glance at the paper you linked and it sounds like they're doing this within extensional MLTT. Is this possible in an intensional theory? I seem to remember there was some sort of problem with the induction principles when it comes to encoding with W types intensionally. $\endgroup$
    – ionchy
    Mar 1, 2022 at 19:33
  • 1
    $\begingroup$ It's actually possible to construct inductive types using W types in intensional type theory. Probably not recommended, but possible. $\endgroup$
    – Dan Doel
    Mar 1, 2022 at 19:47
  • 1
    $\begingroup$ It seems like this might come down to construction of indexed W-types from plain W-types. The usual encoding picks out the properly indexed trees from a larger type of trees, and it's not clear to me how to characterize the 'canonical' values in a way that works out appropriately. It's possible that's just very complicated, though. $\endgroup$
    – Dan Doel
    Mar 1, 2022 at 22:07
  • 1
    $\begingroup$ CIC allows fancy nested types where the type being defined can appear as an indice of a nesting inductive. A minimal example is Inductive T := Leaf : T | Node : forall t1 t2 : T, eq T t1 t2 -> T. I do not know how to encode those things without (a weak form of) induction-induction. $\endgroup$ Mar 1, 2022 at 22:41
  • 2
    $\begingroup$ Here is your tree example in the Why not W? style, starting from indexed W-types. $\endgroup$
    – Dan Doel
    Mar 2, 2022 at 1:37
6
$\begingroup$

A lot of these topics are covered in Bruno Barras' habilitation thesis (http://www.lsv.fr/~barras/habilitation/) which, I think, is an interesting read for advanced Coq users.

See in particular section 8.6 "Advanced features of inductive types" on p136 & following:

  • 8.6.1 Recursively non-uniform parameters
  • 8.6.2 Nested inductive types
  • 8.6.3 Mutual inductive definitions in different sorts
$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

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