Types as sets

If one views a type as merely a set of values, type intersection is straightforward to define and understand (it is merely set intersection). If one adopts the classical view that a type is an algebra[8], however, it is much more difficult to define the meaning of intersection.

The author contends that it is not essential to view a type as an algebra. Types are useful because they provide structure and allow type checking. This can be done even if one views types merely as sets of values. In the rest of this paper, therefore, types are sets of values and $U$ will denote the set of all the values that can belong to a type.

The author contends further that in programming languages types play only one role: they serve as constraints on the domains and codomains of functions. That is, if $D$ and $C$ are types, and $f\; :\; U\; \to U$ is a function with domain constraint $D$ and codomain constraint $C$, then all programming languages require the definition of $f$ to conform to the following:

$f(x)\; =$ $$Undefined $if\; \$x$ \in $D\$$ f(x) $\in$C {$$Undefined} $if\; \$x$ \in $D\$$

Typically, an error is signaled when $f(x)$ returns Undefined (not be confused with non-termination or Bottom). In statically typed languages such errors are sometimes predictable by the compiler.

As a syntactic convenience, we will write $f\; :\; D\; \to \; C$ to show that $f\; :\; U\; \to U$ is a function with domain constraint $D$ and codomain constraint $C$.

The reader may be forgiven for being sceptical about the contention that types only serve to constrain functions. After all, types are used to declare variables and check assignments. What's that got to do with functions?

Everything, as long as we regard variables as functions whose definitions are provided and updated by assignment statements. In other words, a variable declaration such as

V : Some-type

must be regarded as syntactic sugar for

$v$ : {} $\to$ Some-type is a function whose evaluation rule will be supplied later on by an assignment statement and may be changed (as time progresses) by further assignment statements.

We will furthermore regard V to stand for $v()$ when used in an expression ($v$ can be denoted as Address(V)).