Actually, for a large codebase written in a dynamic language, introducing gradual typing to slowly convert all the dynamic code, into more stable statically type code, can be a quite nice approach (compared to rewriting the whole codebase).

Take for example Facebook and their HHVM[0]. They can run the existing code, and then slowly update the code with types, and write new code with types. The alternative would be years and years of rewriting the whole codebase.

Personally though, I'm more a fan of the type-checking done in languages like Haskell, F# and ML.

[0] http://hhvm.com

HHVM is a rather odd example, I think.

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:

    Any = Bool + Int + Float + Resource + String + List ((String + Int) * Any) + (Any -> Any) + ...

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.

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.

[0] http://hacklang.org

[1] http://en.wikipedia.org/wiki/Gradual_typing

[2] http://en.wikipedia.org/wiki/Hack_(programming_language)

[3] http://php.net/manual/en/language.oop5.typehinting.php

Even so, one would know at code writing time "this is a number of some sort" , "this will be a string of some sort", "I'm expecting a class in here", "this will be a collection".

If one uses a decent type system that has user defined types and interfaces then that gradual stuff disappears.