Hi Bryan, I know most people know you from your prolific work on many great Haskell libraries ( Criterion, Attoparsec, Aeson, ...). Did Haskell have any role in the development of Hack? Looking at the code base it seems like the type system is primarily written in ML, what made the team decide to use OCaml over Haskell?
As you note, the team developed the typechecker in OCaml, as that's what the founding engineers were familiar with. Many of ML's cousin languages happen to be well suited to this kind of work.
Say I'm starting out with an entirely new project and want to leave the legacy of dynamic typing behind. Is there a flag available to enforce the use of type signatures, causing Hack to throw a compilation error when they're omitted?
Do you imagine a future where Hack will merge back into PHP (like PHP 7), in the same style that Beryl & Compiz then rejoined? Or does the team intend for the two to always be adjacent-yet-separate?
HHVM developer & PHP runtime developer here. I've got hands in both runtimes and all even I can say is: Maybe.
I think the most likely outcome is that PHP will adopt some of HHVM's additional features, but remain a separate project. IMO that's a great outcome, since we'll both likely drive the other to be better.
My impression is that Facebook mostly write their stand-alone services in Java or C++, and are using PHP only where they're "stuck" with it due to a large existing code base.
Do you think Hack is a good language to start a new project in, compared to non-PHP languages? Are you using Hack for things besides the main web page?
Yeah, I think Hack is a good language to start a new project in. For as much flak as PHP gets, there are actually a lot of good things about the language. The fast development cycle -- edit php script, refresh -- is something amazing that you don't get in a lot of statically typed languages, which usually have a compilation step. The crazy dynamic things you can do also occasionally have their place, though it's certainly easy to shoot yourself in the foot.
On the other hand, a lot of the time you want the safety that strong static typing can give you. Even just the null propagation checking can immediately find tons and tons of silly little bugs without even running the code, and ensure that the code stays consistent as a "mini unit test" if you will.
Hack hits the sweet spot of both. Wiring the Hack typechecker into vim was really revolutionary for me -- having both the immediate feedback of the type system for all the silly bugs that I was writing, along with the fast reload/test cycle from PHP, is great.
Er, `paste serve --reload` restarts small-to-medium Python projects faster than I can alt-tab, which is actually faster than my static blog engine can regenerate itself too.
Is there a statically typed variant of Python that would work with existing web servers, etc..? I am aware that there's Cython and I know that py3k technically permits type annotations (which Jetbrain's Python IDE uses quite effectively), but that isn't true static type checking in the same way as Hack does this.
Statically-typed Python would ruin a great number of Python libraries you'd probably want to be using. It'd be a very different language.
Once you have type annotations, it wouldn't be too much of a stretch to enforce them statically with a separate tool. You could even go as far as rejecting first-party code if you can't statically determine every single value's type. Pylint's underlying astroid library has a bunch of inference tools you could perhaps build on top of.
Such a tool would be no less difficult to build than hack itself, though. Hack's "gradual typing" solves the problem of re-using existing code that you've mentioned.
FB already had a PyLint-like tool earlier that could do some static analysis, namely pfff (also open source and written in OCaml), but it did not provide a full-on static type system like Hack. (Background: I used pfff when I was in bootcamp at FB itself. This was however prior to hack, I worked solely on C++, Java, and a bit of Python at FB after bootcamp).
I am sure if FB started off with Python, a similar solution could have been found, but if you're looking for a tool that exists _right_ now, Hack is actually quite decent.
Creating a static type system, implement local type inference, as well as working out "gradual typing" and associated problems (all while being able to do type-checking at speeds developer _expect_) is not a trivial problem.
The announcement post says the actual type-checking happens in a persistent server that watches for filesystem changes. That sounds pretty close to continuously running a linter. It also says "without breaking things", so I'm a little fuzzy on whether badly-typed code will actually execute or not.
For that matter, can you call a typed function from an untyped one? Or, worse, a typed method? If the typing is purely static, there's no way to know the method you're calling is actually typed, so there's no actual guarantee that it receives the types it's declared unless your entire program is typed. It doesn't seem like a very strong guarantee if both the caller and the callee have to opt into the typing.
If you're looking for a tool that exists right now, you either have an existing codebase and can't port it to Hack if it's not already PHP anyway (for the same reason Facebook couldn't port away from PHP), or you're starting from nothing and could just use a statically-typed language in the first place.
I don't know if I'd even be excited about the prospect of optional static typing in Python. (It hasn't gotten me interested in Dart, for example.) I'd kinda rather see the effort poured into something that could do static duck-typed analysis/inference, e.g. balk if I pass an argument that could be a non-string into a function that tries to call `.startswith` on it. (Ah, but maybe it could theoretically be a string or None, and I only know it isn't None for reasons the type system can't see, and now I hate the type system.)
I didn't say it was a trivial problem. I just don't feel excited by the solution.
The default mode in Hack is partial: in partial mode, the code itself must be typed and must past the typechecker, but it can call untyped code (that's in a separate compilation unit).
Another mode (you specify the mode per file/compilation unit) is "strict". In strict mode, you can not code any un-typed code (note, the standard library is typed with hack).
(There is a bit more nuance here, but you can read that in the documentation.)
So the idea is to eventually migrate most of the code to strict, but code that relies on legacy can remain partial and you can write new code without waiting for a re-write to finish.
"Shapes" are also a neat feature specifically for parts where static typing can be frustrating for dealing with HTTP requests specifically: http://docs.hhvm.com/manual/en/hack.shapes.php
(FWIW I don't see myself using Hack, but I'm not a web developer. I'd say the ML family languages are my favourite, but for what I do day-to-day it's not really an option.)
Do you know if other languages have static null checking i.e. your null annotation/propagation (apart from Haskell's Maybe union type etc)?
I'm intrigued, because it's such a good idea (especially when null's originator claimed it was a "billion dollar mistake"), though Java doesn't have it. I'm wondering if there's some subtle problem with it...?
Also, how do you make your vim typechecker fast enough? Usually, even syntax colouring is local to ensure adequate performance - and a typechecker with inference/propagation would be very non-local.
I'm stoked. And disappointed the "elvis" operator didn't make it in.
I hope some day Java breaks backwards compatibility and eliminates null entirely. Then again, that's already happened with the proliferation of other JVM languages. But that doesn't me at my day job, where we have a large legacy code base... which would need to be ported to a backwards-incompatible version of non-null Java anyway. Hm.
Well, with Java 8 I can at least start to grow null-safe code within our codebase.
>The fast development cycle -- edit php script, refresh -- is something amazing that you don't get in a lot of statically typed languages
You seriously think that? That's how we do haskell web development. Both yesod and snap do this out of the box. That's how every java developer I know works.
I have a little bit by way of Haskell chops, and I'll venture that the performance of the Hack typechecker is a very big deal, and it is in a different breed than the turnaround time you get from snap or yesod (or Java).
Edit: I misread what you wrote. I thought you were saying there was something fundamentally different about the type checker, but more that reload experience is different then what you get with Yesod.
"Type checking is faster than other statically typed languages" is quite different from "other statically typed languages don't offer this workflow", which is what was claimed.
How do you do it in java? Compile (takes time) -> hotswap (takes time), or can't hotswap since changes to signature, will need to restart server (takes lot of time).
Yeah, that's the one we're using. Still takes a couple of seconds, though. And as I said, big changes can't be reloaded, so the whole server will have to be restarted.
100% of our web front end developers use Hack now. This has been an organic process of growth over the past year, by which I mean our engineers are using it because they like it and see value in it, not because there's someone standing over them with a big stick :-)
The biggest learning step for our engineering teams was to treat type errors from Hack as actual logic errors. We have a collection of "linters" that provide advice on code style and other nice-to-have factors. Some people (quite reasonably) initially thought of Hack errors as lint-like stuff that it was safe to ignore, when in fact they indicate real logical inconsistencies in code.
> Some people (quite reasonably) initially thought of Hack errors as lint-like stuff that it was safe to ignore, when in fact they indicate real logical inconsistencies in code.
Interesting, thanks!
One followup: what has it been like from an ops perspective? Similar to PHP, or is there a better frame of reference?
Sure. I guess I'm wondering how it compares to running plain old Apache/PHP in a production environment. Or, is it more like a Django/Rails stack? Does it use the same memory footprint as PHP, etc?
Facebook hasn't used plain old Apache/PHP in production for several years (HipHop for PHP was announced in Feb 2010), so it is hard to compare.
HHVM is its own web server (although it supports FastCGI for easier use with existing infrastructure like nginx), and that's how we use it in production. It's hard to compare memory usage, except at scale, where it benefits from not having a whole bunch of interpreters (in different processes) running at the same time and some other benefits by using more appropriate types to store values through type inference.
On the scale of a single request (doing stuff from the command line), most benchmarks I've seen are about half the memory footprint. Obviously that's going to vary program to program ($data = file_get_contents("some2gbfile.txt"); is going to take 2GB, regardless), but for "normal usage" 1/2 looks fairly common.
On a webserver, that goes further since HHVM is single-process/multi-thread, whereas PHP (in its typical setup) is multi-process/single-thread. This cuts HHVM's memory overhead much further.
Yes, PHP can run multi-threaded, but it still has a number of instability issues in that mode.
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.
The key difference is affecting the runtime. All those typescript features can be compiled down to regular JS and typescript-generated javascript can be run in a browser without extending the JS engine.
I don't know what you mean by that... stuff like classes were already in the harmony proposal phase before Typescript implemented them. Stuff like type hints won't be in JS ever.
At least to date, Microsoft stresses the "TypeScript is just JavaScript." New language features are added to ES6 and then wrapped with types in TypeScript.
A question about the type inference mechanism: in PHP, while it is possible to define object interfaces which classes may be defined against, by the dynamic nature of the language, functions don't necessarily need that interface specification to accept an object conforming to it, explicitely or implicitely. OCaml provides something "similar" with its object system, but much more powerful with static inference of an object (super)type from its usage. will Hack be able to infer an object interface as well from its usage in a function?
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.
Thanks! I was mostly thinking about point 2, and I understand your motivations in going in a different direction after trying it. Very good and enlightening answer!
We don't do any type inference across function boundaries, so we largely dodge the issue that I think you are getting at. (Please elaborate if I misunderstand!) We rely on interface and class definitions in order to know what methods are available, and even though the runtime resolves everything at runtime so you can call any method that happens to exist at that time ("duck typing"), we enforce statically that methods do exist where we can. So for example, the following code will work at runtime since the method `g` does exist, our static typechecker will reject it since it does not exist on type `I`.
<?hh // strict
interface I { public function f(): void; }
class C implements I {
public function f(): void {}
public function g(): void {}
}
function f(I $i): void {
$i->g();
}
f(new C());
Thank you! You brought an interesting point with the example you gave, it is one of the things I was thinking about. Thank you for your work, and for making it available!
Pretty star-studded cast you have on the core team, there.
What's your motivation, aside from modernizing Facebook's code base? What language niche does Hack serve which is not served by other languages? Why Facebook at all (aside from the rarity of finding a company to pay you to write a compiler :))?
The sweet spot that Hack hits is that it combines gradual typing (an idea that hasn't yet seen much real-world adoption) with an incredibly fast typechecker.
This lets you choose the pace and extent to which you want to adopt the safety of static typing, while preserving your dynamically typed code -- and without sacrificing the rapid turnaround of PHP.
How does your approach compare to Typed Racket and Typed Clojure? Could they conceivably achieve the same performance or is there a fundamental difference?
Does Typed Racket have DrRacket support for instant feedback on errors? (It didn't 4+ years ago when I used Racket.)
Typed Racket also includes more types, like ": Integer [more precisely: Negative-Fixnum]" (from docs), as well as polymorphic data structures and higher-order functions. I don't know if this is a "fundamental difference" but it might mean Facebook's type checker can optimize in certain ways that Racket's cannot.
Yes, Typed Racket does have that -- DrRacket continuously expands in the background, so Typed Racket gets it for free by integrating into the macro system.
The Typed Racket type checker is much slower than Hack, though.
Hack does seem to have polymorphic data structures and higher-order functions.
If you look at the original C syntax for function types, it is also a bit weird: part of the type (the return type) is placed before, and part (the parameters) after.
That syntax in hack seems more "functional" to me. That said, I must admit that I kind of like the C syntax, because of its oddity.
I too programmed for a long time in AS3/Haxe, and while I prefer variable:type as I think it's more readable, most static languages (java, C#) do it the other way.
Thank you for your work on this and for open sourcing it. It looks like it can make large code bases in PHP a great deal more manageable.
Do you expect Hack to be stable without large breaking changes going forward?
The documentation doesn't say much about the scheduling for asynchronous tasks. Can async functions be used to batch requests to e.g. caches and databases? Can Awaitable be used to interface with code that expects chainable Future or Promise-style interfaces?
Can HHVM/Hack use standard PHP extensions, or how much work is it to port an extension?
Is there a Hack plugin for IntelliJ?
Does the Hack project have a mailing list or forum?
Our internal plumbing is different, so the extension APIs aren't the same, thus PHP extensions can't normally be used with HHVM. Paul has a source-compatability transformer which works for simple extensions (no fancy stuff allowed), but we recommend anyone with an extension consider porting the code.
If your extension is one of those "This was written in PHP but we wanted it to be faster so we turned it into C" types, you should consider going back to PHP for it. In practice, we find that HHVM can JIT PHP code into running about as fast as (sometimes faster than) C/C++ extension code.
If you do need to dip into C/C++ (because you're calling an external library), the API we've designed is a LOT easier to work with than PHP's. And I say that with the authority of having written THE book on writing PHP extensions: http://amazon.com/dp/067232704X .
With Async functions I'm not sure if the documentation is lacking or I'm just slightly thick, I believe the later.
(I'm not a php developer so excuse my ignorance)
It seems you only have 1 method 'await', to check if the async function has completed its job (it self, if I'm understanding is a blocking operation in which ever thread/worker its called).
So is there a way to run something more similar to
Because as I see it now, what ever I run asynchronously I.E.:
gen_foo(get_user_data); //async
$x = do_something_for_a_while(); //do something while gen foo processes
do_new_thing($x, await gen_foo()); //do something with rendezvous result
I'm forced to time out my async calls so that they'll rendezvous in the same place won't I?
Again if I'm completely off the mark please let me know.
async/await allows cooperative multitasking on a single thread: stay tuned for more...
The way it works is quite different from your example:
async function gen_foo(): Awaitable<string> {
echo "until we get to an await, eager execution\n";
// ...
await gen_bar();
// this code is only executed after await
return 'result';
}
$x = gen_foo(); // x is a handle, suspended at the point of its first 'await'
await $x; // ... and now it's resumed
The benefit comes from being able to batch these async functions together:
list($x, $y, $z) = await genva(
gen_foo(),
gen_bar(),
gen_baz();
); // genva creates a wait handle for awaiting its args
// ... and when we get here $x, $y, and $z are all assigned
As the author of pretty much THE book on writing PHP Extensions ( http://amazon.com/dp/067232704X ), I can say with a fair bit of authority that writing HHVM extensions is SO SO SO much easier.
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.
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.
Not Bryan, but I am an engineer who works on Hack :)
We don't (statically) protect against type errors when you cross from untyped into typed code. If you call an untyped function, we assume the programmer knows what they are doing -- just like PHP does. You might get a runtime exception if you are calling a method on null, for example.
This is actually a pretty important part of the conversion process. You don't have to convert all your code all at once. Typed code can be verified statically; untyped code is assumed to work just as before.
Parameter and return type annotations are enforced at runtime by HHVM (just like you can add a class type annotations to a parameter in PHP). This will protect against some inconsistencies -- again, just as if you weren't using Hack.
At runtime, we check and enforce parameter types at function entry and return types at function exit. The extra type information can also enable the JIT to emit more efficient code in some cases, and work is ongoing to make that even more efficient. But having these types is independent of being in Hack -- you can have fully untyped Hack code, though I wouldn't advise it, as you are leaving one of the most powerful features of the language on the table.
What do you do with higher-order functions (which PHP has I believe)?
If I write a typed map : (a -> b) -> [a] -> [b]
and then it's called with an untyped function as input, but it returns a something that's not a b. Do you place some kind of barrier around it so that that's stopped immediately?
Does this presentation match the current version of Hack fairly well? It has a nice explanation of the type system that is more concise than the one on the web site.
The idea of bolting a static checker onto a dynamic language and using an unresolved top type to make it work is cool. The presentation refers to your system as SoA gradual typing. Are there any papers or presentations which explain that approach and how it works in more detail? Particularly in how it might differ from gradual typing?
I'm a little confused as to the need for Hack unless you have a code base in PHP and need to ship tighter code (which is a problem Facebook has and my team probably has as well).
Adding lambdas makes PHP more Ruby-like and generics and type checking are straight out of Java. I'm still unconvinced in how this makes programming websites more efficient or bug-free than existing languages. Can you please elaborate on that?
If you're looking for a statically-typed version of Python/Ruby, I'd say nimrod gets fairly close. It's also fantastically fast and compiles to portable ANSI C.
Nimrod is not a statically typed version of Python in the sense Hack is a statically typed version of PHP. Not at all. Hack is gradually typed, Nimrod is not. Big difference.
I thought it was clear I wasn't trying to draw an analogy between PHP/Hack and Python/Nimrod, but rather pointing out that Nimrod is a very nice language for someone who enjoys Python but wants static typing.
Have you guys looked at the new Truffle/Graal back end in Java 8? It has seen some impressive numbers in other languages, did you explore this as a possibility?
That's coming in PHP 5.7 anyhow. It's been implemented and works, but Nikita Popov hasn't had the time to change the function definitions of the standard library to work with it, hence PHP 5.6 won't have it, sadly.
Wow, I haven't kept up with things, but gosh that sounds pretty great. Type checking + named params is a fairly difficult combination of great language features to find in the same language.
Static types are more than syntactic sugar, they allow you to make additional guarantees about the behavior of the code, like having unit tests without actually writing them.
I program in php every day and miss static typing (as opt-in mechanism). Sadly i'm on windows and use oracle, so hhvm is not applicable.
We are just beginning to use the static type information that Hack provides to yield performance optimizations, and that's definitely on the cards as something we'd like to push further.
