key: cord-0054948-hmcba9i3
authors: Johann, Patricia; Polonsky, Andrew
title: Deep Induction: Induction Rules for (Truly) Nested Types
date: 2020-04-17
journal: Foundations of Software Science and Computation Structures
DOI: 10.1007/978-3-030-45231-5_18
sha: 1741958f96ada9d130ca045e29cba912cd4a1092
doc_id: 54948
cord_uid: hmcba9i3

This paper introduces deep induction, and shows that it is the notion of induction most appropriate to nested types and other data types defined over, or mutually recursively with, (other) such types. Standard induction rules induct over only the top-level structure of data, leaving any data internal to the top-level structure untouched. By contrast, deep induction rules induct over all of the structured data present. We give a grammar generating a robust class of nested types (and thus ADTs), and develop a fundamental theory of deep induction for them using their recently defined semantics as fixed points of accessible functors on locally presentable categories. We then use our theory to derive deep induction rules for some common ADTs and nested types, and show how these rules specialize to give the standard structural induction rules for these types. We also show how deep induction specializes to solve the long-standing problem of deriving principled and practically useful structural induction rules for bushes and other truly nested types. Overall, deep induction opens the way to making induction principles appropriate to richly structured data types available in programming languages and proof assistants. Agda implementations of our development and examples, including two extended case studies, are available.

This paper is concerned with the problem of inductive reasoning about inductive data types that are defined over, or are defined mutually recursively with, (other) such data types. Examples of such deep data types include, trivially, ordinary algebraic data types (ADTs), such as list and tree types; data types, such as the forest type, whose recursive occurrences appear below other type constructors; simple nested types, such as the type of perfect trees, whose recursive occurrences never appear below their own type constructors; truly 1 nested types, such as the type of bushes (also called bootstrapped heaps by Okasaki [16] ), whose recursive occurrences do appear below their own type constructors; and GADTs. Proof assistants, including Coq and Agda, currently provide insufficient support for performing induction over deep data types. The induction rules, if any, they generate for such types induct over only their top-level structures, leaving any data internal to the top-level structure untouched. This paper develops a principle that, by contrast, inducts over all of the structured data present. We call this principle deep induction. Deep induction not only provides general support for solving problems that previously had only (usually quite painful and) ad hoc solutions, but also opens the way for incorporating automatic generation of useful induction rules for deep data types into proof assistants.

To illustrate the difference between structural induction and deep induction, note that the data inside a structure of type List a = Nil | Cons a (List a) is treated monolithically (i.e., ignored) by the structural induction rule for lists: ∀(a : Set) (P : List a → Set) → P Nil → (∀ (x : a) (xs : List a) → P xs → P (Cons x xs)) → ∀ (xs : List a) → P xs By contrast, the deep induction rule for lists traverses not just the outer list structure with a predicate P, but also each data element of that list with a custom predicate Q:

∀ (a : Set) (P : List a → Set) (Q : a → Set) → P Nil → (∀(x : a) (xs : List a) → Q x → P xs → P (Cons x xs)) → ∀(xs : List a) → List ∧ Q xs → P xs

Here, List ∧ lifts its argument predicate Q on data of type a to a predicate on data of type List a asserting that Q holds for every element of its argument list. The structural induction rule for lists is, like that for any ADT, recovered by taking the custom predicate in the corresponding deep rule to be λx. True.

A particular advantage of deep induction is that it obviates the need to reflect properties as data types. For example, although the set of primes cannot be defined by an ADT, the primeness predicate Prime on the ADT of natural numbers can be lifted to a predicate List ∧ Prime characterizing lists of primes. Properties can then be proved for lists of primes using the following deep induction rule: ∀(P : List Nat → Set) → P Nil → (∀(x : Nat) (xs : List Nat) → Prime x → P xs → P (Cons x xs)) → ∀(xs : List Nat) → List ∧ Prime xs → P xs

As we'll see in Sections 3, 4 , and 5, the extra flexibility afforded by lifting predicates like Q and Prime on data internal to a structure makes it possible to derive useful induction principles for more complex types, such as truly nested ones. In each of the above examples, a predicate on the data is lifted to a predicate on the list. This is an example of lifting a predicate on a type in a non-recursive position of an ADT's definition to the entire ADT. However, the predicate to be lifted can also be on the type in a recursive position of a definition -i.e., on the ADT being defined itself -and this ADT can appear below another type constructor in the definition. This is exactly the situation for the ADT Forest a, which appears below the type constructor List in the definition Forest a = FEmpty | FNode a (List (Forest a))

The induction rule Coq generates for forests is ∀ (a : Set) (P : Forest a → Set) → P FEmpty → (∀ (x : a) (ts : List (Forest a)) → P (FNode x ts)) → ∀ (x : Forest a) → P x However, this is neither the induction rule we intuitively expect, nor is it expressive enough to prove even basic properties of forests that ought to be amenable to inductive proof. The approach of [11, 12] does give the expected rule 2 ∀ (a : Set) (P : Forest a → Set) → P FEmpty → (∀ (x : a) (ts : List (Forest a)) → (∀ (k < length ts) → P (ts!!k)) → P (FNode x ts)) → ∀ (x : Forest a) → P x But to derive it, a technique based on list positions is used to propagate the predicate to be proved over the list of forests that is the second argument to the data constructor FNode. Unfortunately, this technique does not obviously extend to other deep data types, including the type of "generalized forests" introduced in Section 4.4 below, which combines smaller generalized forests into larger ones using a type constructor f potentially different from List. Nevertheless, replacing ∀ (k < length ts) → P (ts!!k) in the expected rule with List ∧ P ts, which is equivalent, reveals that it is nothing more than the special case for Q = λx. True of the following deep induction rule for Forest a:

When types, like Forest a and List (Forest a) above, are defined by mutual recursion, their (deep) induction rules are defined by mutual recursion as well. For example, the induction rules for the ADTs data Expr = Lit Nat | Add Expr Expr | If BExpr Expr Expr data BExpr = BLit Bool | And BExpr BExpr | Not BExpr | Equal Expr Expr of integer and boolean expressions are defined by mutual recursion as ∀(P : Expr → Set) (Q : BExpr → Set) → (∀(n : Nat) → P (Lit n)) → (∀(e1 : Expr) (e2 : Expr) → P e1 → P e2 → P (Add e1 e2)) → (∀(b : BExpr) (e1 : Expr) (e2 :

As the examples of the previous section suggest, the key to deriving deep induction rules from (deep) data type declarations is to parameterize the induction rules not just over a predicate over the top-level data type being defined, but over predicates on the types of primitive data they contain as well. These additional predicates are then lifted to predicates on any internal structures containing these data, and the resulting predicates on these internal structures are lifted to predicates on any internal structures containing structures at the previous level, and so on, until the internal structures at all levels of the data type definition, including the top level, have been so processed. Satisfaction of a predicate by the data at one level of a structure is then conditioned upon satisfaction of the appropriate predicates by all of the data at the preceding level. The above deep induction rules were all obtained using this technique. For example, the deep induction rule for lists is derived by first noting that structures of type List a contain only data of type a, so that only one additional predicate parameter, which we called Q above, is needed. Then, since the only data structure internal to the type List a is List a itself, Q need only be lifted to lists containing data of type a. This is exactly what List ∧ Q does. Finally, the deep induction rule for lists is obtained by parameterizing the standard one over not just P but also Q, adding the additional hypothesis Q x to its second antecedent, and adding the additional hypothesis List ∧ Q xs to its conclusion.

The deep induction rule for forests is similarly obtained from the Coqgenerated rule by first parameterizing over an additional predicate Q on the type a of data stored in the forest, then lifting P to a predicate on lists containing data of type Forest a and Q to forests containing data of type a, and, finally, adding the additional hypotheses Q x and List ∧ P ts to its second antecedent and the additional hypothesis Forest ∧ Q x to its conclusion.

Predicate liftings such as List ∧ and Forest ∧ may either be supplied as primitives, or be generated automatically from the definitions of the types themselves, as described in Section 4. For container types, lifting a predicate amounts to traversing the container and applying the argument predicate pointwise.

Our technique for deriving deep induction rules for ADTs, as well as its generalization to nested types given in Section 3, is both made precise and rigorously justified in Section 4 using the results of [13] . This paper can thus be seen as a concrete application, in the specific category Fam, of the very general semantics developed in [13] ; indeed, our induction rules are computed as the interpretations of the syntax for nested types in Fam. A general methodology is extracted in Section 5. The rest of this paper can be read either as "just" describing how to generate deep induction rules in practice, or as also proving that our technique for doing so is provably correct and general. Our Agda code is at [14] .

Appropriately generalizing the basic technique of Section 2 derives deep induction rules, and therefore structural induction rules, for nested types, including truly nested types and other deep nested types. Nested types generalize ADTs by allowing elements at one instance of a data type to depend on data at other instances of the same type so that, in effect, the entire family of instances is constructed simultaneously. That is, rather than defining standalone families of inductive types, one for each choice of types to which type constructors like List and Tree are applied, the type constructors for nested types define inductive families of types. The structural induction rule for a nested type must therefore account for its changing type parameters by parameterizing over an appropriately polymorphic predicate, and appropriately instantiating that predicate's type argument at each application site. For example, the structural induction rule for the nested type Deep induction rules for nested types must similarly account for their type constructors' changing type parameters while also parameterizing over the additional predicate on the type of data they contain. Letting Pair ∧ Q be the lifting of a predicate Q on a to pairs of type a × a, so that Pair ∧ Q (x, y) = Q x × Q y, this gives the deep induction rule ∀ (P : ∀ (a : Set) → (a → Set) → PTree a → Set) → (∀ (a : Set) (Q : a → Set) (x : a) → Q x → P a Q (PLeaf x)) → (∀ (a : Set) (Q : a → Set) (x : PTree (a × a)) → P (a × a) (Pair ∧ Q) x → P a Q (PNode x)) → ∀ (a : Set) (Q : a → Set) (x : PTree a) → PTree ∧ Q x → P a Q x for perfect trees, and the deep induction rule

for lambda terms. As usual, the structural induction rules for these types can be recovered by setting Q = λx. True in their deep induction rules. Moreover, the basic technique described in Section 2 can be recovered from the more general one described in this section by noting that the type arguments to ADT data type constructors don't change, and that the internal predicate parameter to P can therefore be lifted to the outermost level of ADT induction rules.

We conclude this section by giving both structural and deep induction rules for the following truly nested type of bushes [8] :

Bush a = BNil | BCons a (Bush (Bush a)) (Note that this type is not even definable in Agda.) Correct and useful structural induction rules for bushes and other truly nested types have long been elusive. One recent effort to derive such rules has been recorded in [10] , but the approach taken there is more ad hoc than not, and generates induction rules for data types related to the nested types of interest rather than for the original nested types themselves. To treat bushes, for example, Fu and Selinger rewrite the type Bush a as NBush (Succ Zero) a, where NBush = NTimes Bush and

Their induction rule for bushes is then given in terms of these rewritten ones as

NBush n a) (xs : NBush (Succ (Succ n)) a) → P n x → P (Succ (Succ n)) xs → P (Succ n) (BCons x xs)) → ∀ (n : Nat) (xs : NBush n a) → P n xs This approach appears promising, but is not yet fully mature. The core difficulty is that, although Fu and Selinger "hint at how the construction ... can be generalized to arbitrary nested types" and "give an example of nested data type [sic] that is hopefully general enough to make it clear what one would do in the general case" in Section 5 of [10] , they do not show how to derive their induction rules in a uniform and principled way even for the "reasonably arbitrary and general" nested types they consider. As a result, it is unclear what guarantees that the induction rules they derive are correct, either for the original nested types or for their rewritten versions, or whether the induction rules for the rewritten nested types are sufficiently expressive to prove all results about the original nested types that one would expect to be provable by induction. This latter point echoes the issue with Coq-derived induction rules for forests mentioned above, and has the unfortunate effect of forcing users to manually write induction (and other) rules for such types for use in that system [17] .

Direct application of the general technique illustrated above and explicated in full in Section 4 below derives the following first-ever useful induction rule for bushes, respectively -a full 20 years after they were first introduced! ∀(P : ∀(a : Set) → Bush a → Set) → (∀(a : Set) → P a BNil) → (∀(a : Set) (x : a) (y : Bush (Bush a)) → P (Bush a) y → P a (BCons x y)) → ∀(a : Set) (x : Bush a) → P a x

In the next section we will see that this rule is derivable from the following more general one:

This section gives a grammar generating a robust class of nested types, including ADTs and truly nested types, and recaps the semantics given in [13] for them from which we derive their deep induction rules. This entire paper can thus be read as a practical application of the abstract results of [13] .

We write a : A if A is category and a is an object of A. We write 0 A and 1 A for the initial and terminal objects of A, and o A and ! A for the unique maps o A : 0 A → A and ! A : A → 1 A , respectively. If A is the category Set of sets and functions between them, we write 0 for 0 Set , i.e., for ∅, and 1 for any 1-element set, i.e., for 1 Set . If a : A we write K a for the constantly a-valued functor on A. The category Fam, which we will use to interpret predicates, is given by: 

If V is a countable set of type variables, V ⊆ V is finite, α ∈ V, and we write V, α for V ∪ {α}, then the following grammar generates (representations of) all standard polynomial ADTs over V , i.e., all ADTs defined over data of primitive types:

The grammar A = V A V also generates (representations of) deep ADTs, i.e., ADTs defined not just over data of the primitive types, but over data of other ADTs as well. For example, it generates the representation List α := µβ. 1+α×β of the type List a, the representation Forest α := µβ. 1 + α × µγ. 1 + β × γ of the type Forest a, and the representation µδ. 1 + (µβ. 1 + α × µγ. 1 + β × γ) × δ of the type List (Forest a). Using Bekič's Lemma, it can also generate (representations of) ADTs defined by mutual recursion such as Expr := µα. s(α, µβ. t(α, β)) and BExpr := µβ. t(Expr , β), where s(α, β) := Nat + α × α + β × α × α and t(α, β) := Bool + β × β + β + α × α for the ADTs of integer and boolean expressions from Section 1. ADTs with more than one type argument can be handled by tupling them into one or, equivalently, by noting that such ADTs are generated by the extension N of the grammar A given in Section 4.4. We adopt the usual conventions regarding free and bound type variables for A.

As usual, ADTs are interpreted relative to environments.

A set environment σ is a function from a finite subset V of V to Set. We write Env Set V for the set of set environments whose domain is V . If A ∈ Set, σ ∈ Env Set V , and α ∈ V , then σ[α := A] is the set environment with domain V, α that extends σ by mapping α to A. We write σα in place of σ(α) for the image of α under σ, and [] for the set environment with domain V = ∅.

It is well-known that the ADTs generated by the grammar A have initial algebra semantics in the category Set. That is, each such ADT µα. E can be interpreted as the carrier µF of the initial algebra for the polynomial endofunctor F on Set that interprets its body E. In particular, the final clause of the next definition is well-defined.

Like Set, the category Fam has sufficient structure to interpret ADTs generated by the grammar A. In particular, it interprets bodies of polynomial ADTs.

Definition 4. The category Fam supports the following constructions: and (α , β ) :

is defined by δ(inL a) = βa and δ(inR a ) = β a . As expected, ((α, β) + (α , β )) • inL = (α, β) and ((α, β) + (α , β )) • inR = (α , β ). , β ax) ). As expected, π 1 • ((α, β) × (α , β )) = (α, β) and

To interpret ADTs generated by A in Fam we also need to be able to interpret expressions of the form µα.E. This we do by computing the least fixed point in Fam of the functor G : Fam → Fam interpreting E. It is natural to try to do this using the same technique in Fam that gives its Set-interpretation, i.e., by iterating G ω-many times starting from the initial object 0 of Fam. This gives the least fixed point µG of G as the colimit G ω 0 in Fam of the sequence

This approach is indeed viable, and is formally justified by [13] . There, it is shown that if λ is a regular cardinal, C is a locally λ-presentable category, and G : C → C is a λ-accessible functor drawn from a particular class of functors that goes far beyond just first-order polynomial ones, then the least fixed point µG of G exists in C and can be computed as the transfinite colimit G λ 0 of the sequence

That the sequence (*) computes µG for all polynomial functors on Fam then follows by taking λ to be ω, noting that Fam is locally finitely presentable, and recalling that all such functors are ω-accessible. That (*) further computes µG for every functor G on Fam that interprets an expression generated by A now follows easily by structural induction. We record this as:

Theorem 1. If G : Fam → Fam is a functor interpreting an expression (with a distinguished variable) generated by the grammar A, then the least fixed point µG of G (with respect to that variable) is G ω 0. Concretely, the colimit G ω 0 can be computed as lim − →n∈N (A n , P n ) = (A, P ), where A = lim − →n∈N A n with mediating morphisms α n : A n → A, and P is defined by P x = lim − →n∈N,y∈α −1

To define interpretations in Fam for ADTs generated by A we need the following analogue of Definition 2:

Definition 5. A predicate environment ρ is a function from a finite subset V of V to Fam. We write Env Fam V for the set of predicate environments whose domain is V . If (A, P ) ∈ Fam, ρ ∈ Env Fam V , and α ∈ V , we write ρ[α := (A, P )] for the predicate environment with domain V, α that extends ρ by mapping α to (A, P ). We write αρ in place of ρ(α) for the image of α under ρ.

Let σ ∈ Env Set V . If ρ ∈ Env Fam V is such that π 1 (αρ) = ασ for all α ∈ V then we say that ρ is a lifting of σ. We write σ for the particular lifting ρ of σ such that αρ = (ασ, K 1 ) for all α ∈ V . In addition, if ρ ∈ Env Fam V maps each α ∈ V to (A α , P α ) then we write π 1 ρ for the set environment with domain V mapping each α ∈ V to A α . We write [] for the unique environment with domain V = ∅.

We then have the following Fam-interpretations for ADTs generated by A:

Before showing how to derive induction rules for the ADTs generated by A we prove two crucial lemmas linking their Setand Fam-interpretations.

Proof. By induction on the structure of expressions. The only non-trivial case is for µα.E ∈ A V . Let ρ ∈ Env Fam and if π 2 (βρ) = K 1 for all β ∈ V then, moreover, π 2 (G(A, K 1 )) = K 1 . We then have π 1 ( µα.E Fam ρ) = π 1 (µ((A, Q) → E Fam ρ[α := (A, Q)])) = π 1 (µG) = π 1 (lim − →n∈N G n 0) = lim − →n∈N π 1 (G n 0) = lim − →n∈N F n 0 = µF = µ(A → E Set (π 1 ρ)[α := A]) = µα.E Set (π 1 ρ). Here, the fourth equality is justified by Theorem 1, and the fifth is justified by ( †) and induction on n. If π 2 (βρ) = K 1 for all β ∈ V as well, then π 2 ( µα.E Fam ρ) = π 2 (µ((A, Q) → E Fam ρ[α := (A, Q)])) = π 2 (µG) = π 2 (lim − →n∈N G n 0) = π 2 (lim − →n∈N (F n 0, K 1 )) = λx. lim − →n∈N,y∈α −1 n x K 1 y = K 1 . Here, the morphisms α n : F n 0 → µF are the mediating morphisms for the colimit, as in Theorem 1, and the fourth equality is justified by the fact that π 2 (G(A, K 1 )) = K 1 and induction on n. 

To derive induction rules for the ADTs generated by A, we first observe that, given an ADT µα.E ∈ A V and a set environment σ ∈ Env Set V interpreting its free variables, the interpretation E Set σ defines a functor F σ A = E Set σ[α := A] such that µα.E Set σ = µ(A → E Set σ[α := A]) = µ(A → F σ A) = µF σ . We can therefore think of F σ as representing the data type constructor associated with the ADT. Thus, as argued in [11, 12] , the semantic induction rule for proving predicates over the σ-instance of the ADT µα.E has the form ∀(P : µF σ → Set). ??? → ∀(x : µF σ ). P x for some appropriate hypotheses ???. We can use the Fam-interpretation of E to discover a semantic counterpart to the hypotheses ???. Reflecting the resulting semantic rule for the σ-instance of µα.E back into the programming language syntax will then derive induction rules for polynomial ADTs.

To deduce what ??? is, we first observe that the conclusion ∀(x : µF σ ). P x of the induction rule for the σ-instance of µα.E is isomorphic to the type of the second component of a morphism in Fam from (µF σ , K 1 ) to (µF σ , P ) whose first component is id . Lemma 1 suggests that if we can see (µF σ , K 1 ) as µG for some functor G : Fam → Fam, then we can fold over a G-algebra on (µF σ , P ) in Fam to get such a morphism, i.e., to inhabit the type that is the structural induction rule for the σ-instance of µα.E. This will provide a proof ind µα.E,σ P that the property P holds for all elements of the σ-instance of µα.E.

To this end, let ρ ∈ Env Fam V be any lifting of σ, and consider again the functor F ρ (A, Q) = E Fam ρ[α := (A, Q)] on Fam given in Lemma 1 (there called G). An F ρ -algebra structure on (µF σ , P ) is a morphism (k , k) :F ρ (µF σ , P ) → (µF σ , P ) in Fam. Then π 1 (F ρ (µF σ , P )) = π 1 ( E Fam ρ[α := (µF σ , P )]) = (π 1 ( E Fam ρ))[α := µF σ ] = E Set σ[α := µF σ ] = F σ (µF σ ), with the third equality holding by Lemma 1. If we take k = in, then k : ∀(x : F σ (µF σ )). π 2 ( E Fam ρ[α := (µF σ , P )])x → P (in x), so that ind µα.E, ρ : ∀(P : µF σ → Set).

(∀(x : F σ (µF σ )). π 2 ( E Fam ρ[α := (µF σ , P )])x → P (in x)) → ∀(x : µF σ ). P x ind µα.E, ρ P k x = π 2 (fold Fam µα.E, ρ (in, k)) x () Here, fold Fam µα. E, ρ (in, k) is the uniqueF ρ -algebra morphism from in :F ρ (µF ρ ) → µF ρ to (in, k) in Fam.

Taking ρ = σ in the above development derives the expected structural induction rules for ADTs generated by A. But this development is actually far more flexible, since the induction rule it derives is parameterized over an arbitrary lifting ρ of the set environment σ, and later specialized to σ to obtain structural induction rules for ADTs. The non-specialized rule can therefore be used to prove properties of ADTs that are parameterized over non-trivial (i.e., non-K 1 ) predicates on the type parameters to the type constructors induced by those ADTs; these are precisely our deep induction rules for ADTs.

As expected, the conclusion of an ADT's deep induction rule will have an additional hypothesis involving the lifting of this predicate to that ADT. As we have seen, the ability to lift a predicate Q on a set A to a predicate T Q on T A, where T is an ADT's type constructor, is therefore central to deep induction. Every type constructor for every ADT generated by the grammar A has such a lifting. Concretely, it is computed as the second component of the interpretation in Fam of that data type. For example, the lifting List Q : List A → Set is Q) ]. This can be coded in Agda as (∀(x : F (µF )).

Simplifying π 2 's argument gives (1, K 1 ) + (A, Q) × (µF, P ). Its predicate part, obtained by applying π 2 , is K 1 + (Q × P ), so the hypotheses for ind List α,ρ are ∀(x : 1 + A × List A).(K 1 + (Q × P ))x → P (in x) = (∀(x : 1). 1 → P Nil ) × (∀(y : A). ∀(ys : List A). Q y → P ys → P (Cons y ys)) = P Nil × (∀(y : A). ∀(ys : List A). Q y → P ys → P (Cons y ys)) Reflecting back into syntax gives the deep induction rule from Section 1: ∀ (a : Set) (P : List a → Set) (Q : a → Set) → P Nil → (∀(y : a) (ys : List a) → Q y → P ys → P (Cons y ys)) → ∀(xs : List a) → List ∧ Q xs → P xs

Taking Q = K 1 gives the usual structural induction rule for lists from Section 1.

Since Forest a and List (Forest a) are mutually recursively defined, the deep induction rule for forests is defined by mutual recursion with the deep induction rule for lists. It can be computed as the type of ind F orest α, ρ for the ADT Forest α := µβ. α × µγ. 1 + β × γ using the same technique as in Example 1. This gives the (deep) induction rule for forests from Section 1.

Example 3. Exactly the same technique delivers the deep induction rules from Section 1 for the mutually recursive ADTs Expr and BExpr whose representations are given before Definition 2.

We can use the technique from Section 4.3 to derive induction rules for nested types as well, including truly nested types and other deep nested types. To do so we first need an extension of the grammar A that generates these types. Since nested types generalize ADTs to allow elements of a nested type at one instance of a type to depend on data at other instances of that nested type, they are interpreted as least fixed points not of ordinary (first-order) functors on Fam, as ADTs are, but rather as least fixed points of higher-order such functors. Moreover, since nested types can be parameterized over any number of type arguments, the (first-order) functors interpreting them can have correspondingly arbitrary arities. For each k ≥ 0 we therefore assume a countable set F k of functor variables of arity k, disjoint for distinct k. We use lower case Greek letters for functor variables, write ϕ k to indicate that ϕ ∈ F k , and say that ϕ has arity k in this case. Type variables are exactly functor variables of arity 0; we continue to write α, β, etc., rather than α 0 , β 0 , etc., for them. We write F = k≥0 F k . If V ⊆ F is finite and ϕ ∈ F k for some k, write V, ϕ for V ∪ {ϕ}.

Definition 7. For a finite set V of F , the set of (truly) nested data types over V is generated by the following grammar:

Here, ϕ k ∈ V and the lengths of the vectors of terms in N V in the third and final clauses of the above grammar are both k.

The grammar N = V N V generalizes A by allowing recursion not just at the level of type variables, but also at the level of functor variables. This reflects the fact that, in programming language syntax, nested types can be parameterized over both types and type constructors. For example, N V generates the representation PTree α := µϕ 1 .λβ.β + ϕ(β × β) α ∈ N α of the type PTree a, the representation Lam α := µϕ 1 .λβ.β + ϕβ × ϕβ + ϕ(β+1) α ∈ N α of the type Lam a and the representation Bush α := µϕ 1 .λβ. 1 + β × ϕ (ϕ β) α ∈ N α of the type Bush a. But it also generates the representation GForest ϕ α := µβ. 1 + α × ϕ β ∈ N ϕ,α of the following nested type of generalized forests with data of type a:

This type is higher-order in the sense that the type constructor GForest takes not just a type, but also a (unary) type constructor, as an argument. It therefore cannot be expressed as an element of A, and thus demonstrates the benefit of working with the more expressive grammar N . On the other hand, it is decidedly ADT-like, in the sense that it defines a family of inductive types rather than an inductive family of types. In fact, if f were a type constructor induced by a nested type generated by our grammar, then GForest f a and f (GForest f a) would be mutually recursively defined. In this case, generalizing Example 2, their structural induction rules would also be defined by mutual recursion.

It is not hard to see that A ⊆ N . Moreover, the grammar N allows nested types to be parameterized over (other) nested data types, just as A allows ADTs to be parameterized over (other) ADTs. For instance, we could have perfect trees of lists or binary trees, bushes of perfect trees, etc.

We have the following notions of functor and application in Fam: Fam is a pair (F, P ) , where F : Set k → Set and P : ∀(X 1 , P 1 )....(X k , P k ). F X 1 ...X k → Set is a Famindexed predicate. The application of a functor (F, P ) : Fam k → Fam to an object (A 1 , Q 1 ), ...., (A k , Q k ) of Fam k is given by

We call a lifted functor G = (F, P ) a lifting of F from Set to Fam, and call P a Fam-indexed predicate. A Set-indexed predicate is a Fam-indexed predicate that does not depend on its arguments' second components. We extend the notions of set environment and predicate environment from Definitions 2 and 5 as follows:

Definition 9. A set environment σ is a mapping from a finite subset V = {ϕ k1 1 , ..., ϕ kn n } of F such that ϕ i σ : Set ki → Set for i = 1, ..., n. We write Env Set V for the set of set environments whose domain is V . If F ∈ Set k → Set, σ ∈ Env Set V , and ϕ k ∈ V , we write σ[ϕ := F ] for the set environment with domain V, ϕ that extends σ by mapping ϕ to F . Similarly, a predicate environment ρ is a mapping from a finite subset V = {ϕ k1 1 , ..., ϕ kn n } of F such that ϕ i ρ : Fam ki → Fam is a lifted functor for i = 1, ..., n. We write Env Fam V for the set of predicate environments whose domain is V . If (F, P ) ∈ Fam k → Fam, ρ ∈ Env Fam V , and ϕ k ∈ V , we write ρ[ϕ := (F, P )] for the predicate environment with domain V, ϕ that extends ρ by mapping ϕ to (F, P ).

The notions of a predicate environment being a lifting of a set environment and the notations σ, π 1 ρ, and [] are now extended in the obvious ways.

The following interpretations of nested types generated by N in the locally finitely presentable categories Set and Fam are shown in [13] to be well-defined:

Straightforward generalization of the analysis in Section 4.3 to N gives induction rules for the type constructors nested types induce. Given a nested type (µϕ k .λα 1 ...α k . E)E 1 ...E k ∈ N V with type constructor T = µϕ k .λα 1 ...α k . E and a set environment σ ∈ Env Set V interpreting its free variables, we have that

where the higher-order functor H σ on Set is defined by

For any lifting ρ of σ, the predicate counterpart to H σ is the higher-order functor H ρ on Fam whose action on a k-ary lifted functor (F, P ) is the k-ary lifted functor H ρ (F, P ) given bŷ The induction rule ind T, ρ for proving predicates over the σ-instance of the type constructor T relative to the lifting ρ is thus given by

To get analogues for nested types of the structural induction rules for ADTs note that, since each σ-instance of the type constructor T = µϕ k .λα 1 ...α k . E associated with a nested type (µϕ k .λα 1 ...α k .E)E 1 ...E k ∈ N V gives rise to an inductive family of types, the appropriate notion of predicate for a nested type is actually a Set-indexed predicate. By direct analogy with structural induction for ADTs, the structural induction rule for a nested type with type constructor T whose σ-instance is interpreted by µH σ is then

To see that the structural induction rule ( ‡) is indeed a specialization of ind T, ρ , suppose we are given a predicate P : ∀(A i , Q i ). (µH σ )A i → Set for a nested type with type constructor T whose σ-instance is interpreted by µH σ , together with induction hypotheses

We can distill from the foundations given in Section 4 a general methodology that will derive correct deep induction rules for any nested type generated by N . Concretely, this methodology comprises the following steps:

1. Given a nested data type definition D, translate its type constructor into an expression N in the grammar N (or, more simply, A, if D defines an ADT). 2. Interpret N in Set to get a fixpoint equation defining D as µH for some (higher-order) operator H. 3. Reinterpret N in Fam to define a corresponding (higher-order) operatorĤ on predicates whose fixed point µĤ is an inductive predicate on µH, i.e., on D. 4. Initiality of µĤ guarantees that there is a unique predicate morphism from µĤ to any other predicate P admitting anĤ-algebra structure. This gives D's deep induction rule.

These are precisely the steps carried out in all of our examples, including those below, which illustrate the derivation for nested types given in Section 4.5. Reflecting µĤ back into syntax gives the inductive predicate

Now, if P is any other predicate on Lam admitting anĤ-algebra structure, then there must exist a morphism k :

Since Lam ∧ reflects the initialĤ-algebra, there is a unique algebra morphism from in :Ĥ(µĤ) → µĤ to theĤ-algebra k on P , i.e., from µĤ to P . Reflecting this morphism back into syntax gives the deep induction rule for lambda terms from Section 3.

The deep induction rule for lambda terms can be used to prove, e.g., properties of lambda terms whose variables are represented by prime numbers or lambda terms over strings that can represent variable names. It can also be used to prove properties of lambda terms over lambda terms, such as the associativity laws needed to show that the functor Lam is a monad; such a proof is included as the first case study in the accompanying Agda code. The second uses deep induction rule we derive in Example 5 to prove some results about bushes.

Since truly nested types are a special case of deep nested types, our methodology can derive useful induction rules for them -including the perpetually problematic truly nested type of bushes [8, 10, 15] introduced in Section 3.

Example 5. Since the truly nested type Bush α := µϕ 1 .λβ. 1 + β × ϕ (ϕ β) α ∈ N α is uniform in its index α, it induces a type constructor Bush := µϕ 1 .λβ. 1 + β × ϕ (ϕ β). Writing H for H [] andĤ forĤ [] , and letting

we have that µH = Bush and the predicate counterpartĤ to H is given bŷ Reflecting µĤ back into syntax gives the inductive predicate

Now, if P is any other predicate on Bush admitting anĤ-algebra structure, then there must exist a morphism k : ∀(x : 1 + Bush (Bush A)).

(K 1 + Q × π 2 ((Bush,P )((Bush,P )(A, Q))))x → P A Q (in x) = ∀(x : 1 + Bush (Bush A)). (K 1 + Q × P (Bush A) (P A Q))x → P A Q (in x)

i.e., (k 1 , k 2 ), where k 1 : ∀(x : 1). 1 → P A Q BNil and k 2 : ∀(x : A). ∀(y : Bush (Bush A)). 1 → P (Bush A) (P A Q) y → P A Q(BCons x y). Since Bush ∧ reflects the initialĤ-algebra, there is a unique predicate morphism from µĤ to P . Reflecting this morphism back into syntax gives the deep induction rule for bushes from Section 3.

The function BDind ⇒ MBDind in our Agda code shows that our methodology also derives a mutually recursive deep induction rule for bushes, there called MBDind.

Examples 4 and 5 show that when the definition of a nested type contains an instance of another nested type constructor C -e.g., Maybe a in the argument Lam (Maybe a) to Abs -its inductive predicate definition, and thus its deep induction rule, will involve a call to the predicate interpretation C ∧ of C. When the definition contains an instance of the constructor for the same type being defined -e.g., Bush a in the type argument Bush (Bush a) to BCons -its inductive predicate definition, and thus its deep induction rule, will involve a recursive call to the inductive predicate being defined. The treatment of a truly nested type is thus exactly the same as the treatment of any other nested type.

Independently of deriving induction rules, even defining some nested types in Agda requires turning off its termination checks in a few tightly compartmentalized places. For example, neither Coq nor Agda currently allows the definition of the bush data type because of the non-positive occurrence of Bush in the type of BCons. The correctness of our development in those places is justified by [13] . This work suggests that the current notion of positivity should be generalized.

As far as we know, the phenomenon of deep induction has not previously even been identified, let alone studied. This paper treats deep induction for nested types, which extend ADTs by allowing higher-order recursion. Other generalizations of ADTs are also well-studied in the literature, including (indexed) containers [1, 2] , which extend ADTs by allowing type dependency. In particular, [3] defines a class of "nested" containers corresponding to inductive types whose constructors can recursively depend on the data type at different instances than the one being defined. The case of truly nested types is not treated there, however. We hope eventually to extend the results of this paper to derive provably correct deep induction rules for (indexed) containers, GADTs, dependent types, and other classes of more advanced data types. One interesting question is whether or not a common generalization of indexed containers and the class of nested types studied here has a rigorous initial algebra semantics as in [13] .

A more recent line of investigation concerns sized types [5] . These are particularly well-suited to termination checking of (co)recursive definitions, and are implemented in the latest versions of Agda [6] . Although originally defined in the context of a type theory with higher-order functions [4] , the current incarnation of sized types does not appear to admit definitions with true nesting. What seems to be missing is an addition operation on sizes, which would allow a constructor such as BCons to combine a structure with size of depth "up to α" with one of depth "up to β" to define a data element of depth "up to α + β".

Tassi [17] has independently implemented a tool for deriving induction principles of data type definitions in Coq using unary parametricity. Although neither rigorous derivation nor justification is provided, his technique seems to be essentially equivalent to ours, and could perhaps be justified by our general framework. True nesting still is not permitted, however. In [7] , mutually recursively defined induction and coinduction rules are derived for mutually recursive and corecursive data types. But these are still the standard structural (co)induction rules, rather than deep ones. This suggests a need for deep coinduction rules, too.

Containers: Constructing strictly positive types

Indexed containers

Representing nested inductive types using W-types

Type-based termination: A polymorphic lambda-calculus with sized higher-order types

Semi-continuous sized types and termination

MiniAgda: Integrating sized and dependent types

Truly Modular (Co)datatypes for Isabelle/HOL

Mathematics of Program Construction

De Bruijn notation as a nested datatype

Dependently typed folds for nested data types

Fibrational induction rules for initial algebras

Generic fibrational induction

Higher-kinded data types: Syntax and semantics

Accompanying Agda code for this paper

An induction principle for nested datatypes in intensional type theory

Purely Functional Data Structures

Deriving proved equality tests in Coq-elpi: Stronger induction principles for containers in Coq

), which permits use, sharing, adaptation, distribution and reproduction in any medium or format, as long as you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons license and indicate if changes were made. The images or other third party material in this chapter are included in the chapter's Creative Commons license, unless indicated otherwise in a credit line to the material. If material is not included in the chapter's Creative Commons license and your intended use is not permitted by statutory regulation or exceeds the permitted use