Recursive Types

Many languages include the ability to define types in terms of themselves. This is essential for data structures such as linked lists and trees: a linked list node contains a reference to another linked list node, while tree nodes reference their child trees.

Fixed Points

As is usual in the study of programming languages, we give meaning to "circular" definitions of types such as t = t*t by considering the related function f(t) = t*t and looking for a fixed point of this function (i.e., a type u such that f(u) == u). This idea has been formalized in type systems by introducing recursive types: the type mu t. t*t is defined to be a fixed point of the function mapping the type t to the type t*t. Although many such fixed points may exist in general, we can uniquely determine one by choosing either the least fixed point or the greatest fixed point.

For example, we can define the type "list of integers" by stating that such lists are either nil or a cons pair containing an integer (the head) and list of integers (the tail). This "circular" definition of lists does not uniquely define the set of possible lists however; it is compatible both with the conclusion that all lists are finite (the least fixed point) and with the conclusion that lists may be finite or infinite (the greatest fixed point).

Equivalence of Types

If (mu t. t*t) is supposed to be a solution of the equation t=t*t, then if follows that we can expect (mu t. t*t) = (mu t. t*t) * (mu t. t*t) Hence equivalence of types is immediately non-trivial and two types can be equivalent without being the same. Since typecheckers typically must be able to determine type equivalence (e.g., to check that the type of a given argument is equal to the parameter type expected by a function) we need an algorithm that determines whether two types are equal or not.

Research Results

In Summer 2001, Andrew Schoonmaker (HMC '02) and I spent some time working with recursive types:

• Most studies of recursive types consider exactly that — recursive definitions of types. Andrew and I defined a system that allows both recursive types and recursively-defined collections (well, tuples) of types; the latter can be used to define mutually-recursive types in a direct fashion.
  
  
• Virtually all studies of recursive types assume that the only interesting equivalences between types are those created by the fold/unfold rule. Andrew and I designed a type-equivalence algorithm for the above system — which includes pairing and projections along with fold/unfold — and proved that the algorithm was correct (sound, complete, and terminating).
  
  
• Most studies of recursive types have assumed the fold/unfold rule, which states that mu t. F(t), the fixed-point of a function F on types, is equivalent to F(mu t. F(t)). An instance of this would be the equivalence (mu t. t*t) = (mu t. t*t) * (mu t. t*t) mentioned above. However, in practice it is sometimes useful to use a less general notion of equivalence, sometimes called Shao's rule; this states that mu t.F(t) = mu t.G(t) whenever F(mu t.F(t)) = G(mu t.G(t)). It turns out that this is implied by the fold/unfold rule, but not vice-versa. Andrew and I devised correctness proof for a type-equivalence algorithm for a version of the system for recursive types that uses coinduction and Shao's rule (instead of the full fold/unfold rule for recursive types) but without the pairing and projections.
  

Open Questions

This work was inspired by the observation that theorists and implementations sometimes add recursive types to already complex type systems (e.g., to extensions of F-omega, a language in which one can write functions mapping types to types and more) but no one had ever given a provably correct algorithm for typechecking this extension. As a first step in this direction, Andrew and I added recursive types to a system that permitted pairs of types and projections from such pairs, and showed that typechecking was still decidable. The next step would be to extend this to adding functions from types to types, as in F-omega, and to see if one can still obtain a correct algorithm for typechecking.

It is likely that the proof we obtained for the system having both the fold/unfold rule and pairs could be modified for a system with Shao's rule and pairs, but this has not yet been verified.

Finally, most papers on recursive types use a coinductive definition of equivalence, rather than an simpler inductive definition, even though in some cases (especially those using Shao's Rule) . There is an obvious way to define equivalence of recursive types inductively, and an obvious way to modify the standard equivalence algorithm, but it is not completely obvious that the resulting algorithm corresponds to the resulting inductive definition. It would be interesting to get a proof that they do indeed correspond.