Compilers should write types for programmers, not the other way around

Note: I’m not an expert in type systems, and my knowledge of compilers is limited. This is more of an actual random thought I had for some time, and I’ve just decided to capture it here, not to be used as an argument on static vs dynamic types. Plus, I wanted to try out ChatGPT and it was a nice opportunity.

With the advent of ChatGPT and a lot of noise around the web about how it understands code, I’ve thought about one of the topics, that is always hot in programming - type-systems. There are a lot of type systems around, that provide different capabilities, and while I can see how it can be interesting to do research on type systems, I absolutely fail to see how it can be interesting to use types in practice.

I’ve been a Clojure programmer for the past two years, and prior to that, I’ve been using C, C++, and Rust to some extent. I’ve liked types in Rust, and seen it as a major step from what C offered, and it was definitively better than C++ in my opinion too. In addition to that, I had looked at other languages, which have interesting type systems, and during that period of time, I had despised languages that were dynamically typed. However, instead of Rust I chose Clojure as my main language for work, and the main reason is that after actually trying it I’ve realized that instead of thinking about types, I can think about writing programs.

Well, this does sound rough, but what I mean is that by the time I’ve thought up all program’s layout in Rust, having all the types in place, I would already finish that program in Clojure. And after trying a language that doesn’t require you to define types, I started questioning the conception that type systems are great for rapid prototyping. Because types make program development more rigid, you have to think up types upfront, or you’ll have to do refactoring. You know, some languages treat a hash-map as a special case of an object, and others treat objects as a special case of a hash-map. And both are valid ways to look at it, I think.

Yes, you can often derive types from the requirements, and use TDD in combination with your language’s type system, making your program robust, but that’s what I’m talking about when I mean that you have to think things upfront. For instance, when I was writing my implementation of the scheme-like language, I had to rethink types a lot of times, instead of focusing on the actual implementation. This, in reality, shows that more often than not, I wasn’t sure what I’m doing, and what’s my end goal actually is, but I think there are often times like that when working on some real projects as well. And Clojure’s dynamic typing and REPL-driven development provide programmers with a much less friction system for rapid prototyping, especially because you don’t really think about types, but about your data flow. Yes, there are purely computational problems, which don’t involve data processing in the general sense, but more often than not we’re manipulating data, and there are not a lot of situations where typing that data really makes sense. Validation still happens at runtime, so in my view using constructors as validators to ensure that the program compiles and data is then parsed and formatted correctly is pretty much the same as just writing a validator for your data. Well, it’s another topic for another day, I guess.

Note that I’m not saying that types are not needed entirely, though. Typed languages have one great advantage, compared with dynamically typed languages, they often generate more optimal machine code. With all that type information available, a sufficiently sophisticated compiler can generate optimal code, so this is a clear benefit. Still, there are purely dynamic languages that generate a quite optimal machine code with their implementations of JIT, so it’s not like it is impossible, it’s just easier to do with known types. And type deduction is a thing that had existed for quite a long time, so a lot of languages today use compile-time type inference allowing programmers to skip type annotations in cases where the compiler can do it for you. And where it can’t, languages often provide facilities for plugging types in.

And that’s what I think any compiler should do - it should generate types based on your code, minimizing the times it wants a programmer to give it a hint. Type deduction is a hard task, and there are a lot of algorithms to solve this problem, but there are situations where it may be hard to do inference. In such cases, it is possible to use the broadest type, which comes at a cost of generation of an unoptimal code or use the runtime which may be slow.

And the rise of neural networks probably can help here. E.g. instead of generating a believable text, I imagine that a neural network can be taught to do code analysis similarly to how humans do it and generate types, again similarly to how humans do it. Speaking about ChatGPT, I’ve tried to ask it to deduce types based on the code I gave it. And it managed to do so with some guidance.

The examples weren’t too intense, but I’m still impressed with how it was able to deduce types and notice various errors. First, I’ve asked it to fill in types for a fairly simple case, just so it could understand my intention:

Next, I’ve moved to compound types:

And to types that inherit methods from other types:

I’ve actually made a typo in that code, defining a method with a name move_to, but using the move instead. This was unintentional, but ChatGPT caught that mistake, so I’ve asked to report such errors in a style of a real compiler:

The type notation is not as precise, as I thought, but from such a message, I could understand that the method is missing, and probably would be able to understand what the issue is. So I fixed the code and sent it back:

However, even though I’ve used the move_to method, it is not included in the generated type, so I asked ChatGPT to include information about inherited types, using an arrow notation:

And here they are, now function has a type that conforms to base types of Dog and Movable. So I’ve decided to try creating functions that expect certain traits to be implemented on a type, and pass it to a type that doesn’t have them, to see if ChatGPT would catch the error:

Even though it did not include Dog in the inherited type for the function foo it’s impressive that it managed to detect a compile error that bar can’t take the object generated by the make_entity function, because types don’t match. Pointing out the error, however, helped ChatGPT to fix the mistake, and it actually explained that the reason for inclusion is the type of make_entity:

I’ve also decided to try it with a language that doesn’t have a static type system, so I chose Lua, as it is a language I know:

It was a pretty simple case, though it’s interesting that it knows about gsub being a string method. Then I’ve asked it to work with tables:

Technically, this is correct, but I’d like to have a more specific type information (not that it matters in this code, though):

This is more interesting, and it actually printed the result of the evaluation which appears to be correct. This function doesn’t do much, but it’s nice to see that ChatGPT understands the code, and can do a more deep analysis, based on the data structures used.

Overall, I think it is an interesting field for neural networks because teaching them to understand a particular language with a well-defined type system can lead to a more robust type deduction, based on user code. I’m not sure, however, how much computation power such a neural network would require, but given that it will have a more narrow scope, I would guess that it won’t require that much. Or maybe such networks can be paired with other type deduction systems, and only used when conventional algorithms unable to deduce a type.

As I’ve said this is a hard task, that is yet to be done right, and I think that in the upcoming ~30 years we will see a language that will combine the ease of use of a dynamically typed language with strict checking and optimization opportunities of a statically typed language.