The Java Way, simple Type Inference and Flow Sensitice Typing

In "Groovy static type checker: status update" Cédric gave one of his favorite type checking examples. Even though the example made some things clear that I was not so clear about in my last blog post, I still think we need to look at this example a bit more in detail.

Perfectly fine Groovy code like this:

class A {

        void foo() {}

}

def name = new A()

name.foo()

name = 1

name = '123'

name.toInteger()

is a problem for a static type checker and I want to explain once more in a bit more detail why. There are currently 3 ways to approach this code...

The Way of Java
In this version we try to be as much Java as possible, but obviously we have to give the def a meaning. In standard Groovy this is basically equal to Object. As I wrote in my last blog post, the view on types is in Groovy a tiny bit different compared to Java. Anyway, if def is just an alias for Object and we compile this code with Java's type rules, then the code will not compile:

class A {

        void foo() {}

}

def name = new A()  // name is of type Object

name.foo()          // error: foo() does not exist on Object

name = 1            // assigning Integer to Object typed name is allowed

name = '123'        // assigning String to Object typed name is allowed

name.toInteger()    // error: toInteger() does not exist on Object

While the assignments would all work just fine, the method calls will not pass, since those methods are not available on Object.

Simple Type Inference
This seems to be the way groovypp goes. If I am wrong about it, feel free to correct me. Again we have to give def a meaning and this time we use right hand side of the assignment to do so. For the remaining code we stay more or less with the Java rules. The result is then this:

class A {

        void foo() {}

}

def name = new A()  // name is of type A

name.foo()          // no problem, foo() exists on A

name = 1            // error: assigning Integer to A typed name

name = '123'        // error: assigning String to Object typed name

name.toInteger()    // error: toInteger() does not exist on A

Instead of the two problem from before we have no 3, 2 of them at a different position in our code. If we want that piece of code to compile then those two approaches won't do it.

Flow Sensitive Typing
In this third version we still have to give def a meaning, but this time the meaning is not fixed:

class A {

        void foo() {}

}

def name = new A()  // name is of flow type A

name.foo()          // no problem, foo() exists on A

name = 1            // name becomes of flow type Integer

name = '123'        // name becomes of flow type String

name.toInteger()    // no problem, toInteger() does exist on String

With this we reach our goal - who would have guessed that ;)

The difficult thing for a Java programmer here probably is, that name is not of a fixed type. In fact, looking at many papers in the area of formal semantics, most type systems out there use the flow type only for type checks, not to actually give a variable a type. On the other hand, if you look at the Java way, you could say, that simple type inference is just an enhancement. Instead of letting the user write the type, the compiler will set the type. There are actually many old languages that support that kind of logic. This is really nothing new. Still, if we see that as an enhancement, then saying we let the compiler set the type of a variable automatically at more than one place can be considered as just the next step.

But I am getting side tracked... I only wanted to show why exactly this example is causing a problem or why not. That is all. [UPDATE: I had to reformat the article a bit, because I had problems with my java script based syntax highlighter and with the line length of some code examples]