Excessive explanation, part three
Continuing with my excessive explanation of type inference in ML"
Here we answer the question in the affirmative, for the purely applicative part of ML. It follows immediately that it is decidable whether a program is well-typed, in contrast with the elegant and slightly more permissive type discipline of Coppo. [1]
The "applicative" part of a language is the part of a language concerned with the question "what happens when we call a function with some bunch of arguments?" That is, the function is said to be "applied" to its arguments. (Or is the argument applied to the function? It's a mystery.)
What we're getting at here is: there's a lot of stuff in real-world ML that we're not going to worry about here: data structures and integer literals and pattern matching and all that stuff. The applicative part of the language is its core, and if we can make a sound, general type assignment algorithm for this core of the language, then that's the interesting part; the rest is just filling in the corners, in some sense.
By "in the affirmative", we mean that the paper will show two things. First, that the type assignment algorithm really does always find a type assignment if one exists, and produces an error if it does not. It never goes into infinite loops or returns the wrong answer. And second, that if an answer is produced, it is the most general type possible.
By "decidable" we mean that it is possible to write a computer program that takes as its input a syntactically well-formed ML program and always produces as its output either true: the program does not violate the type system, or false, the program does violate the type system. It never hangs, and it never produces the wrong answer. A program that takes some string and produces a Boolean like this is called a "decision algorithm", and a problem for which a decision algorithm exists is a "decidable problem".
Not all problems are decidable! The canonical example is the Halting Problem, which is "given a well-formed program, can this program go into an infinite loop?" We know that it is impossible to write a computer program that always answers this question correctly; either such a program is sometimes incorrect, or it sometimes goes into an infinite loop itself.
Note that not all type systems are decidable, and in fact, it was recently proven that the C# type system is not decidable! It is possible to write a C# program where the type checker will either get it wrong or run forever, though it is a pretty weird program. I'll talk about that in a later blog series. (I had a very, very, VERY small part in this recent proof which is quite hilarious.)
The paper of Coppo mentioned notes that the ML type system does not allow you to represent some functions. For example, the function "take a function as the argument, pass the function to itself, and return the result" does not have a type in the ML type system.
Now, you might think, hey, we can represent that in C#:
delegate D D(D d);...D weird = d => d(d);
Though that is a function that takes a function as the argument, passes it to itself, and returns the result, notice that this is not general! There's nothing generic here. Coppo points out that there are lots of different types of functions that match the pattern of "it's legal to pass the function to itself", and that there is no way to express that pattern in the ML type system.
In the paper, Coppo presents an extension to the ML type system that allows that, but the authors here point out that Coppo's type system has the down side that it is not actually decidable.
This happens a lot in type systems; you often trade ability to represent a particular kind of odd function in the system for undecidability in extremely weird cases.
Next time, a not-weird case: how can we analyze the type of "map"?
