The nature of Haskell type system: static/dynamic, manual/inferred?

Question

I'm learning Haskell and trying to grasp how exactly Haskell type system works re working out what is the type of the thing: dynamic, static, set manually, inferred?

Languages I know a bit:

• C, Java: set manually by a programmer, verified at compile time, like int i;, strong typing (subtracting integer from a string is a compile error). Typical static type system.

• Python: types inferred automatically by runtime (dynamic typing), strong typing (subtracting int from a str raises exception).

• Perl, PHP: types inferred automatically at runtime (dynamic typing), weak typing.

• Haskell: types often inferred automatically at compile time (either this or type is set explicitly by a programmer before compile time), strong typing.

Does Haskell's type system really deserve description "static"? I mean automatic type inference is not (classic) static typing.

Answer 1

The static-dynamic axis and the manual-inferred (or manifest-inferred) scales are not orthogonal. A static type system can be manifest or inferred, the distinction doesn't apply to dynamic typing. Python, Perl, PHP don't infer types because type inference is the deduction of static types via static analysis (i.e., at compile time).

Dynamic languages don't deduce types like that, they just compute the types of values alongside the actual computation. Haskell does deduce types statically, it is statically typed, you just don't have to write the static types manually. Its type system indeed differs from mainstream type systems, but it differs by being inferred rather than manifest (and many other features), not by being not static.

As for strong/weak typing: Stop using that term, it is overloaded to the point of being useless. If by "the type system is strong/weak" you mean "the type system allows/forbids X" by, then say that, because if you call it strong/weak typing a large portion of your audience will have a different definition and disagree with your use of the terms. Moreover, as you see, for most choices of X it's rather independent of the two distinctions you mention in the title (but then there's the sizable group that uses strong as synonym for static and weak as synonym for dynamic, oh my!).

Answer 2

Does Haskell's type system really deserve description "static"? I mean automatic type inference is not (classic) static typing.

Type inference is done at compile time. All types are checked at compile time. Haskell implementations may erase types at runtime, as they have a compile-time proof of type safety.

So it is correct to say that Haskell has a "static" type system. "Static" refers to one side of the phase distinction between compile-time and runtime.

To quote Robert Harper:

Most programming languages exhibit a phase distinction between the static and dynamic phases of processing. The static phase consists of parsing and type checking to ensure that the program is well-formed; the dynamic phase consists of execution of well-formed programs. A language is said to be safe exactly when well-formed programs are well behaved when executed.

From Practical Foundations for Programming Languages, 2014.

Under this description Haskell is a safe language with a static type system.

As a side note, I'd strongly recommend the above book for those interested in learning the essential skills for understanding about programming languages and their features.

Answer 3

Before going to SO it would be good to check e.g. Wikipedia, which says that "Haskell has a strong, static type system based on Hindley–Milner type inference." Static refers to when type checking is done, so whether types are inferred or not doesn't matter.