julienv's comments

The SQL database that tells you when your query results changed

Well, imagine your type-system was able to tell you exactly what roots are mutable in what scope. Now you can run a garbage collection on a single scope. That's not how it works, but in pseudo code:

collect { // Some code return ...; }

Well, if you don't have a type-system that tells you what is mutable, you have to either scan all the mutable roots, or maintain a write-barrier to know what could have captured data in the scope.

The problem with write-barriers, which is the go-to solution for generational GCs. Is that it is a conservative approach. Meaning, it will promote garbage in the cases where the pointer that lived outside of the scope is dead.

Let's take an example, again, in pseudo code:

myObject = { field1: []};

collect { myObject.field1 = [A, B, C]; myObject = null; }

If you use a write-barrier, what is going to happen is that [A, B, C] is going to be promoted, because the barrier is going to track the object myObject, and it doesn't realize that it's dead.

However, instead, imagine you have a type-system that tells you that in that scope, the only thing that can be mutated is myObject!

Well, now you can run that in a loop, without accumulating garbage!

Makes sense?

Thanks! You can try the version in the site for testing if you want! If you want to build something, let us know!

That's what SQLive is written in. Hence the name SkipLabs!

Fixed! thanks!

It's still very much used at SkipLabs. In fact, it's the language that SQLive is written in: http://sqlive.io

Unfortunately, we use a proprietary fork of SKIP, so that's why the OSS project looks dead.

We might open-source our version some day, but no plans for now.

There seem to be 2 questions here: 1) Is Hack type inference total? Answer no: you must annotate parameters and return types.

It would be pretty much impossible to implement total type-inference without loosing separate compilation in Hack. PHP projects are not organized around a module system, which means that you have "spaghetti" dependencies, and even better, cyclic dependencies all over the place.

So trying to implement total type-inference would be a bad idea, you would not be able to separate the code in independent entities and the checker would not scale.

2) Does Hack support structural sub-typing? Answer: No, but not for obvious reasons.

Fun fact, the first version of the type-checker was implementing structural sub-typing. And it was not scaling, for subtle reasons.

Hack allows covariant return types, so if we implemented structural sub-typing we would have to "dive" into the return types of each method to see if they are compatible. But in turn, these objects could have covariant return types etc ... The process of checking that was too inefficient. Caching is a bad idea (or at least a non trivial idea to implement), because of constraints and type-variables.

Since disallowing covariant return types was not an option (it was crucial to make a lot of code work), we had to kill structural sub-typing.

I hope this answers your question. As a big OCaml fan myself, I like the features you just mentioned (Well, Hack is written in OCaml), but they really didn't seem to be a good fit due to the nature of the language and the kind of checking speed we were shooting for.

Yes and no. Yes, because TypeScript is bringing a type-system to a dynamically typed language and so did Hack. No: because Hack is bringing some additional language features affecting the runtime. Modest changes for now, but we intend to carry on in that direction.