Would Hindley Milner type inference be useful to PyPy for RPython?

Question

Does PyPy do static type checking at compile time to catch type errors at compile time? And if not would something like HM type inference be useful to catch those errors at compile time?

Answer 1

No on both accounts. (I assume that by PyPy, you mean the Python interpreter with JIT compiler and other features.) It does not do static type checking of Python code at any time, because it implements the Python language, not of a statically-typed Python-like language. The truth is, you *can'*t detect all type errors (for most definitions of "type error") in Python programs statically. You can try to find some, but even if you can proof that a type error would occur at runtime, you can't refuse to execute the program, because it's perfectly valid (and sometimes useful) to run that code from somewhere else and catch the exception.

And by the way, the type system Damas-Hindley-Milner infers types for is not even remotely sufficient to express even a useful subset of the "types" in Python programs (not that most popular static type systems fare any better). Try to type zip, for instance (hint: Haskell doesn't have it, it has several functions specialized to 2, 3, 4 arguments). Or, if you want something harder, getattr. And then there's the whole nominal and structural subtyping thing.

There have been attempts to infer types in Python and similar languages, but these approaches are necessarily quite different from what the functional programming world has done in that area (see above). Also, these projects never find all type errors in Python programs (though some have covered vastly simplified subsets, or detect some errors in Python programs). Do some research (Lambda the Ultimate has many links).

Now, the name "PyPy" was historically also used for the RPython translation toolchain, which does indeed, among many other things, infer static types for RPython programs. But RPython isn't Python (it has lots and lots of restrictions, to the point that it is effectively a different language), and the type system and type inference is radically different from DHM (whole-program, based on abstract interpretation, entirely different type system).