Soft Typing

A type system based on two key ideas:

accepting the usefulness of static type checking
accepting that the set of statically typed useful programs is smaller than the set of programs containing typing errors
- more specifically; the set of useful programs for which an ideal typing can be statically determined (either by the programmer, or by TypeInference) is smaller than the set of programs which contain no typing errors. See CompileTimeTypingProblem for a definition of "ideal typing".

This leads to a sort of optional type system. Where the type checker can prove that the program is type safe, all is fine and dandy. Where the type checker can't prove correctness it informs the programmer and inserts appropriate type checks, but doesn't reject the program. DrScheme has such a system, called MrSpidey. SoftTyping is also used by EeLanguage and SlateLanguage.

See also the paper "Soft Typing" by Cartwright and Fagan, available from http://www.cs.rice.edu/CS/PLT/Publications/Scheme/

IntentionalProgramming seems as though it could be usefully combined with SoftTyping, since type annotations generated by the type checker/inferencer (or more generally, annotations to support various kinds of static analysis) can be stored in the tree-based program representation and viewed at whatever level of detail is desired. See http://www.aisto.com/roeder/paper/.

How does this differ from c++ with casts?

Perhaps C with lint did something along these lines? (One is free to ignore lint's warnings, or just refrain from using it.)

It differs from C++ with casts because you need way fewer type declarations. You declare the things you think you need to declare. The system does TypeInference. Anywhere where it can't prove that all values have the expected types, it inserts run-time type checks that will complain if they turn out not to. This is all dependent on having a system that can cope with types being unknown at run time. It's very different from C++.

C++ doesn't insert typechecks unless you, the programmer, tell it to (via DynamicCast and similar). Old, C-style typecasts (and ReinterpretCast?) do not do typechecks; and can lead to uncaught typine errors.

OK, how does this differ from Johnson's TypedSmalltalk?

It doesn't. TypedSmalltalk uses SoftTyping (although its emphasis was on optimization, rather than reporting potential type errors).

An extension to SoftTyping is CompleteTypeInference?/CompleteTypeChecking? (see http://citeseer.nj.nec.com/widera01sketch.html). The main difference is that it will go one step further and reject programs that are provably wrong.

...with respect to typing. Remember that type checks for correctness is both an overapproximation and an underapproximation (there are incorrect programs that are accepted by the typechecker as well as correct programs rejected by the type checker).

"accepting that the set of statically typed useful programs is smaller than the set of programs containing typing errors "

In practice, this is not true. Every type system that is being used in a practical language, does have some way to subvert the checker at the risk of a run-time type error. C, C++, and Java have casts. ML has case statements that leave out cases. (Any challengers to this?) Without such a feature, the system would simply be too frustrating to use. Imagine trying to get anywhere in Java without the ability to insert an occasional cast!

Yes, people do occasionally prove that this or that type system does not allow type errors at runtime. However, to do this, they must use a technical definition of "type error". For example, they leave out casts that turn out to fail. The type system is still useful, but let us not overstate what they do. For a software engineer, a failing cast is just as bad of a type error as if there were no type checker at all. Redefining "type error" very carefully does nothing to help these real problems; it just makes the theorem prettier.

It seems that the Soft Typing people, however, are unusual in really running with this observation....

CategoryLanguageTyping