9
$\begingroup$

In Concepts in Programming Languages, John Mitchell writes that static type checking is necessarily conservative (overly strict) because of the Halting Problem. He gives as an example:

if (complicated-expression-that-could-run-forever)
   then (expression-with-type-error)
   else (expression-with-type-error)

Can someone provide a non-contrived answer that would really be a practical concern?

I understand that Java allows dynamically-checked casts for cases like this:

if (foo instanceof Person) {
    Person p = (Person) foo;
    :
}

but I consider the necessity of that more a Java language/compiler deficiency than a cross-language issue.

$\endgroup$
  • 2
    $\begingroup$ The Java example you gave is a non-contrived example of static type-checking being too conservative. Put another way: the answer depends upon what type system you have in mind. For any example we come up, there will always be a type system that can handle that example (the type system isn't too conservative on that example). For any type system, we can always find an example where it is too conservative. So, I think you need to specify the type system. If the Java type system isn't what you had in mind, is there something more specific you were thinking of? ML-style type inference? $\endgroup$ – D.W. Feb 16 '15 at 21:31
  • $\begingroup$ one might argue that the example is one of static code analysis being "conservative", not nec type checking. it would be helpful to define "conservative". arguably all static type systems will be "conservative" compared to dynamic systems because the former are more strict at compile time by definition. however one might argue neither is more strict at runtime because dynamic checking can return similar (type-based) errors also. and by the way, runtime dynamic checked casts in languages are not a deficiency, they are in most statically checked languages, possibly provably nec. $\endgroup$ – vzn Feb 17 '15 at 16:26
7
$\begingroup$

I've always viewed it more as a matter of convenience, than about whether an algorithm can or can not be expressed at all. If I really wanted to run programs like Mitchell's contrived one, I'd just write the appropriate Turing Machine simulator in my statically typed language.

The trick with a static type system is to offer the right kinds of flexibility just for the cases where the flexibility allows you to write code that is more easily maintainable.

Here's some examples of program structuring techniques that are sometimes thought to be easier to manage in dynamically than statically typed languages.

Generics and Containers

In statically typed languages before ML (c. 1973) and CLU (c. 1974) it was not difficult to create a red-black tree of strings, a red-black tree of integers, a red-black tree of floats, or a red-black tree of elements of specific type Foo. It was, however, difficult (maybe impossible) to create a single implementation of a red-black tree that was both statically checked and which could handle any one of these data types. The ways around the problem were (1) to break out of the type system completely (for example: by using void * in C), (2) to write yourself some kind of macro preprocessor and then write macros that produce the code for each specific type you want or (3) use the Lisp/Smalltalk (and Java) approach of checking the type of the extracted object dynamically.

ML and CLU introduced the notion of, respectively, inferred and explicitly declared (static) parameterized types, which allow you to write generic, statically typed, container types.

Subtype Polymorphism

In statically typed languages before Simula67 (c. 1967) and Hope (c. 1977) it was not possible to both do dynamic dispatch and statically check that you had covered the case for every subtype. Many languages had some form of tagged unions, but it was the responsibility of the programmer to make sure that their case or switch statements, or their jump tables, covered every possible tag.

Languages following the Simula model (C++, Java, C#, Eiffel) provide abstract classes with subclassing where the compiler can check that each subclass has implemented all the methods declared by the parent class. Languages following the Hope model (all the ML variants, from SML/NJ through Haskell) have algebraic subtypes where the compiler can check that every typecase statement covers all the subtypes.

Monkey Patching and Aspect Oriented Programming

Dynamic type systems make a variety of prototyping techniques much easier. In languages where types are represented by hash maps from strings to functions (e.g., Python, Javascript, Ruby) it is quite easy to globally change the behavior of every module that relies on a particular type, simply by dynamically modifying the hash map representing that type.

While there are obvious ways in which monkey patching can be used to make programs harder to maintain, there are also ways in which it can actually be used for "good" rather than "evil". In particular with aspect oriented programming one can use monkey-patching like techniques to do things like modify the file type to point to a virtualized file system, permitting the construction of unit-testing infrastructures for "free", or modify simple exception types so they print log messages every time they are caught for better debuggability.

Unlike Generics and Subtype Polymorphism where the key static checking ideas were available in the 1970s, static checking for aspect oriented programming is (I think) an active research area. I don't know much about it except that there's a language called AspectJ since about 2001.

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.