Hummus and Magnets

Esmertec sent out an innocent-looking press release today: Jean-Claude Martinez Confirmed as CEO of Esmertec. But there’s a bit more to it than the title suggests:

Cost reductions: Management has decided to close down Esmertec’s subsidiary in Denmark and reduce significantly the operations in Japan. The company has assigned resources from other Esmertec’s offices and in Japan to continue supporting the products and customers in these regions.

What that means is that I now have a really long summer vacation. It also means that you shouldn’t expect an open source version of neptune to be released any time soon — in fact, don’t expect any version to be released at all.

Why has this happened? This press release gives a hint.

When I wrote the first post about types in neptune I ran out of steam before I was completely finished. In this post I’ll finish by describing two features I only mentioned briefly in the first post, the void type and protocol literals.

Checks

But first: as Isaac points out, I’ve spent a lot of time explaining what the type system doesn’t do and doesn’t require, and very little explaining what it actually does do for you. I guess I didn’t think to write about it because the checks that are performed are pretty simple and conventional. Here’s a summary of the checks performed by the compiler.

• If you call a method m and the type system knows that the receiver has a type that doesn’t define the method m, the checker will issue a warning:

  protocol Runnable {
    run();
  }
  
  Runnable action = ...;
  action.runn(); // warning: undefined method Runnable.runn()

• If the type checker knows the signature of a method and you pass it an argument with an incompatible type, a warning will be issued:

  int gcd(int a, int b) { ... }
  gcd("foo", "bar"); // warning: incompatible types

  I’ll return to what “incompatible” means in a second.

• If a value is assigned to a variable of type T, a warning is issued if the type of that value is not a subtype of T:

  int x = "4"; // warning: incompatible assignment

• When returning a value from a method with return type T, the returned value must be a subtype of T.

  int foo() {
    return "bar"; // warning: incompatible return type
  }

  As a special case of this rule which I’ll return to later, returning a value from a void method is illegal, and not returning a value from a non-void method is illegal.

• Finally, the compiler checks that methods override each other properly. An overriding method is allowed to return a subtype of the overridden method (return type covariance) and it is allowed to take arguments that are supertypes of the arguments of the overridden method (argument contravariance):

  class SuperClass {
    Object foo(int x) { ... }
  }
  
  class SubClass: SuperClass {
    Object foo(String x) { ... } // incompatible override
    int foo(Object x) { ... } // legal
  }

There may be more checks that I’ve forgotten but at least these are the most important ones. All but one of these checks use the subtype relation between two types which is simple in neptune: The type X is a subtype of Y they are equal, if Y is a class that extends X, directly or indirectly, or if Y implements the protocol of X, again directly or indirectly. It’s a simple version of the nominal typing relation of many other object-oriented languages, including Java and C#, except that it is more general because one class can be a subtype another class without having that class as a superclass.

Besides these checks, the compiler also issues warnings if it thinks a class has not been properly implemented: if non-abstract classes have abstract methods, if a class doesn’t provide all the methods required by the traits it uses, if it declares that a method overrides another but it doesn’t, etc. However, all those things could be checked even if there was no static type system.

I hope that clarifies what the type system will do for you, and then move on to describing the two last features of the type system.

Void

In most languages, methods that don’t return a meaningful value are treated differently than other methods. In the C language family, such functions and methods are declared as if they did return a value of type void, but the void type is special and magical; what it really means is that the function don’t return a value at all. In particular, there is no value of type void and you can’t declare a variable of that type:

void do_nothing() { }

void my_void = do_nothing(); // illegal

Void methods and functions in the C languages are fundamentally different from functions and methods that return values and the type system keeps track of whether or not you’re allowed to use the result of a call. In neptune we can’t do that because you are free to call a method even if the type system knows nothing whatsoever about it. So we couldn’t use the C model, at least not directly.

In smalltalk, on the other hand, there is no such thing as a method that doesn’t return a value. You are free to not explicitly return a value from a method, but in that case the method returns self. I don’t consider that to be a particularly good design and long before we considered switching from smalltalk to another language we experimented with changing this in OSVM. The problem is that many methods really aren’t intended to return a meaningful value but return self by default. Then someone accidentally uses this value and then later when the method is changed, under the assumption that no one is using the return value, the program breaks somewhere completely unexpected. The problem is that the intention of the method isn’t clear because sometimes methods really do intend to return self but you can’t tell if this is the case since the return isn’t written explicitly. Personally, I used the convention that if I wanted a method to return a value I would always explicitly return it, even self. If I didn’t want the method to return a meaningful value, I would return nil.

In neptune, we wanted a combo solution: all methods should return a value but we also wanted to avoid the problems from smalltalk and we wanted the code to look like C. The solution was to make void into a real type and introduce a void value. All methods that don’t explicitly return a value automatically return the void value, and a return statement without an explicit value also returns the void value. The void value itself is a full, real object just like null:

void get_void_value() {
  return;
}

var void_value = get_void_value();
System.out.println(void_value.to_string()); // prints "void"

This model gives you almost the same behavior as C, Java and co. but for different reasons. If you declare that a method returns void the type system will warn you if you return a value of another type, since the returned value is not a subtype of void. If a method is declared to return something other than void but don’t return a value, the type check fails because a method that doesn’t explicitly return is made to return the void value which is not a subtype of the return type. Finally, if the void value ever turns up as the value of a variable or somewhere else where you don’t expect it you’ll know that there is a problem.

This model does give a little more flexibility, some of it is probably useless (but you never know) and some of it is slightly useful. First of all, since void is a regular type you can declare variables of type void. I don’t know why you would do that but you can. Secondly, it is legal to explicitly return a value from a void method if that value is the void value. That might not sound useful but it can be since it means that you can call another method and return in the same statement:

void add(var obj) {
  if (delegate) return target.add(obj);
  ...
}

In java, you can’t call a void method and return in the same statement so you would have to write

void add(Object obj) {
  if (delegate) {
    target.add(obj);
    return;
  }
  ...
}

It’s a small thing but it does give greater uniformity. By the way, I believe you can actually do the same thing in C++.

Of course, having a dynamic representation of the “nothing” value is not a new thing, many languages have that. My experience with it, at least in the context of this kind of language, is that it works very well in practice and better than any of the alternatives I’ve tried.

Protocol literals

The last thing is sort of an oddball. Sometimes it can be practical to represent a type as a run-time value. For instance, in our unit test framework we have a method that asserts that running a particular piece of code throws a particular exception

assert_throws(IOException.protocol, fun -> file.open());

The expression IOException.protocol gives you an object that represents the protocol IOException. A protocol object can be used for exactly one thing: to test whether other objects implement the protocol it represents:

Protocol p = String.protocol;
var x = "Beige";
if (p.is_supported_by(x)) ...

That may not sound very exciting but it can be useful in combination with other abstractions that are built on protocol objects, for instance exception handling. In a post a long time ago I mentioned that in neptune, an exception handler such as this:

try {
  ...
} catch (e: IOException) {
  ...
}

is expanded into this:

fun {
  ...
}.try_catch(
  new Vector { IOException.protocol }, 
  fun (Exception e) {
    ...
  }
)

Exception handling is based on the try_catch method which uses a list of protocol literals to decide whether or not it catches a particular exception. The fact that you can call this method directly means that you can make exception handlers that are not statically bound to a particular exception type but where it can be determined dynamically which exceptions to catch. This is how assert_throws is implemented:

void assert_throws(Protocol type, fun f) {
  fun {
    f();
    fail_not_thrown(type);
  }.try_catch(new Vector { type }, fun {
    // Ignore exceptions of the right type
  });
}

It’s not something you use often but on those rare occasions where you do use it it’s really handy.

The last big thing in neptune that I haven’t written about is the static type system. We’re not actually 100% done with it yet — the design is mostly done but there is still a few late additions that we seem to agree are good ideas but that we haven’t implemented yet. I think we’re far enough, though, that I can give a pretty accurate overview.

The way the type system in neptune came about is kind of unusual. Neptune descends from smalltalk which is not statically typed, but an important goal in the design of the language was to make it look familiar to C and C++ programmers. If you look at these two versions of the same program:

int gcd(int a, int b) {
  while (a != 0) {
    int c = a;
    a = b % a;
    b = c;
  }
  return b;
}

and

gcd(a, b) {
  while (a != 0) {
    var c = a;
    a = b % a;
    b = c;
  }
  return b;
}

the first program looks just like C (because that’s what it is) and the second one looks sort of C-ish but also pretty different. The only difference between the two programs is, of course, that one has type annotations and the other one doesn’t. When we set out to design neptune there was really no question: if we wanted it to look like C, we had to have a static type system. That is not to say that this was the only reason to have a static type system, there are plenty of very good reasons for that, but it is the reason why not having a type system was never an option. Besides the syntax, the most important reasons were that it allows you to write documentation that can be understood and checked by the compiler which again enables much better tool support. The most important non-reasons were optimization security — they were basically irrelevant in the design.

So, what’s the neptune type system like? Well, first of all it’s an optional type system. This means that you are never required to specify a type for anything. For instance, the two gcd programs above are both legal neptune code¹. Basically, we want the type system to be there as a service that you can use if you want to but which doesn’t impose itself on you. From a “genealogical” viewpoint, it is closely related to the Strongtalk type system for smalltalk.

The examples above demonstrate the type syntax. If you use type annotations the syntax is the same as in the C language family. If you don’t use type annotations you either just leave the type out, as with return types and parameters, or use the keyword var, as with local variables. In some cases, for instance method parameters, you can do both.

The type system is based on the concept of protocols, which is smalltalk for what most people know as “interfaces”. A protocol is simply a collection of methods:

protocol SimpleOutputStream {
  void write(int b);
  void flush();
  void close();
}

Unlike most statically typed object-oriented languages, including Java and C#, neptune does not have class types. Class types are a Bad Thing because they not only specify the interface of an object but also dictate how the object must be implemented, breaking encapsulation.

There are two ways to define a protocol. One way is to write it directly, as the SimpleOutputStream example above. Also, whenever you define a class you automatically get a protocol with the same name. That might sound confusing but in practice it isn’t. Protocols work much the same way as interfaces, and protocols defined explicitly work exactly the same way as protocols defined by classes. For instance, you are free to the protocol of a class without subclassing it:

class MyString is String {
  ...
}

In this declaration, “is String” means that MyString implements the protocol of String, not that it extends String — the superclass of MyString is in this case Object. To create a subclass of String you would write

class MyString: String {
  ...
}

A class can extend one other class but implement an arbitrary number of protocols.

If you use String as the type of a variable it’s usually safe to think of it as if the variable can contain instances of String. But that’s is not accurate in general: the variable can actually contain any object that implements String‘s protocol. Neptune has no way to express that a variable can only contain instances of a particular class.

Programs can dynamically test whether or not an object supports a particular protocol by using the is operator:

if (obj is String) ...

One of the things we haven’t implemented yet but seem to agree is a good idea is to combine this with a limited form of dependent types. In most other languages, for instance Java, the compiler doesn’t “remember” instanceof checks:

if (obj instanceof String) {
  label.setText(obj); // illegal: obj not String
}

The compiler doesn’t recognize that you only enter the body of the if if obj is a String — instead, you have to insert a cast:

if (obj instanceof String) {
  String str = (String) obj;
  label.setText(str);
}

In neptune, we plan to allow the compiler to automatically remember extra type information about local variables after is checks, something that will in many cases make casts unnecessary:

if (obj is String) {
  label.setText(obj); // okay, obj is a String
}

In a language like Java that might make programs harder to understand, since the runtime behavior of the program can be affected if the compiler gains more type information. In neptune all it does is avoid unnecessary type warnings, since the runtime behavior of a program is not affected by static types.

This leads me to another aspect: type warnings. In neptune, all problems detected by the type checker are reported as warnings, not errors. It doesn’t matter how wrong you get the types, the program will still compile and run. Well, except for one case: you can’t mix function objects (blocks) and other objects, you have to get the types right there. That is because the compiler needs to be able to track that no references exist to a block after the method that created it returns — otherwise the runtime will die horribly. The philosophy of when to give warnings and errors is simple: we only give errors in a program if we can’t give meaning to the program, otherwise we give warnings. You won’t, for instance, see errors on unreachable code or other such nonsense. You can configure the IDE to give errors instead of warnings but that’s not the default.

Neptune’s static type system is “weak”. Even if x has type int there is no guarantee that it can only contain integers:

var my_string = "blah";
int x = my_string;
int y = x + 18;

In the second line an object of an unknown type is assigned to an integer-typed variable. That is perfectly legal and does not cause a warning so this code will compile without issuing any errors or warnings but will probably fail at runtime in the third line when adding an integer to a string. That doesn’t mean that you can use this to break the runtime. The runtime is strongly typed so no matter how wrong you get the static types it will survive. You might ask why we don’t add runtime checks to catch these situations but that is potentially expensive and it’s probably not worth the trouble. We could also add warnings if we’re not sure that an assignment is safe, but that would generate warnings whenever untyped code called typed code, which goes against the principle that the type system should never impose itself on you if you decide not to use it. Personally, this has never been a problem for me, not even once.

The other thing we’ve discussed and seem to agree upon but haven’t implemented yet are nullable types. By default all types contain the null value:

String str = null; // legal

But often a value is not actually supposed to be null. Nullable types allow you to express this:

String! str = null; // illegal
String? str = null; // legal
String  str = null; // legal

The type String! does not allow null whereas String? does. The type String also allows null but is different from String? in that Strings are completely unchecked whereas using a String? in place of a String! without a null check causes a warning.

Ok, I think that’s enough about types for now. There are still interesting details about the type system that I haven’t written about — protocol objects, the void type, etc. — but that will have to wait.

¹In case you were wondering, int is not a basic type in neptune — neptune has no basic types. It is just a convenient shorthand for the type Integer.