While I couldn't find any specific info, concerning compiling applications with HHVM (it seems to just perform JIT), this seems to suggest you can type check without having to go into the runtime, "Hack provides instantaneous type checking via a local server that watches the filesystem."[0]
>If we're charitable and say that HHVM has gradual typing, then really it's just slightly better gradual typing than what PHP already has.
Isn't a mix of dynamic typing and static typing, being optional which you use, the definition of gradual typing? Wiki also seems to agree with this[1][2].
I'd say HHVM greatly improves on PHPs type hinting[3], which is rather basic, unless you want to recreate every basic type as an object. Also, with PHP type hinting, you can't specify types of Object attributes/variables, which you can in Hack/HHVM.
[1] http://en.wikipedia.org/wiki/Gradual_typing
[2] http://en.wikipedia.org/wiki/Hack_(programming_language)
Firstly, PHP and HHVM have three "levels" of types:
From a type-theory perspective, these languages are "unityped", ie. all values have the same type. We might write this as:
From a procedural or functional perspective, the types are bool, int, float, resource, string, object, function, etc.From an OO perspective, the types are the classes.
PHP already allows a very limited form of type annotation: function/method arguments can be annotated as arrays or as objects of a particular class/subclass/interface-implementation. These are non-nullable, unless null is set as a default value.
These are checked dynamically rather than statically, and a failing check triggers a fatal error. This makes them path-dependent, requiring an extensive test suite to minimise the number of fatal errors in production, and overall makes them feel more like a very limited form of assertion rather than type-checking.
As far as I understand it, the typing features offered by HHVM over PHP are the ability to use "non-OO types" like int, string, etc. in annotations; annotate more things (like object properties); use generics in classes (a poor man's parametric polymorphism); and for annotations to be nullable without requiring a null default value.
Overall, I wouldn't say that HHVM adds gradual typing to PHP. If we're charitable and say that HHVM has gradual typing, then really it's just slightly better gradual typing than what PHP already has.