What was the rationale for being inconsistent in the type notation? Why not be consistent like most languages?

For example, in Java you'd write: int add(int x, int y) { ... }

And in Go you'd write: func add(x int, y int) int { ... }

But it looks like in Hack you'd write: function add(int x, int y): int { ... }

Both Java and Go are consistent, either the type comes before or after the name, no matter which context you're dealing with, be it return type or argument type. Hack seems to mix the two styles, which seems like it would make code harder to read as things get more complex, like when functions accept other functions as arguments.

Am I reading the documentation right? And, if so, can you shed any light on the decision making process that went into this decision?

You are reading the documentation right. I wasn't here when the syntax was codified, but my understanding is the following. For parameter types our hands were tied, since PHP actually already has this syntax for object types (unless we wanted to needlessly break compatibility here). We just extended it with primitive types, generics, etc. For return types, we wanted to preserve the greppability of "function add" in large codebases, both for the actual "grep" tool itself as well as for any other tools like ctags that look for strings like this.

> If all of your code is in strict mode, then we believe the type system to be sound. We haven't done any formal proof of this of course, and there have been plenty of bugs in the past. But that's the goal.

When I look at this from the docs, it seems unsound:

"Hack treats traits as a stand-alone entity during the type checking process. In other words, it ensures type consistency within the trait (i.e., as a black box, so to speak), but does not "copy and paste" the code into all of the classes that use the trait and check for type consistency there. The reason this is done comes down to performance."

Is there something I'm missing that does make this sound?

I'm not sure why you think this is unsound. We check traits in isolation -- we ensure that methods you call are either defined in the trait or declared abstract (and so must be defined in the including class). We also added "trait requirements" to the language, so you can say "the including class must implement this interface" ("require implements IFoo") and we'll know that in the type system too. This means that we can ensure traits are sound even in isolation, and that including classes are sound when they include the traits.

Feel free to play around with the type system in the interactive code editor on http://hacklang.org/.

From playing with the editor, it looks like it is sound.

What I thought the quoted passage was saying was that consistency between a class and a trait used by the class was not checked. That's clearly not the case, though. I don't understand what the performance point is, though, since I don't think the copy-and-paste style would produce different answers.

Finally, the online editor doesn't seem to honor // strict -- it doesn't produce an error when some methods aren't annotated.