Computer Science 591i
Types from an Algebraic Standpoint

The Aim of this Approach

Type theory is usually seen as being distinct from the ideas of evaluation that we have explored previously. There certainly are similarities, for example ascribing a type to an expression makes use of the concept of environment as does ascribing a value. Here, however, I want to explore the possibility of an identification in which a system of types is a combinatorial model, that a type-theory is a kind of Lambda theory, and that ascribing a type to an expression is evaluation.

The utility of type models is that they are smaller than models in which a general computation can be supported. This means that they can serve a useful purpose in predicting whether an error will occur.

Types of Object, Type Errors.

In Computer Science, types serve two major purposes:

In their first role, type-systems can be regarded as a kind of weak logic, capable of inferring that certain events, called type-errors cannot occur. The most important property of a type system is that type-correctness of a program must be decidable. From this requirement, it is clear that not all errors are type-errors, since failure of a program to terminate should clearly be regarded as an error, but the halting problem is undecidable.

If we want to examine the idea of a type-system from the point of view of Combinatory Models, the natural approach is to introduce the idea of a set of exceptions in the model. If an expression can evaluate to an exception, then it should be regarded as erroneous.

Definition

A applicative algebra with exceptions is a triple = <D, > Here EX1 takes precedence over EX2, so that ( 1 2) = 1.

Definition

A combinatory algebra with exceptions is a quintuple = <D,,S, K, > which is an applicative algebra with exceptions, and where S, K are Shonfinkel combinators obeying:

Discussion - A Calvinistic View of Exceptions

The above concept of exception clearly amounts to treating an exception as a fatal error in a computation, from which there is no recovery. This "Wee Free" view of the matter stands in contrast to the general practice of programming language design, in which a computation may be snatched from a free fall occasioned by an exception by the intervention of a handler. Clearly we could develop a concept of exception handlers, which transform an exception to a non-exception. However it would complicate our system unduly.

Definition

Let be a combinatory algebra, with exception set . We say that p in is a procedure if for some d | | , the application (p u) is not in .

We denote the type of procedures of by Proc().

Definition

Let be an applicative algebra. Then a type T is a subset of .

Discussion

The above definition of type is non-constructive. It will serve nevertheless to establish some basic attributes of types. Naturally we will have to find a way of constructively specifying a range of types sufficiently diversified as to support worthwhile discovery of erroneous code. However our investigation of non-constructive types will identify operations that we need to perform constructively.

Definition

If is a combinatory model and TD and TR are types of , then TD TR is the type

If d , we say that d has the (weak) type TD TR if d TD TR.

The Functional Scheme Model

A particular combinatory model which is of interest is the Functional Scheme Model (FSM) which implements the basic functional components of the Scheme language. We shall denote types of the FSM by upper-case bold identifiers, and particular elements of the FSM by lower-case bold identifiers or signs (+, -, *, /, . . .)

It should be noted that given our existing type-descriptive apparatus no unique procedure-type can be ascribed to a procedure. For a given procedure object d it is possible that p TD1 TR1 and also p TD2 TR2 where there is way of expressing these two relationships in the form of p TD3 TR3 without losing useful discriminatory power. For example, the absolute value procedure in the FSM has among its types:

But the second of these statements does not subsume the first, because the first statement tells us the relevant fact that if we give abs an integer as argument it returns an integer as result.

Lemma (contravariance of domain, covariance of range)

If TD1, TD2, TR1, TR2, are types for which TD2 TD1 and TR1 TR2, then

Proof

Let p TD1 TR1 . Then (p d1) TR1 for all d1 TD1 .

But TD2 TD1. Hence for all d2 TD2, (p d2) TR1. Since however TR1 TR2 , we see that (p d2) TR2 .

Thus we have shown that any p TD1 TR1 maps TD2 to TR2, thus establishing our lemma.

A consequence of the contravariance rule is that, for example, despite the fact that Integer Number, the type Integer Integer is not contained in the type Number Number. Thus, for example, the intersection

is non-redundant.

A simple converse of these two lemmas is clearly not true of all combinatory algebras. for consider a combinatory algebra without procedure objects. Then TD TR is always the empty-set for any TR which contains no exceptions, so that TD1 TR1 TD2 TR2 is true for any combinatory algebras and ranges whatever.

The Type of Shonfinkel Combinators.

Since the combinators are denizens of every combinatory algebra, let's start with their type.

Lemma

If T is a type, then I TT

Proof

Let t T. Then I t = t. Thus I TT.

Lemma

If T1 and T2 are types, then K T1 T2 T1

Proof

Let t1 T1, consider (K t1). For all t2 T2, (K t1) t2 = t1. Thus (K t1) T2 T1. Hence K T1 (T2 T1)

Lemma

If T1, T2, T'2 and T3 are types of a combinatory algebra where T'2 T2 , then

Proof

It is sufficient to show that if f T1 T2 T3 then (S f) (T1 T'2) T1 T3

Hence it suffices to show that if, in addition, g T1 T'2 then (S f g) T1 T3 .

Hence it suffices to show that if, in addition, x T1 then S f g x T3 .

But S f g x = (f x) (g x). Since x T1 , and f T1 T2 T3 , it follows that (f x) T2 T3. Likewise (g x) T'2. But T'2 T2 , so that ((f x) (g x)) T3 . Hence (S f g x) in T3 , hence (S f g) in T1 T3 , hence (S f) (T1 T'2) T1 T3 , hence

One interpretation of the above results is that a particular type for one of the combinators is as an intersection. For example, for any two types T1 and T2:

And in general, for any family (Tj) of types:

Quotient Algebras

To an algebraist, the natural approach to types is to regard them as defining a congruence on an algebra. If two elements of an algebra belong to the same type, then they ought to be congruent - they ought to be mapped into the elements of an identical type (possibly different from the first) by the operation() of the algebra. This allows the algebraist to project the original algebra onto a quotient algebra, which she hopes will be sufficiently simple to allow her to make useful predictions about the big algebra.

This is quite easily realised in a simple applicative algebra. For example, consider an algebra which has the Scheme integers and floats, together with the abs procedure, which takes the absolute value of a number. Then we can take Integer, Float, {abs}, as separate types, obtaining a finite applicative algebra:

A projection mapping always induces a partition of its domain into pairwise disjoint sets whose union is the whole domain.

Definition CP

Let = <D, >,be a applicative algebra. Suppose we have a family of types T1, T2, . . . which form a partition of D, that is, they are non-empty, pairwise disjoint [that is Ti Tj = for all i j] and the union T1 T2, . . . = D . Suppose also that, for all Ti for some j, and also for some j. Then we say that T1, T2, . . . form a congruence partition of .

Lemma

Let = <D, > be an applicative algebra with a congruence partition T1, T2, . . .. Define (Ti Tj) to be Tk where for some ti Ti, tj Tj we have (ti tj) Tk. Then the types T1, T2, . . .. form an applicative algebra.

Proof

We need to show that the operation on the types is well defined.

Let ti, t'i Ti and tj, t'j Tj Let (ti tj) . Tk. Then (ti t'j) Tk by HM1, and hence (t'i t'j) . Tk by HM2. Thus the operation is well-defined.

Given a congruence partition of an applicative algebra, where d Ti we write [[d]] for Ti. Thus from definition CP we see that

Suppose our applicative algebra is a combinatory algebra. Then it is easy enough to extend the above lemma to show that a congruence partition of our combinatory algebra is itself a combinatory algebra. Since K and S are defined equationally, the following lemma is an instance of a well known theorem of Universal Algebra. However, we give here an elementary proof.

Lemma

Let = <D,, S, K> be a combinatory algebra with a congruence partition T1, T2, . . .. Then the types of the partition form a combinatory algebra under the operation defined above.

Proof

To extend these ideas to a combinatorial model we need to meet the " conditions" of the combinatory model. But these are not equational, and so are not automatically satisfied by the idea of congruence as defined, just as for example the quotient of an integral domain by an ideal is not necessarily an integral domain. Saying "there are no divisors of zero" is not an equational statement. Thus while the integers form an integral domain, the ring of integers modulo six has divisors of zero, namely [[3]] and [[2]].

We can approach this problem from another point of view. Let's introduce the idea of monomorphic procedure types

Definition

If is an applicative algebra with exceptions, and TD and TR are types of , then the monomorphic procedure type TD TR is the type

Discussion

The above definition captures well the idea of monomorphic procedure types, as found for example in SML. In SML the sin procedure is monomorphic, that is the expression (sin t) is defined only for real t - it is erroneous to apply it to any other type of argument. In Scheme, if we regard the numbers as constituting one single type, then sin is likewise monomorphic.

The concept is of course too restrictive to serve to characterise all of the types of SML procedure, which are parametrically polymorphic. It' also too restrictive to characterise the S, K, I combinators which are likewise parametrically polymorphic. But it does give us a start in letting us create an applicative algebra of types with a simple definition of the operator, and which is extensional with respect to its procedure-types.

Definition

An applicative algebra with exceptions is said to be monomorphically partitioned by
(, T1, T2, . . .) if the Ti are either monomorphic procedure types or consist of non-procedures.

Lemma

Let be a partitioned applicative algebra. Then, if TD, TR and (TD TR) are members of the partition, ((TD TR) TD) = TR.

Proof

Let (p d) ((TD TR) TD), where p (TD TR). Hence (p d) TR. But, by definition of application in the quotient algebra, ((TD TR) TD) is a member of the partition, as is TR, by hypothesis. Hence, having p d in common, they are the same member of the partition.

Lemma

Let be a monomorphically partitioned applicative algebra. Suppose for all T in the partition where the monomorphic functional types TD1 TR1 and TD2 TR2 are members of the partition as are the non-exceptional TD1, TD2, TR1, TR2. Then

Proof

By the previous lemma, Let (p d) ((TD1 TR1) TD2) , where p TD1 TR1, d TD2. Now p is a member of the monomorphic procedure type TD1 TR1 Hence d TD1, for TR2 contains no exceptions, and p raises an exception for every argument not in TD1.

Thus TD1 and TD2 have an element in common, and being members of the partition, TD1= TD2

Also p d TR1 and p d TR2, since . d TD1 and d TD2. Thus TR1, TR2 have an element in common, and being members of the partition, TR1= TR2

Hence the result.

Discussion

We have shown above that a monomorphically-partitioned quotient algebra /( T1 . . .) has part of the requisite extensional property to render it a combinatorial model, assuming it contains the necessary combinators. However we have problems still.

It is not hard to construct monomorphically partitioned applicative algebras with a finite collection of procedure objects, and a finite partition. But adding combinators gives rise to an infinite collection of procedure objects, which require an extension of the idea of monomorphic functional types. Consider for example, the I combinator. It can take as its argument any object. However our requirement that objects be partitioned into distinct types does not allow us to have the idea of type-union, and indeed, a characterisation of I in terms of type-union is too imprecise. For, while I has the (weak) type TD TD where TD is the carrier set of , this does not capture the fact that I T T for all types T, that is to say, that I i (Ti Ti) for any family of types (Ti).

Note on exceptions

What we are dealing with here are essentially type exceptions. Non-type "exceptions" (e.g. division overflow) have to be included as objects in the appropriate type (e.g. a numeric type).