Strongly Typed Without Loopholes

A language is StronglyTypedWithoutLoopholes if it is either impossible for a type failure to occur at RunTime, or all type failures cause a well-defined error or exception. It is WeaklyTyped if type failures are possible and cause UndefinedBehavior.

This is consistent with the usage at TypingQuadrant, and with the definitions of strongly checked and weakly checked in <http://citeseer.ist.psu.edu/cardelli97type.html>.

An example of a loophole that would cause a language to be StronglyTyped for most purposes, but not StronglyTypedWithoutLoopholes, is the OcamlTypeSafetyProblem.

Quoting from the paper referenced above:

In reality, certain statically checked languages do not ensure safety. That is, their set of forbidden errors does not include all untrapped errors. These languages can be euphemistically called weakly checked (or WeaklyTyped, in the literature) meaning that some unsafe operations are detected statically and some are not detected. Languages in this class vary widely in the extent of their weakness. For example, Pascal is unsafe only when untagged variant types and function parameters are used, whereas C has many unsafe and widely used features, such as pointer arithmetic and casting. It is interesting to notice that the first five of the ten commandments for C programmers [Schmidt, D.A., The structure of typed programming languages. MIT Press. 1994] are directed at compensating for the weak-checking aspects of C. Some of the problems caused by weak checking in C have been alleviated in C++, and even more have been addressed in Java, confirming a trend away from weak checking. ModulaThree supports unsafe features, but only in modules that are explicitly marked as unsafe, and prevents safe modules from importing unsafe interfaces.

Most untyped [i.e. DynamicallyTyped] languages are, by necessity, completely safe (e.g., LISP). Otherwise, programming would be too frustrating in the absence of both CompileTime and run time checks to protect against corruption. Assembly languages belong to the unpleasant category of untyped unsafe languages. So are most dialects of ForthLanguage, but SmugForthWeenies do not consider it to be unpleasant.

One shouldn't mistake DynamicallyTyped for untyped''. Realistically, the moment you add typed runtime input, some sort of runtime type checking is essential to avoid erroneous assumptions -- the input should be type-checked, and rejected by some known mechanism if in error, rather than the program entering an undefined state due to questionable input. To gain the benefit of static typing in a system with inputs and outputs, both typed files and typed message transmissions are necessary.

Without loopholes? What about collections, such as arrays, that can hold multiple types? Either you hard-wire the types allowed up-front, limiting run-time flexibility, or you have to do some type-checking at run-time. There is a topic about that somewhere around here. --top

You may limit runtime type checking through use of proper structures. The most common and easiest to understand are TypeValuePairs? <T,v>, constrained by type-compatible(v,T). This is mostly seen with RTTI and reflection, where all objects are forced to become something like TypeValuePairs? by including a pointer back to the 'Class' object. TypeValuePairs? can be specialized by further constraining T and/or v. An array of TypeValuePairs?, then, requires no run-time typechecking regarding either the value or the type because all uses of the TVPair may be fully typechecked. Decisions, however, must be made based on the type and value... but performing such decisions isn't, strictly, type checking.

Sounds almost like emulation of dynamicly-typed variables. Isn't that a "loophole"? --top

No. It is still strongly and statically typed. It would be a loophole only if the static type-safety system did not enforce the type compatibility constraint. By enforcement of this constraint, you gain static type safety because, for every component of the collection you operate upon, you can guarantee at compile-time that the operation is of the correct type; you can guarantee that operations on 'T' are operations over type-descriptors, and guarantee that functions that operate on values of type T will be safe on v. E.g. if you have function f :: Type'S -> S -> R (type-descriptor named S to a function of value-S (a type) to R), you can guarantee that 'f T v' with (T,v) from the type-value pair will be of type R. If R is a procedure type, you can then execute the result.

Essentially, the static type-safety ensures that the dispatching mechanism is entirely type-safe and that the type-value pairs are constructed legally. No dynamic type-checking is required... or even utilized, really, because nothing in the runtime is checking types automatically. However, the behavior of the system as a whole results in a dynamic, runtime computation dispatch based on the 'type' in the type-value pair. This 'type' will often vary dynamically... it might not even be a type that had ever been described before compile-time. One could say this emulates dynamic, runtime dispatch... but I'd counter that this is the real thing, just provided explicitly, and slightly more flexible in that one can make it fully generic. Type dispatch is not the same thing as type-checking. There is no runtime check to ensure that value 'v' is really of type 'T'; that can easily (*cough*) be ensured at compile-time... given a constraints-enhanced typing system.

You would, however, still need runtime typechecking on communications. E.g. for accepting (T,v) pairs off a communications link. In general, you need to runtime-typecheck inputs off communications links unless you can trust them to be error-free, at which point you can optimize the typecheck away (as you would do for intra-process communications, and some inter-process comms). You also need no runtime type-check if there are no unused representations (e.g. Int32, or Byte).