Programming Languages Build, Prove, and Compare

The languages of the preceding chapters, Impcore and μScheme, are dynamically typed, which is to say that many faults, such as applying a function to the wrong number of arguments, adding non-numbers, or applying car to a symbol, are not detected until run time. Dynamically typed languages are very flexible, but on any given execution, a fault might surprise you; even a simple mistake like typing cdr when you meant car might not have been detected on previous runs. And using cdr instead of car doesn’t cause a fault right away: cdr simply returns a list in a context where you were expecting an element. But if, for example, you then try to add 1 to the result of applying cdr, that is a checked run-time error: adding 1 to a list instead of a number. To rule out such errors at compile time, without having to run the faulty code, a programming language can use static typing.