# Recursive Types via Domain Theory

Functional programming languages often include recursive types, allowing programmers to define types satisfying a given isomorphism. Such types cannot all be interpreted as sets, but they can be understood using domain theory. We consolidate and present foundational techniques in domain theory to understand eager programming languages with recursive types from a categorical perspective. We define a category of domains with finite coproducts, a symmetric monoidal closed structure for eager products and functions, and least solutions of recursive domain equations, whose objects are retracts of a universal space and whose morphisms are continuous with respect to a topology of approximations.

# 1 Introduction

When writing code, it is common to use *recursive types* to represent data structures. As a simple example, one might want a type representing the natural numbers. The type of natural numbers can be characterized as the least type such that N \cong 1 + N; we will refer to constraints of the form X \cong F(X) as *domain equations*. In ML-style pseudocode, a least (i.e., inductive) solution to this type equation may be defined as follows:

Here, `Fold : 1 + N -> N`

is the name of the constructor. Via pattern matching, we define its inverse, `unfold : N -> 1 + N`

. Sometimes, types are informally thought of as sets; this type N is thought of as the set \mathbb{N} of natural numbers.

For a more unusual example, non-total programming languages (such as Standard ML, OCaml, and Haskell) allow the following pseudocode:

This defines a type C that is isomorphic to the “function space” from C to 2! In this case, set-oriented reasoning breaks down: by Cantor’s Theorem, there is no set C isomorphic to its power set, 2^C. However, types of this form are very powerful, underpinning unbounded recursion. For example, using C, we may write a diverging (i.e., “infinitely looping”) program by applying an element c : C to itself (up to the given isomorphism):

```
(* unroll : C -> 2 *)
val unroll = fn (c : C) => (unfold c) c
(* val diverge : 2 *)
val diverge = unroll (Fold unroll)
```

This example begins to demonstrate the power granted by recursive types.^{1}

In order to give a categorical account of languages with such unusual type isomorphisms, we must find a suitable category to work in. The category of sets has too many morphisms between each pair of objects, which prevents us from defining types like C; thus, we will work in a subcategory of *domains* that imposes further topological restrictions. In particular, this subcategory will be capable of expressing that some programs may be partially defined (i.e., diverge sometimes).

To model a reasonable eager functional programming language, we will ensure that this subcategory has finite coproducts, a symmetric monoidal closed structure for eager products and functions, and least fixed points of domain equations. We will not give a formal interpretation of a programming language into the category, but we will treat its objects as types and its morphisms as programs in the standard way.

# 2 Directed-Complete Partial Orders

We begin by defining a subcategory of \mathbf{Poset}, called \mathbf{DCPO}, whose objects will ultimately correspond to types. Objects of \mathbf{DCPO} will be posets with particular sensible least upper bounds.

We will understand each type as a DCPO D, where the elements of a type are simply the elements of UD. For x, y \in UD, we understand x \le_D y as “x is at most as defined as y”. For example, a diverging computation (i.e., “infinite loop”) will be less defined than a result value.

Well-behaved functions between DCPOs, known as Scott-continuous functions, should preserve the DCPO structure.

We may now define the category \mathbf{DCPO} of DCPOs in the obvious way.

The category \mathbf{DCPO} has plenty of structure, which will let us understand sum, eager product, and function types.

# 3 Diverging Computations and Partial Functions

As discussed in the introduction, in a programming language with recursive types, a computation may *diverge* (i.e., “infinitely loop”). While a *value* of Boolean type must be either 0 or 1, a *computation* of a Boolean may be a value 0 or 1, or it may diverge. Thus, for each DCPO D of values, we will define a corresponding DCPO {D}_\bot of potentially-diverging computations.

In an eager functional programming language, a function evaluates its definition and performs any suspended behaviors when applied to an argument. For example, values of the thunk type `unit -> t`

are computations of type `t`

, which may diverge when the function is applied to the unique value of type `unit`

(typically written `()`

). If `t`

corresponds to a DCPO D, we will see that `unit -> t`

corresponds to {D}_\bot. We may understand this phenomenon by viewing partiality as an effect, embodied by the *lift monad*.

Now, we may work in the Kleisli category of this monad, following the typical development by Moggi (1991) of categorical models of effectful eager functional programming languages.

Although \mathbf{DCPO} has products, the object D \times E from \mathbf{DCPO} is *not* a categorical product in {\mathbf{DCPO}_\bot}: the presence of the partiality effect breaks the existence condition of the universal property for products.^{2} Although \mathbf{DCPO} products are not categorical products in {\mathbf{DCPO}_\bot}, they will still be useful for understanding eager product types.

We will understand eager product and function types as \otimes and \multimap, respectively.

# 4 Domains as Retracts of a Universal Space

We may now define a category of domains in which we can solve domain equations, which will be a subcategory of {\mathbf{DCPO}_\bot}. Informally, a domain will be an DCPO whose elements can be encoded as sequences of bits.

We will sometimes write elements of \mathbb{U} as infinite streams s of the form ({x}, {s'}), where x \in {2}_\bot and s' is another infinite stream, in place of a function i \mapsto \begin{cases} x & i = 0 \\ s'(i - 1) & i > 0. \end{cases} Additionally, to disambiguate between the bottom element available from the Kleisli category and the bottom element of {2}_\bot, we will refer to the latter as \bullet (as in \mathbb{T}).

A domain will be a DCPO that can be encoded in the universal space \mathbb{U}. We formalize this encoding property using the categorical notion of retract.

With this definition in hand, we may define “domain” in this setting.

This category \mathbf{Dom} is what we were originally looking for: recursive types will make sense within \mathbf{Dom}. Let us now consider some examples of domains.

When working with coproducts, we write [-, -] for copairing, \iota_1 for the left injection, and \iota_2 for the right injection.

# 5 Recursive Types

We will now see that the category \mathbf{Dom} has least fixed point solutions to domain equations.

Using this construction, we can build inductive types in \mathbf{Dom}.

In these examples, F is built from coproducts and (monoidal) products. Our original goal was to define a type C isomorphic to C \multimap 2; however, this places C in a contravariant position, seemingly violating functoriality of F. However, in this category, we can understand internal homs as covariant in both positions.

Now, we may finally find the type C.

# 6 Domains via the Untyped \lambda-Calculus

Domains can alternatively be characterized as subsets of the universal domain, \mathbb{U}.

Other domains are defined similarly, “traversing” the data structure such that the fixed points are precisely the desired elements.

In fact, we can use the untyped \lambda-calculus to define such maps r. The untyped \lambda-calculus can be interpreted into a category with a *reflexive object*.

Going forward, we will omit \llbracket {-} \rrbracket_\varepsilon when defining maps using closed \lambda-terms. For example, we define the domain 2 as \text{FP}({\lambda({s}.\ {\textsf{if}({s};\ {\textsf{tt}};\ {\textsf{ff}})})}). More strikingly, we may use the strict \textsf{Y} fixed-point combinator to solve recursive domain equations.

# 7 Conclusion

In this blog post, we presented a well-known technique from domain theory for solving domain equations in a particular subcategory of \mathbf{Poset}. This subcategory, \mathbf{Dom}, has coproducts, is symmetric closed monoidal, and has least fixed points of domain equations.

Of course, this is only the very foundations of domain theory; there are many other connections to be explored. For example, the approach we considered here can be extended to support polymorphism via partial equivalence relations. Additionally, there are deep connections to computability theory discussed in the given references.

This post represents some of the many things I learned at the Topos Institute as a Summer Research Associate. I owe a great deal of gratitude to Dana Scott, who spent countless hours throughout the summer (and beyond!) sharing with me his vast experience in and passion for domain theory and programming languages. Additionally, I would like to thank David Spivak, Brendan Fong, and everyone at the Topos Institute for the support, guidance, and insightful conversations.

## References

*Handbook of Logic in Computer Science*, 3:167.

*Formal Models and Semantics*, 633–74. Elsevier. https://doi.org/10.1016/B978-0-444-88074-1.50017-2.

*Practical Foundations for Programming Languages*. Cambridge University Press. https://books.google.com?id=J2KcCwAAQBAJ.

*Call-By-Push-Value*. Dordrecht: Springer Netherlands. https://doi.org/10.1007/978-94-007-0954-6.

*Information and Computation*93 (1): 55–92. https://doi.org/10.1016/0890-5401(91)90052-4.

*Journal of Computer and System Sciences*17 (2): 209–36. https://doi.org/10.1016/0022-0000(78)90006-5.

*SIAM Journal on Computing*5 (3): 522–87. https://doi.org/10.1137/0205037.

*To H.B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism*.

*SIAM Journal on Computing*11 (4): 23. https://doi.org/10.1137/0211062.

## Footnotes

For a more detailed account of recursive types, including program-level recursion via such types, see Harper (2016), Chapter 20.↩︎

In fact, {\mathbf{DCPO}_\bot}

*does*have categorical products, defined as D \times_{\mathbf{DCPO}_\bot}E \triangleq{D}_\bot \times_\mathbf{DCPO}{E}_\bot. This is the “lazy product”, sometimes written \& (e.g., in substructural type theory). However, {\mathbf{DCPO}_\bot} does not have exponential objects. (Smyth and Plotkin 1982)↩︎In Plotkin (1978), this object is written \mathbb{T}^\omega. While it is understood in the category of pointed DCPOs with strict maps (and thus is not the equivalent object to \mathbb{U} here), an object is a retract of \mathbb{T}^\omega in this category iff it is a retract of \mathbb{U} in {\mathbf{DCPO}_\bot}.↩︎