Cardelli and Wegner [CW85] give an account of how type systems arise naturally in programming languages, and indeed in human nature. "As soon as we start working in an untyped universe, we begin to organise it in different ways for different purposes." Thus, for example, the same bit pattern in a computer memory may be viewed in a number of different ways according to some properties of the entity it is intended to represent. The same bit patterns may be used to represent the character "a" and the number 97, but a programmer would normally wish to abstract over this fact.
This gives rise to the notion of a type system as an aid to modelling, by the provision of a set of regular interpretations of bit patterns. A programmer may think in terms of values modelled by a type system rather than in terms of a computer's memory state.
This modelling, however, may potentially be violated by the application of inappropriate operations. All values must be modelled by abstraction over bit patterns, but the operations available on bit patterns will not normally be appropriate over the models provided by a type system. Because of this, a type system usually also provides some mechanism by which the inappropriate application of operations is prohibited. Thus a type system is normally regarded as a provider of both modelling and protection within a programming system.
Safety and Flexibility
As always, however, the extra safety provided by the prevention of operations in certain contexts causes a loss of flexibility. For example, it is reasonable to prohibit an operation such as bitwise or on two values which represent integers. On the other hand, it may be convenient for a program to model an integer as a bit pattern, or vice versa, in which case the prevention of this operation is not desirable.
The level at which a type system's protection is specified varies widely between programming languages. Languages such as C [KR78] provide only a modelling role, and if desired any operation may be applied to values of any type. Such languages are very flexible, but at the cost of some safety. Many languages allow at least some operations which violate the type system, for example it is not uncommon to be able to index past the bounds of an array. Again, this allows extra flexibility, but at the cost of safety.
A language whose type system prevents any operations which violate its modelling facilities is referred to as a strongly typed language. Before strong typing is enforced in a programming language, the designers must be confident that the modelling provided by the type system is adequate for the language's purpose. If type system modelling is inadequate, then programmers are forced to use inappropriate type models. In this case strong typing may be over-restrictive.
Time of Checking
An operation which violates a model provided by a type system may be detected at any time before the operation is executed. In general, it is desirable to detect such errors as early as possible. There are two reasons for this:
- program safety
- program efficiency
If an error is detected before a program starts to execute then the semantics of failure need not be dealt with. It may not be acceptable to terminate the execution when a type error occurs. If the absence of type errors can be guaranteed before execution begins, then no dynamic resource is required to check for possible type errors, with a consequent increase in efficiency.
Languages where all type errors may be detected by static analysis of a program are known as statically typed languages. They have the desirable property that no operation which violates type system modelling can ever occur during execution. Once more, however, such systems must forfeit some flexibility to achieve this. For example, such a system can only allow manifest values to be used as array bounds and subscripts, as otherwise a dynamic error could occur. Most programming languages do rely upon at least some dynamic type checking.
Programming systems which deal with large amounts of heterogeneous data require some dynamic typechecking to allow necessary abstraction over the type of this data. A program which binds dynamically to its data should only have to describe the type of that subset of the data upon which it operates. To allow such partial specification in an evolving universe, an infinite union type is required [ABC+83]. Before a value of such a type may be usefully manipulated, a dynamic type check is necessary.
Persistent Type Systems
Type systems are historically viewed as mechanisms which impose static safety constraints upon a program. Within a persistent environment, however, the type system takes on a wider role.
Data manipulated by a programming language is governed by that language's type system. In non-persistent languages, however, data which persists for longer than the invocation of a program may only be achieved by the use of an operating system interface which is shared by all applications. As a consequence of this, such data passes beyond the jurisdiction of the type system of any one language.
Mechanisms which govern long term data, such as protection and module binding, must be dealt with at the level of this interface. Historically this has the consequence that the type system may not be enforced, and knowledge of the typed structure of data may not be taken advantage of. This is shown diagramatically below:
In a persistent system, the storage of data beyond a single program invocation is handled by programming language mechanisms, and no common operating system interface is necessary. The only route by which data may be accessed is through the programming language, and so the type system of a single language may be used to enforce protection upon both transient and permanent data. High-level modelling may be relied upon for the entire lifetime of the data, as it never passes outside the language system. Such a system is shown below:
The universality of the persistent type system has consequences in terms of both the modelling and protection provided by the type system itself, and also presents some new challenges in terms of implementation.
With respect to modelling, the persistent type system must be sufficiently flexible to allow the modelling of activities normally provided by untyped support systems. Such activities include, for example, the linking of separately prepared program units, and file system access protection. Methods of achieving such flexibility whilst maximising safety include the controlled use of infinite unions, parametric and inclusion polymorphism.
With respect to protection, the increased role of a type system means that any protection mechanisms programmed at a high level may be fully relied upon to protect the data for its lifetime, as access from outside the constraints of the type system is not possible. In particular, various high level information hiding techniques may be used to restrict data access, instead of relying upon the normally coarse grain and typeless control provided by outside technologies.
The implementation of such a system presents the challenges of combining the following features:
- a fine-grained type system to maximise safety, resulting in large and complex type descriptions
- infinite unions, parametric and inclusion polymorphism, to allow sufficient flexibility
- the efficient implementation of the above features in a persistent system
Efficiency is considered important as programmers are well known to sacrifice safety and long-term efficiency for short-term performance. Efficiency considerations within a persistent system are notably different from those in a non-persistent system.
- Source: Types and Polymorphism in Persistent Programming Systems.
- Search for 'types' in School publication list.
- [ABC+83] An Approach to Persistent Programming Atkinson, M.P., Bailey, P.J., Chisholm, K.J., Cockshott, W.P. & Morrison, R., Computer Journal 26, 4 (1983) pp 360-365.
- [CW85] On Understanding Types, Data Abstraction and Polymorphism Cardelli, L. & Wegner, P. ACM Computing Surveys 17, 4 (1985) pp 471-523.
- [KR78] The C programming language Kernighan, B.W. & Ritchie, D.M. Prentice-Hall, New Jersey (1978).