Static types, polymorphism and specialization

Question

When I first learned Haskell, I very quickly came to love parametric polymorphism. It's a delightfully simple idea that works astonishingly well. The whole "if it compiles it usually works right" thing is mostly due to parametric polymorphism, IMHO.

But the other day, something occurred to me. I can write foo as a polymorphic function. But when bar calls foo, it will do so with a specific set of argument types. Or, if bar itself is polymorphic, then its caller will assign definite types. By induction, it seems that if you were to take any valid Haskell program and analyse the entire codebase, you can statically determine the type of every single thing in the entire program.

This, in a sense, is a bit like C++ templates. There is no run-time polymorphism, only compile-time polymorphism. A Haskell compiler could choose to generate separate machine code for every type at which each polymorphic function is called. Most Haskell compilers don't, but you could implement one if you wanted to.

Only if you start adding Haskell extensions (ExistentialQuantification is the obvious one) do you start to get real run-time polymorphism, where you have values who's type cannot be statically computed.

Oh, yeah, my question?

1. Are the statements above actually correct?

2. Is there a widely-used name for this property?

Answer 1

Haskell (with no extensions) permits polymorphic recursion, and this feature alone makes it impossible to statically specialize a program to a completely monomorphic one. Here is a program that will print an N-deep nested list, where N is a command-line parameter:

import System  foo :: Show a => Int -> a -> IO () foo 0 x = print x foo n x = foo (n-1) [x]  main = do [num_lists] <- getArgs           foo (read num_lists) 0 

In the first call to foo, a has type Int. In the next recursive call, it has type [Int], then [[Int]], and so forth.

If polymorphic recursion is prohibited, then I believe it's possible to statically specialize a program.