Strong Typing

Appeared in Volume 8/2, May 1995

thomasl@arnold.csd.uu.se
Thomas Lindgren
1st December 1994

John Lloyd writes:
maybe some kind soul would be willing to clarify the terminology for us by giving careful definitions of the major concepts (static/dynamic, strong/weak, etc) for type systems with some illustrative examples? Anyway, I do agree that the Goedel type system is static, by any reasonable definition of that term.

Strongly typed: A strongly typed program cannot 'go wrong' (in Milner's words) - that is, dump core, produce a wrong answer or similar stuff. Note that runtime errors are still possible, but are clearly marked as such. (Such as accessing arrays out of the declared bounds, which is seldom statically checked.) (Examples: Lisp, SML, Goedel, Prolog.)

Weakly typed: No such guarantee is given. (Example: C.)

Statically typed: Type checking is done at compile-time. (SML, C, Goedel)

Dynamically typed: Type checking is done at runtime. (Lisp, Prolog)

Someone should probably define polymorphism (esp. parametric versus ad hoc in all its varieties) as well.

I have heard people make the distinction that dynamic typing assigns types to values, while static typing assigns types to variables. I am not sure this is entirely true, but it is a useful approximation for many languages.

andrew@cee.hw.ac.uk
Andrew Dinn
30th November 1994

I just want to point out that the thing which distinguishes the Prolog, Lisp and Smalltalk type systems from those of e.g. C++, Pascal is that the former have typed values but untyped variables, whereas the latter have typed variables and values. I have never seen a definition of 'static' vs 'dynamic' which comes close to making this distinction.

If 'dynamic' is to be of any use then it must be involved with having runtime type testing as happened in e.g. the Interlisp environment where functions contained 'dtype' opcodes to throw an error when invoked with illegal type arguments, or in Smalltalk-80 where objects respond to methods they do not understand by throwing an error. In other words, the type-correctness of program data is validated at runtime not define time. The reason for this is that the presence of untyped variables and indirect linking makes define time checking impossible in all cases.

The construction of types dynamically is a different kettle of (rose-hued) fish, it being perfectly feasible in a typed environment to detect the validity of such constructions either when the types or, rather, routines which use them are defined or when they are executed.

jamie@cs.sfu.ca
Jamie Andrews
30th November 1994

I generally think of a type system as being "stronger" if it has more restrictions on passing a term of one type as a parameter of another type. This may be a wrong/non-standard definition. I'm pretty sure, however, that the concept doesn't have much to do with having to declare all variables.

Thus Prolog and Lisp have very weak type systems C has a fairly weak type system because although you have to declare everything, you are allowed to coerce (or "typecast") anything into anything. ML has a strong type system because you always have to match up formal and actual parameter types exactly, or use specific coercion functions like the one that converts an integer into a real.

andrew@cee.hw.ac.uk
Andrew Dinn
30th November 1994

John Lloyd (jwl@miki.cs.bris.ac.uk) wrote:
Can someone provide some concrete cases where a strong type system in a language such as Goedel gets in the way to a significant degree for this kind of task?

I don't know enough about Goedel to answer the specific question but I do have an example of a 'hard' problem for many strictly typed languages. The problem is to implement a menu handling library where menus are created parameterised by a list of menu entries. A menu entry is a record containing three fields, a string for use as the menu label, a callback routine to handle a menu selection and a callback argument which contains data specific to the particular menu entry. Generally the callback data belong to a heterogeneous collection of types.

In a strictly typed language the type of supplied callback data must be conformant to the type for the data field in the menu entry which requires the latter to be implemented as a union type. But the range of possible types in the union cannot be predefined so the package cannot be implemented as a stand-alone library - it must 'know' about the menu client types.

Ok, I'll come clean. If you have type parameterisation then the menu entry data field can be typed using a type parameter which is instantiated with a union type supplied by the application (a common parent type in a hierarchical type system would do the same trick - i.e. make your heterogeneous types homogeneous). Still this kind of example is a pain in the neck to code because it requires not just adding the union type but also including case checking in the callback routines to ensure that the appropriate union field is received and handled. And this has to be done every time you define a new menu i.e. it happens once per menu rather than once per application (it's a rare case that all (any?) of an application's menus have the same types of entries).

An alternative for OO languages which avoids the case checking is to use a common parent type for the parameterised type and replace the routine stored in the menu entry with a method selector (sort of like what is done in Smalltalk except that the selector must be defined at compile time rather than evaluated at runtime in order to be type safe). This avoids the need for case checking in the callback routines. The menu code sends the message to the stored object and the implementation appropriate to the object is selected by the message dispatching process. To be type safe, this requires not just type parameters but also the ability to check that a parameter type supports the required interface. However, it still implies definition of the common parent type and the implementation of selector methods for each callback data type to be done per menu.

ted@crl.nmsu.edu
Ted Dunning
30th November 1994

Andrew Dinn writes:
The problem is to implement a menu handling library where menus are created parameterised by a list of menu entries.

This is indeed a difficult problem as stated. But if you are allowed to modify the structure a little bit it becomes easy. In particular, if you just define a menu entry as a record containing a string and a closure which accepts no arguments, then you have all the functionality that you wanted and none of the type problems you alluded to. This does presuppose that you have the equivalent of lambda.

The callback/user data arrangement you originally specified was specifically developed as a workaround for the lack of lambda in C, so it isn't so terribly bad to go back to just using lambda.

thomasl@groucho.csd.uu.se
Thomas Lindgren
7th December 1994

Whether specifying the number of solutions to a predicate should be considered a typing problem is debatable; for instance, Goedel would also be weakly typed if that view was taken (since it shares this behavior with Prolog) which I doubt John Lloyd would agree with :-)

Strongly and statically typed functional languages can fail as well, as an example Miranda session shows below. However, in all three cases, the system is aware that failure has occurred and takes the appropriate action (backtracking or exiting with an error message).

Miranda /f car
compiling car.m
checking types in car.m
Miranda car []

program error: missing case in definition of car
(line   2 of "car.m")
Miranda !cat car.m

car (x:xs) = x

Stong typing eliminates one cause of programs failing - namely that a predicate was called with an argument of the wrong type (e.g calling append(f(X), g(Y), Z)).

The kind of failure that results from not providing clauses for all the data constructors of a type is quite different.

A good example of this point is member/2:

member(X, [X|Xs]).
member(X, [Y|Xs]) :-
	member(X, Xs).

When the query: ?- member(a,[]).

fails, it is not because of a type error, it is the desired behaviour. If the query was member(a, f(b)), it would fail, but the failure would be due to the fact that the f/1 functor is not an allowable data constructor for lists.

lee@munta.cs.mu.oz.au
Lee Naish
19th December 1994

This depends on the type system and the intended types for member. For instance, if sub-types/overloading were allowed member(T, non_empty_list(T)) may be a reasonable type for member and member(a,[]) would not be well typed. The type system may even be able to detect that member(a, [b,c,d]) must fail and report an error if this call appears in the program. Alternatively, member(any, any) may be a reasonable type and you could say that the failure of member(a, f(b)) is the desired bevaviour but not a type error.

The point is that the distinction between failures detected by type checker XYZ and other failures is pretty arbitrary. An interesting way of viewing many type checking algorithms is as ways of detecting clauses which cannot be used in well-typed successful derivations. The problem is undecidable in general of course, but there is no reason why we shouldn't try to maximize the number of cases detected.