There was a talk given by Brian Hurt about advantages and disadvantages of static typing. Brian said that by static typing he don’t mean C#, but F# and Haskell.
Is it because of dynamic keyword added to C#-4.0? But this feature is relatively rarely useful. By the way, there are ⊥ and unsafeCoerse in Haskell which obviously are not the same, but something that could blown your head off in runtime similarly like exception thrown as a result of dynamic.
Finally, why F# and Haskell could be named a statically typed languages and C# couldn’t?
2
I’m addressing the overlap between Haskell and
F#’s type systems. The part they share is a simplified subset of a system known sometimes as System F. F# by necessity provides bits and pieces of C#’s type system, but this isn’t what the speaker was talking about.
Both C# and Haskell/F# are statically typed, but they’re two different flavors.
Subtyping
Specifically, C# is a statically typed language with subtyping. This means that if you look at the typing rules for C# there’s one like
Env |- x : T, T' <: T
---------------------
Env |- x : T'
Which means that any well typed term has more than one potential type. This in not the case in (vanilla) Haskell or F#. Every type has a single most general type, a principal type. This has a few benefits like total type inference.
Expressions Everywhere
Besides this, Haskell and F# have a greater emphasis on expressions, expressions have types, but statements don’t. This means that in C#, the compiler is checking less of your code, because less of your code has types. In Haskell, everything has a real, checkable type.
In substantive terms, every single node on a Haskell AST has a type or kind (or sort). The same cannot be said of a C# one.
Sum Types
Beyond this, Haskell and F# have what are known as sum types.
data Bool = True | False
This is how a boolean is defined in Haskell. This provides a few different guarantees than in C#. For example, when there are a discrete number of things in C#, like say, an AST. We can model this with an inheritance hierarchy, but these are open. Anyone can come along and add something to it. We can use an Enum, but then there’s no sane way to attach data to each tag uniformly. This is what’s called a tagged union, and it’s up to you to implement/use it correctly, the compiler ain’t gonna help.
This makes it very hard to ensure that we’ve covered all possible nodes of an AST. For example, say you have a function
doStuff :: AST -> AST
doStuff (SomeExpr ..) = ...
doStuff (SomeStatement ..) = ...
--// doStuff (SomeIf ...) = Oh noes, we forgot a node
The compiler can warn you because it can prove exactly how many nodes there are, ever. In C#, the equivalent would have to be done with downcasting, and then, since the set of nodes in our hierarchy is open, there’s no way to issue compile time warnings.
A company, Jane Street, raves about how useful this feature is in their large OCaml code base. Watch a few of their talks, they talk quite a bit about how using OCaml impacts them in the Real World.
Soapbox
Now I’ve outlined quite a few differences over System F over many mainstream type systems, but they’re all still static type systems. It does bother me when people call Java/C#/C++ “not statically typed” they are. And they certainly give you more compile time guarantees than say, Python. So it’s a bit unfair to dismiss them out right.
16
There is lot of “marketing religion” and very few science here.
A static_typed laguage must support the definition of types and type checking at compile time, and a dynamic typed language must support the change of the type of the variable at runtime.
The two things are not necessarily mutually exclusive: a language can support both the paradigms:
the only important thing is that what is defined to be static cannot become silently dynamic.
1
Slightly paraphrased and shortened:
What I don’t mean by static typing: C#. What I do mean: F#. Now with an actual solid definition …
That’s not a definition, let alone a solid one. I think the answer to why C# isn’t statically typed is, but F# is, is: Because the author of the talk said so.
A “definition” like that is completely useless, it doesn’t say absolutely anything. And it’s impossible to reach any conclusions based on that.
After watching the talk: it basically seems to be a praise of Haskell’s type system.
Some of the points don’t apply to the languages that supposedly have static typing (you can’t easily implement STM in F#, because it’s not pure). Some of the points do apply to the languages that “don’t have” static typing (you don’t have to worry about nulls much in modern C++; you can write type-safe Either in C#).
13