Programming Languages – Why C# is Not Statically Typed but F# and Haskell Are

%fchaskell

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?

Best Answer

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.

Related Topic