Three Kinds of Typed Languages

There are a lot of questions on stackoverflow about difference between static and dynamic typing, e.g. why is Smalltalk considered dynamically typed. Here is my very own perception on the subject.

Background: Type systems are conservative static analysis

Here is the definition of a type system from Types and Programming Languages:

A type system is a tractable syntactic method for proving the absence of certain program behaviors by classifying phrases according to the kinds of values they compute.

The “kind of values they compute” is usually referred as a “type”. What the type system usually proves is that the program will not be “stuck”. Thinking of the semantics of the programming language as a set of evaluation rules, it means the evaluation of the program will terminate.

int x = 0;
if (false) {
   x = "hello";
} else {
   x = 1;
}

The above program will actually always terminate, since the true-branch will never be executed. However, it would fail to type-check, since the type system rejects x=”hello”. Reaching this statement would stuck the evaluation, since there is no consistent evaluation rules for it (unless the semantics define coercion rules). Type checking is a conservative analysis.

Run-time checks

For very simple language, evaluation rules do not perform run-time checks, and type checking usually means that the program terminates without run-time error. For any realistic program, there will be run-time checks for certain evaluation rules.

int x = 10;
int y = 0;
return x / y

One of the simple evaluation rules that requires a run-time check is integer division. Dividing by zero is not possible. If this situation occurs, a run-time error occurs. Run-time errors can either lead to the abrupt termination of the program, or the semantics can define error handling. Null pointers are other typical run-time checks.

Run-time type tags

Certain languages do not need run-time type tags to distinguish different kinds of structure in the heap. Evaluation rules depend on the static type solely, and the heap is flat array of unstructured data. (Lambda calculs with record and references, and C-like languages fall in this category, I guess.)

However, in many languages, run-time type tags are needed to distinguish different kinds of structures in the heap. Run-time type tags are requires to implement polymorphic behavior. In object-oriented language, this corresponds to interface and subclasses. The specific type of an object might be unknown, but it conforms to a type that is known statically.

Run-time type checks

Evaluation rules in such language perfrom run-time type checks. The check is necessary to “dynamically dispatch” the operation accordingly to the run-time type. Type systems can prove that the run-time type check will never fail, that is, the operation can always be dispatched, and the execution will not be stuck.

Three kinds of languages

The evaluation rules of the programming language, which define its semantics, can use static types and/or run-time types.

1. Run-time type only — Let us consider Smalltalk. Smalltalk’s core semantics is entirely defined by the dynamic types: When you send a message to an object what must be executed depends on the dynamic types of the receiver. If a message can not be dispatched, the program is stuck. In practice, the error is reified into message not understood exception.
   The semantics of the language does not need a type system/type checking. You can however type check the code to guarantee that there will be no such run-time type error, see Strongtalk. With type inferrence, only minimal static types will be needed.  This is the approach that pluggable types promotes. The type system is optional.
2. Static type only — A language with object, but without subtyping nor inteface. Such a language would not need type information at run-time. The heap is flat array of data whose type/structure can not be discovered at run-time. With proper information in the code about the expected type of objects, you can still define a valid semantics for the language: when you send a message to an object you know what must be executed since the type in statically known in the code. By definition such a language could not have dynamic dispatch and inheritance polymorphism. (The typed lambda calculus without subtyping is maybe of this kind).
3. Static and run-time types — Let’s consider Java. It mixes both static and run-time types. Objects have dynamic types for dynamic dispatch and polymorphism. However,the exact semantics of the language rely also on static types. For instance, method overloading in Java depends on the static types of the paramters. A class can define methods print( A a ) and print( B b ). The semantics of anObject.print( anotherObject ) depends on the static type of anotherObject: when you send a message to an object, you define what must be executed depending on the dynamic type of the receiver, and the static types of the parameters. 
   

Note that by “static type”, I don’t mean the type is explicitely in the source. The static type is the result of a static analysis, and can be inferred. Inferred types can be the union of explicit types. The static types can be though of a “parametrization” of the evaluation rules.

function printHello( object ) {
     object.hello();
}
function printHelloA() {
     A a = new A();
     printHello( a );
}
function printHelloB()  {
     B b = new B();
     printHello( b );
}

Even if A and B are distinct types (not implement an interface or so), a type system can still figure out that printHello in passed either A or B and that both implement hello().

A language with first-class function can implement dynamic dispatch even without interface nor subclassing. Indeed, an object can store function that a client can access to emuate polymorphism. Functions have a type and are polymorphic by nature.

• What to know before debating type systems