Soft Typing

A type system based on two key ideas:

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

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

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++.

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 The main difference is that it will go one step further and reject programs that are provably wrong.

"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....

View edit of March 28, 2006 or FindPage with title or text search