# Topology of data types

## Lecturer

Martin Escardo, University of Birmingham
## Abstract

It is known from various lines of attack (intuitionistic and
constructive mathematics, recursion theory, domain theory,
programming language semantics, type-two theory of effectivity) that
domains of computation, or data types, are topological spaces, and
that computable maps are continuous. Moreover, the topologies that
arise are familiar. For instance, computable functions on infinite
sequences of binary digits are continuous with respect to the Cantor
topology. Many applications of the topology of data types are known
in the theory of computation. To give a simple example, it follows
from the compactness of the Cantor space that equality of
integer-valued predicates on the Cantor space is decidable.

We approach this from what we call \emph{synthetic topology}. The
idea is to define topological notions (such as continuous map, open
set, discrete space, Hausdorff space, compact space) by means of
familiar computational concepts (computable function, semidecidable
set, set with semidecidable equality, set with semidecidable
apartness, set over which one can universally quantify by
computational means), and prove topological theorems about them by
computational means. For example: (1) Compactness of the Cantor
space is proved by constructing a program for universally
quantifying over it. (2) The theorem that a compact subspace $Q$ of
a Hausdorff space $X$ is closed has the following computational
manifestation: If we can computationally tell distinct points of $X$
apart and we can computationally quantify over $Q$, then we can
computationally semidecide the complement of $Q$. The proof is the
evident algorithm that defines the semidecision function for the
complement of $Q$ from the apartness map of $X$ by universally
quantifying over $Q$.

At a later stage, we convince ourselves that both the synthetic
definitions and the computational proofs match the classical
topological ones. In fact, after having developed synthetic
topology, we turn the programme on its head: We show that one can
cheaply develop the core of classical topology via the
lambda-calculus.

## Material

See Martin's paper Topology of data types,
the course will cover Chapters 1-5, and some bits of Chapter 12.

Thorsten Altenkirch
Last modified: Thu Jan 29 12:24:11 GMT 2004