CS611 Lecture 32 Recursive Types 22 November 2006Lecturer: Dexter Kozen1 IntroductionMany programming languages have the ability to define recursive data types. For example, suppose we wantto define binary trees with integer data at the nodes. In Java we can writeclass Tree {Tree leftChild, rightChild;int data;}A binary tree is an object of this class. In ML we can writedatatype tree = Leaf | Node of tree * tree * intThese types are recursive because they are defined in terms of themselves.In the typed λ-calculus, we do not yet have any mechanism to define recursive types. We would like thetype tree to satisfytree = 1 + tree ∗ tree ∗ int, (1)where 1 (aka unit) represents the empty tree; in other words, we would like tree to be a solution of theequationα = 1 + α ∗ α ∗ int. (2)However, no such solution exists among the types we have seen so far.How might we augment our set of types to include solutions to recursive typ e equations such as (2)?There are two basic approaches, called the equirecursive and isorecursive approach, respectively.2 Recursive Types as Regular Labeled Trees—The Equirecursive ViewBy unwinding (2), we can see thatα = 1 + α ∗ α ∗ int= 1 + (1 + α ∗ α ∗ int) ∗ (1 + α ∗ α ∗ int) ∗ int= 1 + (1 + (1 + α ∗ α ∗ int) ∗ (1 + α ∗ α ∗ int) ∗ int) ∗ (1 + (1 + α ∗ α ∗ int) ∗ (1 + α ∗ α ∗ int) ∗ int) ∗ int= · · ·At each level, we have a finite type with the type variable α appearing at some of the leaves, and we obtainthe next level by substituting the right-hand side of (2) for α. This gives a sequence of deeper and deeperfinite trees, where each successive tree is a substitution instance of the previous tree.If we take the limit of this process, we have an infinite tree. We can think of this as an infinite labeledgraph whose nodes are labeled with the type constructors *, +, int, and 1. This is very much like an ordinarytype expression, except that it is infinite. There are no more α’s, because we have substituted for all of themall the way down. This infinite tree is a solution of (2), and this is what we take as the type tree.In general, let Σ be a signature consisting of several type constructors of various arities. For example,Σ might consist of the type constructors →, *, +, 1, and int. We can form the set of (finite) types over Σinductively in the usual way. Each such type can be regarded as a finite labeled tree. For example, the typeint → int → int can be viewed as the labeled treeintintint→→@@@@1Now let us add some infinite types. These are infinite labeled trees that respect the arities of theconstructors in Σ; that is, if the constructor is binary (such as * or →), any node labeled with that constructormust have exactly two children; and if the c onstructor is nullary, such at 1, then any node labeled with thatsymbol must be a leaf. Within these constraints, the tree may be infinite.A (finite or infinite) expression with only finitely many subexpressions up to isomorphism is called regular.For example, the infinite typeintintint...→→→@@@@@@is regular, since it has only two subexpressions up to isomorphism, namely itself and int. The limit of theunwinding of (2) above, which we took to be the type tree, is also regular; it has exac tly five subexpressionsup to isomorphism, namely tree, 1, tree * tree * int, tree * tree, and int.Regular trees are all we need to provide solutions to finite systems of type equations of the form (2).Supp ose we have n type equations in n variables:α1= τ1... (3)αn= τn,where e ach τiis a finite type over the typ e constructors Σ and type variables α1, . . . , αn. This system has asolution σ1, . . . , σnin which each σiis a regular tree. Moreover, if no right-hand side is a variable, then thesolution is unique.2.1 The µ ConstructorWe can specify the infinite solutions to systems of type equations (3) using a finite syntax involving a newtype constructor µ, the fixpoint type constructor. If we have an equation α = τ such that the right-handside is not α, then there is a unique solution, which is a finite or infinite regular tree. The solution will beinfinite if α occurs in τ and will be finite (in fact it will just be τ) if α does not occur in τ . We denote thisunique solution by µα. τ.Syntactically, µ acts as a binding operator in type expressions as λ does in λ-terms, with the same notionsof scope, free and bound variables, α-conversion, and safe substitution.Since µα. τ is a solution to α = τ, we haveµα. τ = τ {µα. τ /α}. (4)For example, to get a tree type satisfying (1), we can definetree4= µα. 1 + α ∗ α ∗ int.The desired equation (1) is just (4) for this case.The solutions σ1, . . . , σnto any finite system of the form (3) can be expressed in terms of µ. For example,suppose τ1and τ2are finite type e xpressions over the type variables α1, α2such that neither τ1nor τ2is avariable. The systemα1= τ1α2= τ2has a unique solution σ1, σ2specified byσ1= µα1. (τ1{µα2. τ2/α2}) σ2= µα2. (τ2{µα1. τ1/α1}).Mutually recursive type declarations arise quite often in practice. For example, c onsider the followingJava class definitions for Node and Edge:2class Node {Edge[ ] inEdges, outEdges;}class Edge {Node source, sink;}Note that Node refers to Edge and vice versa. So we must take a mutual fixpoint when assigning types.2.2 Typing RulesIn the equirecursive view, since µα. τ = τ {µα. τ /α}, the typing rules are quite simple:(µ-intro)Γ ` e : τ {µα. τ /α}Γ ` e : µα. τ(µ-elim)Γ ` e : µα. τΓ ` e : τ {µα. τ /α}Equivalently, we can just allow substitution of equals for equals in type expressions.3 Folding and Unfolding—The Isorecursive ViewThere is another approach to recursive types, the isorecursive approach. Here we do not have any infinitetypes, but rather the expression µα. τ is itself a type. In this approach, µα. τ and τ {µα. τ/α} are considereddifferent (but isomorphic) types .The step of substituting µα. τ for α in τ is called unfolding, and the reverse operation is called folding.The conversion of elements between these two types is accomplished by explicit fold and unfold operations.unfoldµα. τ: µα. τ → τ {µα . τ/α}foldµα. τ: τ {µα. τ /α} → µα. τ(we suppress the subscripts when there is no ambiguity). In this view, the equality symbol in (4) is notreally an