Jasmin Christian Blanchette

Fabian Meier

Andrei Popescu

Dmitriy Traytel

Foundational Nonuniform (Co)datatypes for Higher-Order Logic

Nonuniform (or "nested" or "heterogeneous") datatypes are recursively defined types in which the type arguments vary recursively. They arise in the implementation of finger trees and other efficient functional data structures. We show how to reduce a large class of nonuniform datatypes and codatatypes to uniform types in higher-order logic. We programmed this reduction in the Isabelle/HOL proof assistant, thereby enriching its specification language. Moreover, we derive (co)induction and (co)recursion principles based on a weak variant of parametricity.

I. INTRODUCTION

Inductive (or algebraic) datatypes-often simply called datatypes-are a central feature of typed functional programming languages and of most proof assistants. A simple example is the type of finite lists over a type parameter α, specified as follows (in a notation inspired by Standard ML):

α list = Nil | Cons α (α list)
A datatype is uniform if the recursive occurrences of the datatype have the same arguments as the definition itself, as is the case for list; otherwise, the datatype is nonuniform. Nonuniform types are also called "nested" or "heterogeneous" in the literature. Powerlists are nonuniform:

α plist = Nil | Cons α ((α × α) plist)
The type α plist is freely generated by the constructors Nil : α plist and Cons : α → (α × α) plist → α plist. When Cons is applied several times, the product type constructors (×) accumulate to create pairs, pairs of pairs, and so on. Thus, any powerlist of length 3 will have the form Nonuniform datatypes arise in the implementation of efficient functional data structures, such as finger trees [START_REF] Hinze | Finger trees: a simple general-purpose data structure[END_REF], and they underlie Okasaki's bootstrapping and implicit recursive slowdown optimization techniques [START_REF] Okasaki | Purely functional data structures[END_REF]. Yet many programming languages and proof assistants lack proper support for such types. For example, even though Standard ML allows nonuniform definitions, a typing restriction disables interesting recursive definitions. As for proof assistants, Agda, Coq, Lean, and Matita allow nonuniform definitions, but they are built into the logic (dependent type theory), with all the risks and limitations that this entails [13, Section 1].

For systems based on higher-order logic such as HOL4, HOL Light, and Isabelle/HOL, no dedicated support exists for nonuniform types, probably because they are widely believed to lie beyond the logic's ML-style polymorphism. Building on the well-understood metatheory of uniform datatypes (Section II), we disprove this folklore belief by showing how to define a large class of nonuniform datatypes by reduction to their uniform counterparts within higher-order logic (Section III).

Our constructions allow variations along several axes. They cater for mutual definitions:

α ptree = Node α (α pforest) α pforest = Nil | Cons (α ptree) ((α × α) pforest)
They allow multiple recursive occurrences, with different type arguments:

α plist = Nil | Cons 1 α (α plist ) | Cons 2 α ((α × α) plist )
They allow multiple type arguments, which may all vary:

(α, β) tplist = Nil β | Cons α ((α × α, unit + β) tplist) Moreover, they allow the presence of datatypes, codatatypes, and other well-behaved type constructors both around the type arguments and around the recursive type occurrences:

α stree = Node α (((α fset) stree) fset)
Here, fset is the type constructor associated with finite sets.

Furthermore, the constructions can be extended to coinductive (or coalgebraic) datatypes-codatatypes. Codatatypes are generally non-well-founded, allowing infinite values. They are often used to model the datatypes of languages with a nonstrict evaluation strategy, such as Haskell, and they can be very convenient for some proof tasks. The codatatype definition α pstream

)).

Unlike dependent type theory, higher-order logic requires all types to be nonempty (inhabited). To introduce a new type, we must both provide a construction in terms of existing types and prove its nonemptiness. For example, a datatype specification analogous to the pstream codatatype above should be rejected. In previous work [START_REF] Blanchette | Witnessing (co)datatypes[END_REF], we showed how to decide the nonemptiness problem for uniform types-including mutually recursive specifications and arbitrary mixtures of datatypes 978-1-5090-3018-7/17/$31.00 c 2017 IEEE and codatatypes-by viewing the definitions as a grammar, with the defined types as nonterminals. Here, we extend this result to nonuniform types (Section IV). This is achieved by encoding the nonuniformities in a generalized grammar, which can decide nonemptiness of the sets that arise in the construction of the nonuniform types.

Once a datatype has been introduced, users want to define functions that recurse on it and carry out proofs by induction involving these functions-and similarly for codatatypes. A uniform datatype definition generates an induction theorem and a recursor. Nonuniform datatypes pose a challenge, because neither the induction theorem nor the recursor can be expressed in higher-order logic, due to its limited polymorphism. For example, induction for plist should look like this:

∀Q. Q Nil ∧ ∀x xs. Q xs = ⇒ Q (Cons x xs) = ⇒ ∀ys. Q ys
However, this formula is not typable in higher-order logic, because the second and third occurrences of the variable Q need different types: (α × α) plist → bool versus α plist → bool. Our solution is to replace the theorem by a procedure parameterized by a polymorphic property ϕ α : α plist → bool (Section V). For plist, the procedure transforms a proof goal of the form ϕ α ys into two subgoals ϕ α Nil and ∀x xs. ϕ α×α xs = ⇒ ϕ α (Cons x xs). A weak form of parametricity is needed to recursively transfer properties about ϕ α to properties about ϕ α×α . Our approach to (co)recursion is similar (Section VI).

All the constructions and derivations are formalized in the Isabelle/HOL proof assistant and form the basis of highlevel commands that let users define nonuniform types and (co)recursive functions on them and reason (co)inductively about them (Section VII). The commands are foundational: Unlike all previous implementations of nonuniform types in proof assistants, they require no new axioms or extensions of the logic. An example involving λ-terms in De Bruijn notation demonstrates the practical potential of our approach.

Our main contributions are the following: First, we designed a reduction of nonuniform datatypes to uniform datatypes within the relatively weak higher-order logic, including recursion and induction. Second, we adapted the constructions to support codatatypes as well, exploiting dualities. Third, we coded the reduction in a proof assistant based on higher-order logic, yielding a first implementation of nonuniform datatypes without dependent types. The formal proofs, the source code, and the examples are publicly available [START_REF] Blanchette | Formalization and implementation accompanying this paper[END_REF].

II. PRELIMINARIES A. Higher-Order Logic

We consider classical higher-order logic (HOL) with Hilbert choice, the axiom of infinity, and rank-1 polymorphism. HOL is based on Church's simple type theory [START_REF] Church | A formulation of the simple theory of types[END_REF]. It is the logic of Gordon's original HOL system [START_REF]Introduction to HOL: A Theorem Proving Environment for Higher Order Logic[END_REF] and of its many successors and emulators, notably HOL4, HOL Light, and Isabelle/HOL.

Primitive types are built from type variables α, β, . . . , a type bool of Booleans, and an infinite type ind using the function type constructor; thus, (bool → α) → ind is a type. Primitive constants are equality = : α → α → bool, the Hilbert choice operator, and 0 and Suc for ind. Terms are built from constants and variables by means of typed λ-abstraction and application.

A polymorphic type is a type T that contains type variables. If T is polymorphic with variables α = (α 1 , . . . , α n ), we write α T instead of T. Formulas are closed terms of type bool. The logical connectives and quantifiers on formulas are defined using the primitive constants-e.g., True as (λx : bool. x) = (λx : bool. x). Polymorphic formulas are thought of as universally quantified over their type variables. For example, ∀x : α. x = x really means ∀α. ∀x : α. x = x. Nested type quantifications such as (∀α. . . .) = ⇒ (∀α. . . .) are not expressible. We will express concepts in standard mathematical language whenever the expressiveness of HOL is not a concern.

The only primitive mechanism for defining new types in HOL is type definition: For any existing type α T and predicate P : α T → bool such that {x : α T | P x} is nonempty, we can introduce a type α S isomorphic to {x : α T | P x}. Upon meeting the definition α S = {x : α T | P x}, the system requires the user to prove ∃x : α T. P x and then introduces the type α S, the projection Rep S : α S → α T, and the embedding Abs S : α T → α S such that ∀x. P (Rep S x), ∀x. Abs S (Rep S x) = x, and ∀x. P x = ⇒ Rep S (Abs S x) = x. The nonemptiness check is necessary because all types in HOL must be nonempty. This is a well-known design decision connected to the presence of Hilbert choice in HOL [START_REF]Introduction to HOL: A Theorem Proving Environment for Higher Order Logic[END_REF], [START_REF] Paulson | A formulation of the simple theory of types (for Isabelle)[END_REF].

Thus, unlike dependent type theory, HOL does not have (co)datatypes as primitives. However, datatypes [START_REF] Berghofer | Inductive datatypes in HOL-Lessons learned in formal-logic engineering[END_REF], [START_REF] Gunter | A broader class of trees for recursive type definitions for HOL[END_REF], [START_REF] Harrison | Inductive definitions: Automation and application[END_REF], [START_REF] Melham | Automating recursive type definitions in higher order logic[END_REF], [START_REF] Traytel | Foundational, compositional (co)datatypes for higher-order logic: Category theory applied to theorem proving[END_REF] and, more recently, codatatypes [START_REF] Traytel | Foundational, compositional (co)datatypes for higher-order logic: Category theory applied to theorem proving[END_REF] are supported via derived specification mechanisms. Users can write fixpoint definitions an ML-style syntax, and the system defines the type using nonrecursive type definitions (ultimately appealing to ind and →); defines the constructors and related operators; and proves characteristic properties, such as injectivity of constructors, induction theorems, and recursor theorems.

B. Bounded Natural Functors

We take uniform (co)datatypes for granted, thus assuming the availability of types such as α list. Often it is useful to think in terms of type constructors. For example, list is a type constructor in one variable, sum (+) and product types (×) are binary type constructors. Most type constructors are not only operators on types but have a richer structure, that of bounded natural functors (BNFs) [START_REF] Traytel | Foundational, compositional (co)datatypes for higher-order logic: Category theory applied to theorem proving[END_REF].

We write [n] for {1, . . . , n} and α set for the powertype of α, consisting of sets of α elements; it is isomorphic to α → bool. An n-ary BNF is a tuple

F = (F, map F , (set i F ) i∈[n] , bd F ), where • F is an n-ary type constructor; • map F : (α 1 → β 1 ) → • • • → (α n → β n ) → α F → β F; • set i F : α F → α i set for i ∈ [n];
• bd F is an infinite cardinal number satisfying the following properties:

• (F, map F ) is an n-ary weak-pullback-preserving functor;

• each set i F is a natural transformation between the functor (F, map F ) and the powerset functor (set, image);

• ∀i ∈ [n]. ∀a ∈ set i F x. f i a = g i a = ⇒ map F f x = map F g x; • ∀i ∈ [n]. ∀x : α F. set i F x ≤ bd F .
We regard the elements of α F as containers filled with "content" from α i -the set i F functions return the α i -content (known to be bounded by bd F ) and map F f replaces content via f . For example, list is a unary BNF, where map list is the standard map function, set list collects all the lists's elements, and bd list is ℵ 0 .

BNFs are closed under uniform (least and greatest) fixpoint definitions [START_REF] Traytel | Foundational, compositional (co)datatypes for higher-order logic: Category theory applied to theorem proving[END_REF] and the nonemptiness problem for BNFs constructed by basic functors, fixpoints and composition is decidable [START_REF] Blanchette | Witnessing (co)datatypes[END_REF]. These crucial properties enable a modular approach to mixing and nesting uniform (co)datatypes and deciding if a high-level specification yields valid, i.e., nonempty, HOL types. In addition, BNFs display predicator and relator structure [START_REF] Rutten | Relators and metric bisimulations[END_REF]. The predicator pred F :

(α 1 → bool) → • • • → (α n → bool) → α F → bool and the relator rel F : (α 1 → β 1 → bool) → • • • → (α n → β n → bool) → α F → β F → bool,
are defined from set F and map F as follows:

• pred F P x ⇐ ⇒ ∀i ∈ [n]. ∀a ∈ set i F x. P i a; • rel F R x y ⇐ ⇒ ∃z. (∀i ∈ [n]. set i F z ⊆ {(a, b) | R i a b}) ∧ map F fst z = x ∧ map F snd z = y,
where fst and snd are standard projection functions on the product type ×. For list, pred list P xs states that P holds for all elements of the list xs, and rel list R xs ys states that xs and ys have the same length and are element-wise related by R.

Relators and predicators are useful to track parametricity [START_REF] Reynolds | Types, abstraction and parametric polymorphism[END_REF], [START_REF] Wadler | Theorems for free![END_REF]. A polymorphic constant c : α F is parametric if, for all relations R i :

α i → β i → bool for each i ∈ [n],
we have rel F R c c-i.e., every two instances of c are related by the lifting of the relations associated with the component types. Parametricity applies not only to BNFs but also to any combination of BNFs using the function space. For polymorphic functions f : α F → α G between two BNFs, f is parametric if and only if f is a natural transformation [12, Appendix A].

III. (CO)DATATYPE DEFINITIONS

Before describing the reduction of nonuniform (co)datatypes to uniform (co)datatypes in full generality, we start with a simple example that conveys the main idea. The reduction proceeds by defining a larger uniform datatype and carving out a subset that is isomorphic to the desired nonuniform type. To prove that the constructed type is the intended one, we establish the isomorphism between the defined nonuniform type and the right-hand side of its specification.

A. Introductory Example

Okasaki [START_REF] Okasaki | Purely functional data structures[END_REF]Section 10.1.1] sketches how to mimic nonuniform datatypes using uniform datatypes. He approximates powerlists by the following definitions:

datatype α sh = Leaf α | Node (α sh × α sh) datatype α raw = Nil 0 | Cons 0 (α sh) (α raw) The type α raw corresponds to lists of binary trees α sh. It is larger than powerlists in two ways: (1) α sh allows nonfull binary trees, which cannot arise in a powerlist; (2) α raw imposes no restriction on the depth of the binary trees, whereas a powerlist has elements successively of depth 0, 1, 2, . . . . Okasaki considers these mismatches as one of two disadvantages of the above encoding. The other disadvantage is that We overcome the first disadvantage by using a type definition. From the raw type, we select exactly those inhabitants that correspond to powerlists. To achieve this, we define two predicates, ok : nat → α sh → bool and ok : nat → α raw → bool, as the least predicates satisfying the following rules:

ok 0 (Leaf x) ok n l ∧ ok n r = ⇒ ok (n + 1) (Node (l, r)) ok n Nil 0 ok n x ∧ ok (n + 1) xs = ⇒ ok n (Cons 0 x xs)
The predicate ok n t checks whether t is a full binary tree of depth n, and ok n xs checks that the first element of a list is a full tree of depth n, the second is of depth n+1, and so on. The desired type starts at depth 0:

α plist = {xs : α raw | ok 0 xs}.
The second disadvantage is addressed by hiding the internal construction of α plist. We define the powerlist constructors Nil : α plist and Cons : α → (α × α) plist → α plist in terms of Nil 0 and Cons 0 . These definitions will require some additional machinery on the raw type.

B. Datatypes

We assume that the desired nonuniform datatype has a single constructor. Separate constructors are easy to introduce as syntactic sugar [START_REF] Blanchette | Truly modular (co)datatypes for Isabelle/HOL[END_REF]Section 4]. For powerlists, the single constructor definition is α plist = Ctor plist (unit + α × (α × α) plist). It corresponds to finding a least solution (up to isomorphism) to the type fixpoint equation α plist (α, (α F) plist) G with α F = α × α and (α, β) G = unit + α × β.

We generalize this setting in multiple dimensions. First, we support a simultaneous definition of an arbitrary number i of mutual nonuniform datatypes. For example, ptree and pforest from Section I are given by the system of fixpoint equations

α ptree (α, (α F 1 ) ptree, (α F 2 ) pforest) G 1 α pforest (α, (α F 3 ) ptree, (α F 4 ) pforest) G 2 where (α, β, γ) G 1 = α × γ, (α, β, γ) G 2 = unit + β × γ, α F 1 = α F 2 = α F 3 = α, and α F 4 = α × α.
We assume that all G's depend on the same type variables, even though the dependence may be spurious, as in the case of G 1 and β.

Second, a type may occur several times on the right-hand side of a definition. We support an arbitrary number j of such occurrences. This feature is used in the plist type:

α plist (α, (α F 1 ) plist , (α F 2 ) plist ) G, where (α, β, γ) G = unit + α × β + α × γ, α F 1 = α, and α F 2 = α × α.
Finally, the construction supports an arbitrary number k of type parameters. The parameter changes may differ for different type parameters, such as in the tplist example:

(α, β) tplist (α, β, ((α, β) F 1 , (α, β) F 2 ) tplist) G, where (α, β, γ) G = β + α × γ, (α, β) F 1 = α × α, and (α, β) F 2 = unit + β.
As before for the G's, all F's may depend on all type parameters of the specified nonuniform type.

In the sequel, the indices i, j, and k range over [i], [j], and [k], respectively. Moreover, we abbreviate indexed sequences using a horizontal bar; for example, α stands for α 1 , . . . , α k , A definition of i mutual nonuniform datatypes T i is a system of i type fixpoint equations

(α, (α F 1 ) T σ(1) , . . . , (α F j ) T σ(j) ) G i Ctor i map G i id Rep σ(1) ... Rep σ(j) / / (α, (α F 1 ) [] raw σ(1) , . . . , (α F j ) [] raw σ(j) ) G i map G i Leaf 1 ... Leaf k ↑ 1σ(1) ... ↑ jσ(j) map G i id Abs σ(1) ... Abs σ(j) o o α T i dtor i O O Rep i / / α raw [] i Abs i o o unRaw i / / (α sh [] , α raw [1] σ(1) , . . . , α raw [j] σ(j) ) G i Raw i o o map G i unLeaf 1 ... unLeaf k (↓ 1σ(1) []) ... (↓ jσ(j) []) O O
α T i α, (α F 1 ) T σ(1) , . . . , (α F j ) T σ(j) G i (1)
where the G i 's are (k + j)-ary BNFs, the F jk 's are k-ary BNFs, and σ : [j] → [i] is a monotone surjective function that expresses which of the i mutual types belongs to which recursive occurrence. The construction generalizes Okasaki's idea and yields k-ary BNFs T i that are least solutions (up to isomorphism) to equation [START_REF] Abbott | Representing nested inductive types using W-types[END_REF]. A uniform datatype definition [START_REF] Blanchette | Truly modular (co)datatypes for Isabelle/HOL[END_REF] is a special case with j = i, σ(i) = i, and α F jk = α k . We start by defining the shape types α sh k that overapproximate the recursive changes to the type arguments. There are k shape types, corresponding to the k type arguments, and they are mutually recursive uniform datatypes:

α sh k = Leaf k α k | Node 1k (α sh F 1k ) | • • • | Node jk (α sh F jk )
For plist, the sh type is sh. In general, each recursive occurrence may change the type arguments in a different way; this is reflected in the different Node constructors.

Next, we define i uniform mutually recursive datatypes raw i that recurse through the G i 's in the same way as the T i 's do, except that they keep the type arguments unchanged. The immediate α arguments to G i are replaced by α sh:

α raw i = Raw i ((α sh, α raw σ(1) , . . . , α raw σ(j) ) G i )
For every i, we specify subsets of the types α raw i that are isomorphic to the nonuniform types T i , by defining predicates ok i that characterize the allowed shapes and their changes in the recursion. As in the powerlist example, the definition of ok i relies on auxiliary predicates ok k : [j] list → α sh k → bool on the shape types. The type of ok k shows an important difference to the plist example: The first argument is not just a natural number denoting the depth of a full tree but has more structure. We call it the shadow of the shape and let ∆ stand for [j] list. The additional structure is necessary because different Node jk constructors may occur in a single shape element. These occurrences in the full shape trees are layered: All Node constructors right above the Leaf constructors belong to a fixed occurrence j. The next layer of Nodes may belong to a different fixed occurrence j . The shadow summarizes the occurrence indices. Consider Cons 1 (u : α) (Cons 2 (v : α) (Cons 2 (w : α×α) (Cons 1 (x : (α×α)×(α×α)) Nil))) : α plist . This order of constructors forces x's type to be α

F = α F 1 F 2 F 2 , with α F 1 = α and α F 2 = α × α. Consequently, x is embedded into α sh as Node 2 (map F 2 Node 2 (map F 2 (map F 2 Node 1 ) (map F Leaf x))), whose shadow is [2, 2, 1].
Formally, the predicates ok k are defined together as the least predicates satisfying the rules

ok k [] (Leaf k x) pred F jk (ok 1 u) . . . (ok k u) f = ⇒ ok k ( j u) (Node jk f )
where [] and are notations for Nil and Cons. To access the recursive components of sh, we rely on the predicators associated with the F's. Predicators are monotone. The i mutual predicates ok i : ∆ → α raw i → bool are defined similarly:

pred G i (ok 1 u) . . . (ok k u) (ok σ(1) (1 u)) . . . (ok σ(j) (j u)) g = ⇒ ok i u (Raw i g)
We access the k immediate components of the shape type and the j recursive components of the raw type through the predicator. We write that an element r of type α raw i has shadow u if ok i u r holds.

Finally, the nonuniform type T i can be defined as the subset of raw i that satisfies the ok i predicate for the empty shadow: α T i = {r : α raw i | ok i [] r}. Such a type definition introduces a new type and the embedding-projection pairs Rep i : α T i → α raw i and Abs i : α raw i → α T i . The emerging nonemptiness problem is discussed in Section IV.

We can prove by induction that ok i is invariant under the map raw i function.

Lemma 1:

ok i u (map raw i f r) ⇐ ⇒ ok i u r.
This property is sufficient to prove that T i is a BNF. By virtue of being a BNF, T i can appear around type arguments and recursive type occurrences in future uniform or nonuniform (co)datatype definitions.

C. Constructors

If the type T i is the nonuniform type that we intended to construct, it should satisfy equation [START_REF] Abbott | Representing nested inductive types using W-types[END_REF]. We prove this isomorphism by defining a constructor Ctor i : (α, (α F 1 ) T σ(1) , . . . , (α F j ) T σ(j) ) G i → α T i and a destructor dtor i : α T i → (α, (α F 1 ) T σ(1) , . . . , (α F j ) T σ(j) ) G i and by showing that they are inverses of each other.

Figure 1 gives diagrammatic definitions of Ctor i (by composing the functions on the outer arrows) and dtor i (by composing the functions on the inner arrows). All shape and raw types occurring in the diagram are annotated with their shadows. Abs i can be applied only to raw elements with shadow [].

The unLeaf k and unRaw i functions are inverses of the corresponding constructors; they satisfy unLeaf k (Leaf k a) = a and unRaw i (Raw i r) = r. Note that unLeaf k is underspecified and (like Abs i ) may be applied only to Leaf k shape elements with shadow []. Moreover, the definition must bridge the gap between the types α F j raw σ( j) of shadow [] and α raw σ( j) of shadow [ j] (the rightmost arrows in Figure 1). This must happen recursively (even though the constructor Ctor i itself is not recursive), by inlining the additional Fs into a new layer of the shape type (directly above the Leaf constructors) and therefore requires a generalization that transforms an arbitrary shadow u into u j (i.e., the list u with the element j appended to it). For each fixed j, inlining is implemented by means of i mutual primitively recursive functions ↑ ji : (α F j ) raw i → α raw i , whose definition uses k mutual primitively recursive functions ↑ jk : (α F j ) sh k → α sh k on the shape type:

↑ jk (Leaf k f ) = Node jk (map F jk Leaf f ) ↑ jk (Node j k f ) = Node j k (map F j k ↑ j f ) ↑ ji u (Raw i g) = Raw i (map G i ↑ j ↑ jσ(1) . . . ↑ jσ(j) g)
Inlining is injective. We define the (partial) inverse operations ↓ ji : ∆ → α raw i → (α F j ) raw i and ↓ jk : ∆ → α sh k → (α F j ) sh k , which are useful when defining the destructors dtor i . The additional shadow parameter in ↓ ji denotes how many more layers to destruct until we arrive at the last layer of Nodes (with only Leaf constructors below).

↓ jk [] (Node jk f ) = Leaf k (map F jk unLeaf f ) ↓ jk ( j u) (Node j k f ) = Node j k (map F j k (↓ j u) f ) ↓ ji u (Raw i g) = Raw i G i (↓ j u)(↓ jσ(1) (1 u)) . . . (↓ jσ(j) (j u)) g)
We establish the expected behavior of ↑ ji and ↓ ji with respect to shadows and prove that they are mutually inverse. The proofs proceed by induction on the raw type using very similar omitted auxiliary lemmas for ↑ jk and ↓ jk .

Lemma 2:

1) ok i u r = ⇒ ok i (u j) (↑ ji r); 2) ok i (u j) r = ⇒ ok i u (↓ ji u r); 3) ok i u r = ⇒ ↓ ji u (↑ ji r) = r; 4) ok i (u j) r = ⇒ ↑ ji (↓ ji u r) = r.
Since every pair of arrows in Figure 1 is mutually inverse (when applied to elements of the right shadow), we obtain our desired isomorphism property for Ctor i and dtor i .

Theorem 3: dtor i (Ctor i g) = g and Ctor i (dtor i t) = t. Finally, we prove characteristic theorems for T i 's BNF constants. We focus on the property that map T i commutes with the constructor Ctor i . The theorems for the relator, the predicator, and the set functions are proved analogously.

Theorem 4: map T i f (Ctor i g) = Ctor i (map R i f g) where α R i = (α, (α F 1 ) T σ(1) , . . . , (α F j ) T σ(j) ) G i and map R i is the map function associated to this composite BNF.

The proof of Theorem 4 relies on commutation properties of map raw i and ↑ ji and of map sh k and ↑ jk that can be proved by induction. This is a pervasive pattern when defining recursive functions on nonuniform datatypes.

Lemma 5: map sh k f (↑ jk s) = ↑ jk (map sh k (map F j f ) s) and

map raw i f (↑ ji r) = ↑ ji (map raw i (map F j f ) r).

D. Codatatypes

The construction can be gracefully extended to support codatatypes, which are types whose elements may be infinitely deep. Codatatypes are the types T i that are greatest solutions to equation ( 1).

This change in semantics needs to be reflected only at the raw level. Accordingly, the raw i types are defined as mutually corecursive uniform types. The shape types remain unchanged, since even in an infinitely deep object all type arguments are finite (but unbounded) type expressions.

The subsequent changes are also minor. The predicates ok i are defined as a mutual greatest (or coinductive) fixpoint of the same introduction rule as before for datatypes. The functions ↑ ji and ↓ ji are defined by primitive corecursion using the same equations as before.

All theorems from Subsections III-B and III-C hold as stated also for codatatypes. The proofs, however, are different: For example, whereas Lemma 2(1-2) was proved by induction on r, for codatatypes the corresponding argument proceeds by coinduction on the now coinductive definitions of ok i . Similarly, the equational statements (e.g., Lemma 2(3-4) or the raw part of Lemma 5) are proved by coinduction on =.

IV. THE NONEMPTINESS PROBLEM

Types in HOL must be nonempty. As we are developing more sophisticated high-level datatype specification mechanisms, the problem of establishing nonemptiness of the introduced types becomes more difficult. For nonuniform mutual (co)datatypes T i , the question is whether T i are indeed valid HOL types, i.e., are nonempty. We want an answer that is automatic (i.e., is given without asking the user to perform any proof) and complete (i.e., does not reject valid types).

In previous work, we offered a solution for mutual uniform (co)datatypes [START_REF] Blanchette | Witnessing (co)datatypes[END_REF]. It is based on storing, for each BNF α K with α = (α 1 , . . . , α n ), complete information on its conditional nonemptiness, i.e., on which combinations of nonemptiness assumptions for the argument types α i would be sufficient to guarantee nonemptiness of α K. For example, if n = 3 and α K is α 1 stream + α 2 × α 3 , then for α K to be nonempty it suffices that either α 1 , or both α 2 and α 3 be nonempty. We say that both {α 1 } and {α 2 , α 3 }, or, simply, {1} and {2, 3} are witnesses for the nonemptiness of α 1 stream + α 2 × α 3 .

The above discussion assumes that K operates on possibly empty collections of elements (which, technically, as a type constructor, it does not, since the HOL type variables are assumed to range over nonempty types). To model this, we employ the set K operators to capture the action of K on sets, as the homonymous constant K :

α 1 set → • • • → α n set → (α K) set, defined by K A 1 . . . A n = {x : α K | ∀i ∈ [n]. set i K x ⊆ A i }.
The constant K operates on sets in the same way as the type constructor K operates on types. Since sets can be empty, we can use them to express witnesshood.

Given I ⊆ [n], we call I a witness for K if, for all sets A, ∀i ∈ I. A i = ∅ implies K A = ∅. A set I ⊆ [n] set of witnesses for K is called perfect if for all witnesses J ⊆ [n] there exists a witness I ∈ I such that I ⊆ J. Thus, a perfect set of witnesses for K is one where no witness is missed, in that any witness J is equal to, or improved by, a witness I ∈ I .

We fix a definition of i mutual nonuniform datatypes T i , as depicted in equation ( 1) from Section III-B. We assume that the involved BNFs (the G i 's and the F jk 's) are endowed with perfect sets of witnesses I (G i ) and I (F jk ). We will show how to effectively construct perfect sets of witnesses for the T i 's. This construction allows us to decide whether the T i 's are nonempty, hence valid HOL types, by simply checking if their perfect sets are nonempty. In addition, it equips the T i 's with the infrastructure needed to establish the nonemptiness of future (co)datatypes that may use them as parameters.

To find the witnesses for the T i 's, we generalize the approach we developed for uniform datatypes. We define a context-free set-grammar (which is like a standard context-free grammar except that its productions act on finite sets instead of words) having the T i 's as nonterminals and the argument types α i as terminals. The productions of the set-grammar follow the direction of the destructors, α T i dtor i -→ (α, αT 1 , . . . , αT i ) G i , with each T i deriving sets containing the nonterminals T i and the terminals α k allowed by witnesses of G i .

For the nonuniform case, when recursively applying productions α T i dtor i -→ (α, (α F 1 ) T σ(1) , . . . , (α F j ) T σ(j) ) G i following the definitions, the T i 's are applied to increasingly larger polynomial expressions involving the F jk 's. To keep the grammar finite, we take a more abstract view, retaining from the F jk -expressions only their witness-relevant information, obtained by suitably combining their perfect sets I (F jk ). We define the set PolyWit, of polynomial witness sets (or polywits), inductively as follows:

• If k ∈ [k], then {{k}} ∈ PolyWit. • If ( j, k) ∈ [j] × [k]
I∈I (F jk ) { k ∈I J k | J ∈ ∏ k ∈I p k }.
This composition captures the computation of witnesses for the composition of F jk with the BNFs corresponding to the polywits p 1 , . . . , p k .

We fix a set of tokens, Tok = {t i | i ∈ [i]}, to symbolically represent the T i 's. We define the set-grammar Gr = (Term, NTerm, Prod) as follows. Its terminals are [k], i.e., one number k ∈ [k] for each type variable α k . The nonterminals are either polywits or have the form (p 1 , . . . , p k ) t i , where each p k is a polywit and i ∈ [i]. There are two types of productions:

1) p -→ I, where p ∈ PolyWit and

I ∈ p; 2) p t i -→ Γ J where i ∈ [i], J ∈ I (G i ) and Γ J = {p k | k ∈ J ∩ [k]} ∪ {(p • I (F j1 ), . . . , p • I (F jk )) t σ( j) | k + j ∈ J}.
The first type of production selects witnesses from polywits. The second type mirrors the recursion in the definition of the T i 's by following the destructors and selecting the terminals and nonterminals according to the witnesses of G i .

Let Lang i (Gr) be the language (i.e., the set of subsets of [k]) generated by Gr starting from the nonterminal ({{a 1 }}, . . . , {{a k }}) t i (the token for T i applied to the trivial polywits for its argument types). Let Lang ∞,i (Gr) be the language cogenerated by Gr-allowing infinite chains of productions, and infinite derivation trees-again, starting from ({{a 1 }}, . . . , {{a k }}) t i .

Theorem 6: If we interpret the definition as specifying mutual datatypes, then the definition is valid in HOL (i.e., the specified types are nonempty) if and only if Lang i (Gr) = ∅ and Lang i (Gr) is a perfect set of witnesses for T i . If we interpret the definition as specifying mutual codatatypes, then the definition is always valid in HOL and Lang ∞,i (Gr) is a perfect set of witnesses for T i .

The theorem statement distinguishes the nonemptiness subproblem from the witness problem. This is because the T i 's cannot be introduced as types without knowing their nonemptiness (i.e., the nonemptiness of their representing predicates ok i []). For codatatypes, nonemptiness always holds owing to the greatest fixpoint nature of the construction.

Since the raw i 's are BNFs, we have a perfect set of witnesses for them, but these will usually fail to satisfy ok i [] (and even if they do satisfy the predicate, they need not constitute a perfect set for T i ). To prove the theorem, we adapt the notion of witness from types to predicates and show that the languages (co)generated by Gr offer perfect sets for ok i u for any shadow u. We generalize from [] to an arbitrary u because the shadow increases along applications of the raw i destructors. Our technical report [12, Appendix B] provides the details.

For any finite set-grammar Gr, the languages Lang i (Gr) and Lang ∞,i (Gr) are effectively computable by fixpoint iteration [START_REF] Blanchette | Witnessing (co)datatypes[END_REF]. Moreover, iteration needs at most a number of steps equal to the number of nonterminals [14, Section 4.3]. For uniform datatypes, this number is precisely that of mutual types, i; for nonuniform datatypes, it is the larger number j × k × |PolyWit|, where |PolyWit| = O(2 2 k ). Fortunately, the worst-case double exponential in k is unproblematic in practice for two reasons. First, the defined types tend to have few type variables. Second, the nonemptiness witnesses for the BNFs G i can prune a large part of the search space: If a G i has a constructor without recursive arguments, then {} is a witness for G i and thus also for the (co)datatype T i regardless of k.

Consider the following contrived nonuniform codatatype of alternating streams over α 1 and α 2 :

(α 1 , α 2 ) alt ∞ = C α 1 ((α 2 , α 1 ) alt) | D α 2 ((α 2 , α 1 ) alt) We have i = 1, j = 1, k = 2, σ is the unique function from [1] to [1], (α 1 , α 2 ) F 11 = α 2 , (α 1 , α 2 ) F 12 = α 1 , and (α 1 , α 2 , α 3 ) G 1 = α 1 × α 3 + α 2 × α 3 .
Thus, {{2}}, {{1}}, and {{1, 3}, {2, 3}} are perfect sets of witnesses for F 11 , F 21 , and G 1 , respectively. Figure 2 shows two infinite derivation trees from the initial nonterminal ( 1 , 2 ) t 1 in the grammar Gr associated with this definition, where we write 1 and 2 for the polywits {{1}} and {{2}}. The trees repeat the same pattern after reaching ( 1 , 2 ) t 1 . In the left tree, the top production is ( 1 , 2 ) t 1 -→ { 1 , ( 2 , 1 ) t 1 }; this is a valid production of type 2, based on G 1 's witness {1, 3}. The tree's other production of type 2, ( 2 , 1 ) t 1 -→ { 1 , ( 1 , 2 ) t 1 }, uses the other witness, J = {2, 3}. The frontiers of the two trees are {1} and {2}, respectively. The set {{1}, {2}} is perfect for alt.

( 1 , 2 ) t 1 1 1 ( 2 , 1 ) t 1 1 1 ( 1 , 2 ) t 1 . . . ( 1 , 2 ) t 1 2 2 ( 2 , 1 ) t 1 2 2
( 1 , 2 ) t 1 . . . Even though alt is always nonempty (since it is a codatatype), a perfect set of witnesses is necessary to decide the overall nonemptiness problem. If we used an imperfect set such as {{1, 2}}, we would reject valid datatypes such as α fractal = Fractal ((α, ((α, α) alt) fractal) alt), where we must know that {{1}} is a witness for alt to infer nonemptiness.

V. (CO)INDUCTION PRINCIPLES

In a proof assistant, high-level abstractions are pointless unless they are supported by a reasoning apparatus. Just like the types themselves, reasoning principles for nonuniform (co)datatypes can be derived in HOL. To avoid cluttering the ideas with technicalities, in this and the next section we discuss the restricted situation of a single (co)datatype α T defined as fixpoint isomorphism α T (α, α F T ) G as in Section III-B but with i = j = k = 1. We reuse the infrastructure from that section but omit most indices.

(Co)induction involves reasoning about the elements of a (co)datatype and those of their (co)recursive components. BNFs allow us to capture components abstractly, in terms of the "set" operators. For example, for any element r of the uniform (co)datatype α raw, its components are the elements r of set 2 G (unRaw r)-because, in its fixpoint definition, raw appears recursively as the second argument of G.

A. Induction

Induction for uniform datatypes can be smoothly expressed in HOL. For example, the induction principle for α raw is the following HOL theorem, which we will refer to as Ind raw :

∀Q. (∀r : α raw. (∀r ∈ set 2 G (unRaw r). Q r ) = ⇒ Q r) = ⇒ ∀r : α raw. Q r
It states that to show that a predicate Q holds for all α raw, it suffices to show that Q holds for any element r given that Q holds for the recursive components set 2 G (unRaw r) of r. As we remarked in Section I, a verbatim translation of Ind raw for T would not be typable, since Q would be a variable used with two different types. But even if we change Q from a quantified variable to a polymorphic predicate Q : α raw → bool (and remove the outer ∀), the formula would be unsound, due to the cross-type nature of the T components: Whereas t has type α T, its components t have type α F T. For example, if Q is vacuously false on the type nat F T, we could use such an induction theorem (with α instantiated to nat) to wrongly infer that Q is true on nat T.

On the other hand, for each polymorphic predicate P : α T → bool, we can hope to prove the following inference We start by defining Q to be P • Abs and try to prove ∀r. ok [] r = ⇒ Q r using Ind raw , hoping to be able to connect the hypothesis of Ind P T with that of Ind raw . We quickly encounter the following problem, depicted in Figure 3.1 Suppose r : α raw corresponds to t : α T (via the embedding-projection pair); then T-induction speaks about the T components t : α F T of t, which do not correspond to the raw components r : α raw of r, but rather to elements r : α F raw of the form ↓ [] r . This mismatch is a consequence of our representation technique: To represent T's destructor using raw's destructor, we applied the "correction" ↓ []. To cope with it, we appeal to the shape type α sh, which in the simplified setting amounts to α + α F + α F 2 + • • • and thus includes all the types inhabited by t, its components, the components' components, and so on.

So we weaken our goal and try to prove that P holds for types of the form α sh T. For Q, this means switching from α raw to α sh raw. As shown in Figure 4, now we can travel from the type α sh F raw back to the type α sh raw, by applying Node to level the nonuniformity F into the larger type sh. For this to work, Q must reflect map raw Node, i.e., have Q (map raw Node r ) imply Q r .

Another issue is that r = map raw Node r is not in the image of Rep: r has shadow [START_REF] Abbott | Representing nested inductive types using W-types[END_REF] instead of the required [].

We must generalize the goal to arbitrary shadows, i.e., to α sh raw

↓ ↓ ↑ ↑ u / / unRaw α sh raw unRaw Abs / / α sh T dtor (α sh sh, α sh raw) G id ↓ ↑ [] (α sh sh, α sh raw) G ↓ ↓ ↑ ↑ u ↓ ↓ ↑ ↑ (1 u)
/ / (α sh sh, α sh raw) G (α sh, α sh F T) G

: ∆ → α sh raw → bool that extends Q in that Q [] = Q.
To this end, we define ↓ ↑ : ∆ → α sh raw → α sh raw, an operator that generalizes the trip from r to r to r described above to an arbitrary shadow u, and ↓ ↓ ↑ ↑, the cumulative iteration of ↓ ↑:

↓ ↑ u r = map raw Node (↓ u r) ↓ ↓ ↑ ↑ [] r = r ↓ ↓ ↑ ↑ (u 1) r = ↓↑ u ( ↓ ↓ ↑ ↑ u r)
Intuitively, we can regard the elements of both β sh and β raw as trees with β leaves and whose nodes branch according to F. Then ↓ ↑ traverses elements of α sh raw until it reaches their innermost nodes (with only leaves, i.e., elements of α sh, as subtrees) and immerses them as top nodes in the inner shape layer. The additional shadow argument u is needed to identify when an innermost tree has been reached (since we count on well-behavedness of ↓↑ u r only if ok u r).

The sh counterparts of the above, ↓↑ : ∆ → α sh sh → α sh sh and ↓ ↓ ↑ ↑ , are defined similarly (using map sh instead of map raw ). The key property of the "immerse" family of operators is that they commute with raw's destructor in the following sense.

Lemma 7: The left subdiagram in Figure 5 is commutative. Now, we can take Q u r to be Q ( ↓ ↓ ↑ ↑ u r). Q can be proved by raw-induction on r, since it achieves the desired correspondence between the raw components and the T components (i.e., between the leftmost and rightmost edges of Figure 5). That the correspondence works is ensured by the diagram's commutativity, as a composition of two commutative subdiagrams (the left subdiagram by the above lemma and the right one by the definition of dtor).

Thus, assuming the hypothesis of Ind P T , we have proved ∀α. ∀r : α sh raw. ∀u : ∆. ok u r = ⇒ Q u r-in particular, ∀ α. ∀r : α sh raw. ok [] r = ⇒ Q r, which implies ∀α. ∀t : α sh T. P t. From this, we prove the more general fact ∀α. ∀t : α T. P t. It would suffice that P reflects map T Leaf : α T → α sh T. We can simply asume that P is injective-antitone-parametric (IAP), meaning that P (map T f t) implies P t for all t : α T and all injective functions f : α → β (including Leaf and Node). In conclusion:

Theorem 8: If P is IAP, then Ind P T is derivable in HOL. IAP is substantially weaker than (general) parametricity, which for P would mean P t ⇐ ⇒ P (map T f t) for all t and arbitrary functions f [12, Appendix A].

Due to the limitations of HOL, we were able to prove only a restricted form of induction. However, all formulas built from the usual terms used in functional programming and employing equality, the logical connectives, and universal quantifiers are IAP (if not fully parametric), and therefore fall within the scope of our theorem. The main outcasts are constants defined using Hilbert choice, existential quantifiers, and ad hoc overloaded constants.

B. Coinduction

We designed the above infrastructure, consisting of the "immerse" operators, to work equally well for the codatatype as it does for the datatype. When α T is a codatatype, these operators are defined in the same way and can be used to derive the soundness of a nonuniform coinduction rule under similar assumptions to the induction case (from the corresponding uniform coinduction on the raw type):

∀α. ∀t 1 , t 2 : α T. P t 1 t 2 = ⇒ rel G (=) P (dtor t 1 ) (dtor t 2 ) ∀α. ∀t : α T. P t 1 t 2 = ⇒ t 1 = t 2 Coind P

T

For this rule to be sound, P : α T → α T → bool must again interact well with injective functions, but this time in the opposite direction. We say that P is injective-monotoneparametric (IMP) if P t 1 t 2 implies P (map T f t 1 ) (map T g t 2 ) for all t 1 , t 2 : α T and injective functions f, g : α → β.

Theorem 9: If P is IMP, then Coind P T is derivable in HOL. Unlike IAP, IMP disallows the usage of the universal quantifier in P, while it allows the existential quantifier. This is a quite desirable symmetry: Induction requires the universal quantifier to perform generalization over non-inductive parameters. For coinduction, the existential quantifier takes this role.

VI. (CO)RECURSION PRINCIPLES

For nonuniform (co)datatypes to be practically useful, there must exist some infrastructure supporting (co)recursive function definitions. We start with datatypes and consider the following simple recursive function on powerlists:

split : (α × β) plist → α plist × β plist split Nil = (Nil, Nil) split (Cons (a, b) xs) = let (as, bs) = split (map plist swap xs)
in (Cons a as, Cons b bs)

Here, the pattern-matched variable xs has type ((α × β) × (α × β)) plist, and the auxiliary swap function is defined as swap

((a 1 , b 1 ), (a 2 , b 2 )) = ((a 1 , a 2 ), (b 1 , b 2 )).
The function split uses polymorphic recursion: Its type on the right-hand side of the specification is different from the one on the left-hand side. More precisely, the recursive call is applied to an argument of type ((α × α) × (β × β)) plist. None of the existing HOL-based tools for defining recursive functions support polymorphic recursion-the gap we are about to fill.

The split function is not primitively recursive in the standard sense: The recursive call is applied to a modified patternmatched argument map plist swap xs. However, the modification takes place through the map plist function, which leaves the length of xs unchanged. Hence, such generalized primitively recursive specifications are terminating.

A. Recursion

Primitively recursive specifications in HOL are reduced to nonrecursive definitions using a recursion combinator [START_REF] Blanchette | Truly modular (co)datatypes for Isabelle/HOL[END_REF]. The equally expressive but less convenient primitively iterative specifications can be reduced as well, using a simpler fold combinator. For a uniform datatype α T = Ctor ((α, α T) G) (e.g., α T = α list with (α, β)

G = unit + α × β), the fold combinator has type ((α, β) G → β) → α T → β. A function f = fold b for some fixed b : (α, β) G → β, satisfies the characteristic recursive equation f (Ctor g) = b (map G id f g).
We call b the blueprint of f. Note that b describes how to combine the results of the recursive calls into a new result of type β. The recursion combinator's blueprint, of type (α, α T ×β) G → β, generalizes fold's blueprint by providing access to the original α T values, in addition to the results of the recursive calls. For simplicity, we focus on iteration.

For a nonuniform datatype α T = (α, α F T) G, the natural generalization of fold would be a combinator of type

∀Y. (∀α. (α, α F Y) G → α Y) → β T → β Y
where the universally quantified type constructor Y captures the positions where α have to be replaced by α F, since the recursive calls will be applied to a term of type α F T. The explicit universal quantification over α indicates that the blueprint needs to be truly polymorphic in α.

The primitive iteration schema provided by the above combinator is very restrictive, because it forces the type argument β of T to be fully polymorphic. Neither the split function nor a simple summation of a powerlist can be expressed using that fold. To overcome this limitation, Bird and Paterson [START_REF] Bird | Generalised folds for nested datatypes[END_REF] propose a generalized fold of type

∀X Y. (∀α. (α X, α F Y) G → α Y) → (∀α. α X F → α F X) → β X T → β Y
where the second argument enables recursive functions of a more refined type β X T → β Y by providing a distributive law a : ∀α. α X F → α F X which we call the (argument) swapper.

Bird and Paterson require X and Y to be functors and the two arguments b and a to be natural transformations. The function f = fold b a is then a natural transformation as well and satisfies

f (Ctor g) = b (map G id (f • map T a) g) (2)
It is straightforward to allow functors X and Y to be of arbitrary arity n. The function split can then be defined by setting n = 2, (α, where Inl and Inr are the left and right embeddings of +. For simplicity, the rest of this section assumes n = 1.

β) G = unit + α × β, α F = α × α, (α, β) X = α × β, (α, β) Y = α plist × β plist, a =
We propose an even more flexible fold combinator that replaces the functor F, which is fixed in the nonuniform datatype specification and appears in the recursive calls, with another arbitrary functor V of the same arity as F (here, 1):

∀X Y. (∀α. (α X, α V Y) G → α Y) → (∀α. α X F → α V X) → β X T → β Y
This allows the recursive calls to return a type α V Y instead of the fixed α F Y. The combinator satisfies the same characteristic equation ( 2) (with the more general types). All these expressive combinators for nonuniform types have one problem in common: In HOL, type constructor quantification and type variable quantification can only occur at the outermost level. Thus, it is impossible to define the fold constants for nonuniform datatypes.

Instead, we follow a similar route as for induction. We devise a recursion procedure that takes (here, unary) BNFs V, X, and Y,2 a blueprint b : (α X, α V Y) G → α Y and a swapper a : α X F → α V X as input and yields a function f : α X T → α Y satisfying equation [START_REF] Abel | Fixed points of type constructors and primitive recursion[END_REF].

The procedure defines a recursive function using b and a on the raw type and lifts it to the nonuniform type. To perform such a lifting for induction, the inductive property P must be a polymorphic IAP term. For recursion, we require both b and a to be polymorphic injective-parametric terms, i.e., parametric only for relations that are graphs of injective functions. This is a weaker assumption than Bird and Paterson's naturality assumption (e.g., map F (map X f ) = map X (map V f ) • a for a). On (bounded) natural functors, injective-parametricity implies the weak naturality assumption that demands for the above equation to hold only for injective functions f . Consequently, f will also only be a natural transformation for injective functions. By contrast, our construction is closed: If both b and a are fully parametric in some type parameters, f is fully parametric in the same type parameters.

The definition of f proceeds in four steps. First, we define a shape type sh V for V analogously to sh for F, including the constructors Leaf V , Node V , their inverses unLeaf V , unNode V , and the functions ok V , ↑ V , and ↓ V . Second, we lift a to shapes a : ∆ → α X sh → α sh V X by recursion on the shadow:

a [] = map X Leaf V • unLeaf a (1 u) = map X Node V • a • map F (a u) • unNode
Third, we define a raw version of our function f raw : ∆ → α X T → α sh V Y by primitive recursion:

f raw u (Raw g) = b (map G (a u) (map Y unNode V • f raw (1 u)) g)
The generalization to sh V in the return type of f raw is similar to what we did for induction. Finally, we define the function f

as f = map Y unLeaf V • f raw [] • Rep.
Figure 6 justifies the above definitions by proving equation [START_REF] Abel | Fixed points of type constructors and primitive recursion[END_REF]. Some of the arrows labeled by injective functions,

α X T f 1 2 Rep , , (α X, α X F T) G Ctor o o id map T a id Rep r r 3 α X raw f raw [] 4 (α X sh, α X raw) G Raw o o a [] f raw [1] (α X , α X F raw) G Leaf ↑ o o id map raw a (α sh V X, α sh V Y) G id map Y unNode V (α X , α V X raw) G id f raw [] id Abs / / (α X , α V X T) G id f t t α sh V Y 5 (α sh V X, α sh V V Y) G b o o (α X, α V sh V Y) G map X Leaf V map Y ↑ V m m 7 6 α Y map Y Leaf V 2 2 (α X, α V Y) G b o o id map Y Leaf V O O map X Leaf V map Y (map V Leaf V )
j j 1 Fig. 6. Proof of the recursive specification of the function f such as Leaf (V) and Node (V) (possibly under further maps), must be inverted for the diagram to make sense. Elements of the two highlighted types have shadow [START_REF] Abbott | Representing nested inductive types using W-types[END_REF]. All other elements of types sh, sh V , and raw in the diagram have shadow [].

Equation ( 2) is the outermost pentagon, which is filled by commutative diagrams starting by unfolding the definitions of f 1 (twice), Ctor 2 , and map T 3 as well as the recursive specification of f raw 4 . The quadrilateral 5 follows from the naturality for injective functions (Leaf V ) of b and 6 from the recursive specification of ↑ V . The remaining commutative pentagon 7 relates f raw and ↑ (similarly to Lemma 5 for map raw ); the proof follows by induction. Therefore, the property used in 7 for shadow [] must be generalized to an arbitrary u and requires an auxiliary fact about a and ↑ together with the facts that a and f raw preserve ok u and ok u. The proofs rely on the injective-parametricity of a and b.

Lemma 10: 1) ok u s = ⇒ pred sh V (ok V u) (a u s);

2) ok u r = ⇒ pred raw (ok V u) (f raw u r);

3) ok u s = ⇒ a (u 1) (↑ s) = map X ↑ V (a u (map sh a s));

4) ok u r = ⇒ f raw (u 1) (↑ s) = map Y ↑ V (f raw u (map raw a s)).
Requiring Y to be a functor is very restrictive, because it disallows many recursive functions with parameters. We generalize the entire construction to

α Y = α Y 1 → α Y 2 ,
where Y 1 and Y 2 are natural functors. This allows first-order arguments as well as higher-order arguments that do not refer to α in their domain. This generalization is straightforward but technically involved.

B. Corecursion

The recursion procedure is designed to work dually for codatatypes. The corecursion procedure mainly reverses function arrows: It takes the injective-parametric blueprint b : α Y → b : (α X, α V Y) G and swapper a : α V X → α X F as inputs and yields the function f : α Y → α X T, which satisfies

f y = Cons (map G id (map T a • f) (b y)).

VII. IMPLEMENTATION

To add support for nonuniform types to Isabelle/HOL, we followed the same general strategy as previously [START_REF] Blanchette | Truly modular (co)datatypes for Isabelle/HOL[END_REF]:

1) We formalized in Isabelle/HOL an abstract datatype example α T = Ctor ((α, α F T) G) as well as a codatatype.

2) We developed ML functions that generalize the abstract examples to produce the derivations for a concrete set of mutual types with an arbitrary number of type variables and to derive the nonemptiness witnesses.

3) We developed ML functions that extend the results of step 2 to multiple curried constructors-the high-level view presented to users.

4)

We developed the commands that process type and function definitions and that perform (co)induction.

For datatypes, step 1 starts by defining the type α T, Ctor, and the BNF constants; then it derives theorems about them and registers T as a BNF. This registration is performed by an existing Isabelle command that lifts the BNF structure of a type across an embedding-projection pair [START_REF] Biendarra | Functor-Preserving Type Definitions in Isabelle/HOL[END_REF]. Induction is formalized by deriving a lemma Q t in terms of a fixed but unknown polymorphic predicate Q that is IAP and inductive (i.e., (∀x ∈ set 2 G g. Q x) = ⇒ Q (Ctor g) holds). Recursion is formalized as a function f defined such that the recursive equation f (Ctor g) = b (map G id ( f • map T a) g) holds for a fixed injective-parametric blueprint b and swapper a.

The code for step 2 constructs the low-level types, terms, and lemma statements presented in Sections III to VI and proves the lemmas using specialized tactics-ML programs that generalize the proofs from the formalization. In principle, the tactics should always succeed, but it is necessary to execute them to obtain the highest level of trustworthiness. Assuming Isabelle's inference kernel is correct, bugs in the new commands might lead to run-time failures but never to logical inconsistencies. For step 3, we were able to generalize and reuse the infrastructure for uniform types that performs the same lifting from low to high level [START_REF] Blanchette | Truly modular (co)datatypes for Isabelle/HOL[END_REF].

Step 4 takes the form of six main commands available to the users and making definitions and reasoning about nonuniform types almost as convenient as for uniform types.

The nonuniform _ (co)datatype commands can be used to define nonuniform types. For example, the following definition introduces a type of λ-terms over variables drawn from α, with De Bruijn notation for bound variables [START_REF] Bird | De Bruijn notation as a nested datatype[END_REF]:

nonuniform _ datatype α tm = Var α | App (α tm) (α tm) | Lam ((unit + α) tm)
Entering a λ-abstraction (Lam) creates a new variable, which is accommodated by the extended type unit + α consisting of the values Inl () (the new variable) and Inr x for all x : α. The command performs the type construction and computes a nonemptiness witness. Then it defines the constructors Var, App, Lam and corresponding destructors and derives characteristic theorems about the constructors, the destructors, and the BNF constants map tm , pred tm , rel tm , and set tm . The nonuniform _ prim(co)recursive commands allow users to define primitively (co)recursive functions, by specifying their (co)recursive equations. 3 For example, the following definition introduces a function join that "flattens" a term whose variables are themselves terms:

nonuniform _ primrecursive join : α tm tm → α tm where join (Var

x) = x | join (App s t) = App (join s) (join t) | join (Lam u) = Lam (join (map tm (λx. case x of Inl () ⇒ Var (Inl ()) | Inr y ⇒ map tm Inr y) u))
The command extracts blueprints and swappers from the equations and emits parametricity proof obligations that must be discharged by the user. In the example, the swapper is the λexpression of type unit + α tm → (unit + α) tm that is passed to the outer map tm . Once the proofs are complete, the command derives a low-level characteristic theorem about the defined function, from which the user-specified equations follow.

One of the most basic operations on λ-terms is substitution: subst : (α → β tm) → α tm → β tm. Due to the limitation that arguments to recursive functions must be BNFs, we cannot define higher-order functions like subst that depend on a type variable that changes in the recursive calls. But we can define subst as a composition: subst σ = join • map tm σ.

The nonuniform _ (co)induct commands can be used to prove a lemma by (co)induction. For example, the command nonuniform _ induct s in subst_subst: subst τ (subst σ s) = subst (subst τ • σ) s emits proof obligations for parametricity and the three cases of the induction on s. Often, the parametricity proofs can be delegated to Isabelle's Transfer tool [START_REF] Huffman | Lifting and Transfer: A modular design for quotients in Isabelle/HOL[END_REF]. Once the obligations are discharged, the stated property is derived and stored under the specified name (subst_subst). For the technical reason given in Section V, the derivation can be performed only by an Isabelle command, not by a proof method as is done for uniform (co)datatypes [START_REF] Blanchette | Truly modular (co)datatypes for Isabelle/HOL[END_REF]. Unlike commands, proof methods can be invoked on arbitrary proof goals in the middle of a proof.

As a simple example involving nonuniform codatatypes, we prove the equivalence between two definitions of the constant powerstream. The required proofs are fully automatic after specifying the trivial bisimulation relation R l r ⇐ ⇒ ∃x xs. l = const x ∧ r = map pstream (λ_. x) xs in the coinduction proof: nonuniform _ codatatype α pstream = Cons α ((α × α) pstream) 3 The implementation of these two commands is incomplete at the time of this writing. We do not foresee any difficulties beyond those which we met for the other commands and expect to finish the implementation in the weeks following the submission deadline. The archive [START_REF] Blanchette | Formalization and implementation accompanying this paper[END_REF] will be updated. We generalized Okasaki's construction [START_REF] Okasaki | Purely functional data structures[END_REF] to a large class of datatypes. Nordhoff et al. [START_REF] Nordhoff | Finger trees[END_REF] partially relied on this construction (defining the sh and raw types but without introducing a new nonuniform type) in their Isabelle/ HOL formalization of 2-3 finger trees. We have not found any corresponding reduction of nonuniform to uniform codatatypes in the literature.

For recursion, we refined Bird and Paterson's generalized fold combinators [START_REF] Bird | Generalised folds for nested datatypes[END_REF] in several ways, including weakening the parametricity/naturality condition and enabling non-functor target domains. In turn, Bird and Paterson had improved on the standard sheaf-functor approach from category theory [START_REF] Lambek | Subequalizers[END_REF].

Our (co)induction principles take advantage of the BNF structure including set operators and relators. They constitute a lightweight alternative to fibration-based approaches [START_REF] Ghani | Generic fibrational induction[END_REF], [START_REF] Hermida | Structural induction and coinduction in a fibrational setting[END_REF] for the category of sets and functions. b) Comparison with Other Proof Assistants: Our work shows that nonuniform (co)datatypes and the associated polymorphic (co)recursion [START_REF] Henglein | Type inference with polymorphic recursion[END_REF], [START_REF] Mycroft | Polymorphic type schemes and recursive definitions[END_REF] can be supported in the minimalistic rank-one polymorphic framework of HOL, and therefore made available in HOL-based proof assistants, which cover about half of the theorem proving community.

The dependent type theory (DTT) camp, represented by Agda, Coq, Matita, and Lean, has sophisticated type systems built into their mechanized logic, including native nonuniform datatypes. Several case studies in these proof assistants exploit nonuniformity [START_REF] Benton | Strongly typed term representations in Coq[END_REF], [START_REF] Danielsson | Lightweight semiformal time complexity analysis for purely functional data structures[END_REF], [START_REF] Hirschowitz | Nested abstract syntax in Coq[END_REF], [START_REF] Naves | Balancing lists: A proof pearl[END_REF], [START_REF] Sozeau | PROGRAM-ing finger trees in Coq[END_REF].

Compared with the DTT systems, our support for nonuniform types in HOL has some limitations. Obviously, dependent families of (nonuniform) types cannot be expressed in HOL. In addition, Agda supports self-nested (co)datatypes-e.g., α bush = BNil | BCons α (α bush bush). Moreover, our (co)induction principles have some restrictions concerning (a weak form of) parametricity. The reason is that we cannot perform well-founded induction across types in HOL. Although practical predicates about functional programs obey them, the restrictions are not necessary semantically. Our technical report [START_REF] Blanchette | Foundational nonuniform (co)datatypes for higher-order logic[END_REF]Appendix D] presents an axiomatic extension that eliminates them. However, adding axioms, regardless of how provably correct they may be, is generally frowned upon by users of HOL-based systems.

Our approach derives some advantages from its categorytheoretical orientation. First, arbitrary parameter types, and not only (co)datatypes, are allowed in the specifications for nonuniform types, either inside or outside of the recursive occurrences in the specification. For example, the type stree from Section I is possible because the type α fset of finite sets is a BNF. This is excluded with DTT, which restricts datatypes to a predefined grammar. Second, since the foundational approach compels us to maintain the functorial structure to justify fixpoint definitions, users enjoy map functions and relators, as well as some polytypic properties directly or within immediate reach. Our nonuniform recursion principle delivers parametric functions, i.e., natural transformations. Moreover, the fusion laws [START_REF] Bird | Generalised folds for nested datatypes[END_REF] [12, Appendix C], which help reasoning about functional programs, depend on functoriality and naturality, and they are immediate in our framework. By contrast, in DTT, little structure is available for nonuniform datatypes after definition. In particular, map functions and relators are missing and can be tricky to add for some types.

c) Other Work: The pioneering work of Bird and his collaborators on nonuniform datatypes [START_REF] Bird | Nested datatypes[END_REF], [START_REF] Bird | De Bruijn notation as a nested datatype[END_REF], [START_REF] Bird | Generalised folds for nested datatypes[END_REF] has been extended in several directions, including structures for efficient functional programming [START_REF] Hinze | Efficient generalized folds[END_REF], [START_REF] Hinze | Finger trees: a simple general-purpose data structure[END_REF], [START_REF] Martin | Disciplined, efficient, generalised folds for nested datatypes[END_REF], datatypes with references [START_REF] Ghani | Representing cyclic structures as nested datatypes[END_REF], as well as work directly relevant for DTT proof assistants: reduction to W-types and container types [START_REF] Abbott | Representing nested inductive types using W-types[END_REF], typed term rewriting frameworks for total programming [START_REF] Abel | Fixed points of type constructors and primitive recursion[END_REF], [START_REF] Abel | Iteration and coiteration schemes for higher-order and nested datatypes[END_REF], [START_REF] Matthes | Recursion on nested datatypes in dependent type theory[END_REF], and induction in intensional DTT [START_REF] Matthes | An induction principle for nested datatypes in intensional type theory[END_REF]. Our contribution was concerned with bootstrapping nonuniform datatypes in HOL on a sound and compositional basis. Time will tell if Isabelle/ HOL users, or more generally the HOL community of users and researchers, will embrace nonuniform datatypes and their applications to the same extent as in advanced programming languages and type theories.

  Cons a (Cons (b 1 , b 2 ) (Cons ((c 11 , c 12 ), (c 21 , c 22 )) Nil))

∞=

  Cons α ((α × α) pstream) introduces "powerstreams," with infinite values of the form Cons a (Cons (b 1 , b 2 ) (Cons ((c 11 , c 12 ), (c 21 , c 22 )) . . .

  the encoding requires users to insert Leaf and Node coercions to convert an element such as (a, b), (c, d) : (α×α)×(α×α) to Node (Node (Leaf a, Leaf b), Node (Leaf c, Leaf d)) : α sh.

Fig. 1 .

 1 Fig. 1. Definitions of constructors and destructors

  and p 1 , . . . , p k ∈ PolyWit, then (p 1 , . . . , p k ) • I (F jk ) ∈ PolyWit. Polywits are sets of subsets of [k]. In the second clause above, we use the composition (p 1 , . . . , p k ) • I (F jk ), which is defined as

Fig. 2 .

 2 Fig. 2. Derivation trees in the witness set-grammar

Fig. 3 .Fig. 4 .T

 34 Fig. 3. The raw representation of T r α sh raw dtor

Leaf map raw Node•Rep o o Fig. 5 .

 o5 Fig. 5. Borrowing induction and coinduction from raw to T

  swap, and b (Inl ()) = (Nil, Nil) b (Inr ((a, b), ys)) = let (as, bs) = ys in (Cons a as, Cons b bs)

  nonuniform _ primcorecursive const : α → α pstream const x = Cons x (const (x, x)) nonuniform _ coinduct R in const_alt: const x = map pstream (λ_ : α. x) xs VIII. DISCUSSION AND RELATED WORK a) Inspiration:

Starting with this figure, we replace map G f g arrow annotations with arrows carrying two labels: f to the right in the arrow's direction of travel and g to the left.

Strictly speaking, the boundedness assumption is not needed for X and Y, which implies that α set is permitted to occur in those type expressions.

We thank David Basin for supporting this research, Peter Lammich for pointing us to his work on finger trees and for formalizing Okasaki's construction for powerlists, Johannes Hölzl for taking the time to explain Lean's nonuniform datatypes, and Mark Summerfield and the anonymous reviewers for suggesting textual improvements. Blanchette has received funding from the European Research Council (ERC) under the European Union's Horizon 2020 research and innovation program (grant agreement No. 713999, Matryoshka). Popescu has received funding from UK's Engineering and Physical Sciences Research Council (EPSRC) via the grant EP/N019547/1, Verification of Web Services (VOWS). The authors are listed alphabetically.