undefined | Better HN

0 pointsjwatzman12y ago0 comments

Engineer working on Hack here.

It's complicated.

If you use partial mode, which doesn't enforce that every function is fully typed, then it's trivial to break the type system by just using an untyped function. In order to ease conversion, we just assume the programmer knows what they are doing with untyped functions and let anything pass.

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.

Some types are enforced at runtime -- just like PHP5 enforces class type annotations on parameters. However, at least for now, the runtime doesn't do a lot of the clever things with the type system that the static typechecker does. It's much more conservative with using the type information, and doesn't do things like check generics at all. (At least right now! We probably will change this in the future.) This means that we can play a little more fast and loose with the type system in the static parts; we want it to be sound, but it doesn't have to be right now; it's not going to cause a JIT crash or anything.

There are more details on the modes here: http://hacklang.org/manual/en/hack.modes.php

0 comments

5 comments · 2 top-level

samth12y ago· 2 in thread

> 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?

jwatzmanOP12y ago

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/.

samth12y ago

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.

curun1r12y ago· 1 in thread

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?

jwatzmanOP12y ago

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.

j / k navigate · click thread line to collapse

0 comments

5 comments · 2 top-level

samth12y ago· 2 in thread

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

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

jwatzmanOP12y ago

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

samth12y ago

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

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

curun1r12y ago· 1 in thread

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 { ... }

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

jwatzmanOP12y ago

j / k navigate · click thread line to collapse