5

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?

  • 14
    Well, I guess Mr. Hurt meant "F# and Haskell have better static typing than C#" (and not that C# is not statically typed). – Doc Brown Oct 20 '13 at 17:45
  • 6
    @DocBrown Agreed. The speaker isn't saying "C# Isn't statically typed", he's saying "C#'s static typing system isn't the kind of static typing I'm talking about here" (where F# and Haskell have a much stronger and more robust static typing system, by comparison) – KChaloux Oct 20 '13 at 18:03
18

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.

  • 2
    But F# has subtyping too. You can write a class and then another class that derives from it. – svick Oct 20 '13 at 18:17
  • 3
    @svick The question is, How do languages like Haskell and F#'s type systems differ from C#. The overlap of Haskell and F# is system F. I could also say Haskell has existentials which can be used to throw away type information, but that wouldn't make sense the part on F#. – Daniel Gratzer Oct 20 '13 at 18:22
  • 5
    @MauricioScheffer I feel like your kinda proving my point, 142 lines of code to define a simple sum? And how much of this can the compiler validate for you (in your implementation as well). In Haskell or F# it's 1 line. It's the same argument as encoding subtyping in Haskell, you can do it, but it's so ugly and impractical that it's just not the same benefits as with languages with first class support for it – Daniel Gratzer Oct 21 '13 at 14:04
  • 2
    What does line count have to do with anything? You say "Anyone can come along and add something to it.", I'm showing how that's not true. I'm not proving your point, I'm proving you wrong. "Ugly", "impractical" aren't objective arguments. I use this encoding every day in my C# day job and find it very useful and "practical". Also, 142 lines includes the entire example. Definitions are 80 LoC including functor and applicative functor operations. – Mauricio Scheffer Oct 21 '13 at 14:08
  • 7
    @MauricioScheffer your point about sum types appears to be "You can create them in C# too" which is basically the old fallback of in a turing complete language you can create any other language, that doesn't mean the language inherently has the features of that other language. jozefg's point is that sum types are a language feature in F# and Haskell – Jimmy Hoffa Oct 21 '13 at 14:48
2

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.

  • @jozefg: you're right, but in this context the formalism and the actual implementation are irrelevant. Modern languages are often multiparadigm, and can support both the ways in a more or less simple way. C# just supports both the paradigms. Saying "it's not one", just because "it has also the other" (like the speaker says) is instrumental to other means, but not to proper definition of terms. – Emilio Garavaglia Oct 20 '13 at 19:21
0

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#).

  • 1
    @downvoter: it would help if you explained what you think is wrong with my answer. – svick Oct 20 '13 at 18:06
  • 1
    I'm an up-voter: your answer has nothing wrong. But since what we are talking about is a religion (or better: two religions at the same time) every believer in one of the two down-votes. Who knows both of them up-votes (but they are few, and considered miscredents from all the others), and all the real "atheist", simply don't care, and use C++11 – Emilio Garavaglia Oct 20 '13 at 18:52
  • 1
    I'm a downvoter. The question is asking what did someone mean in a sentence. You are assuming that the person that said that sentence wanted to give a "definition", why do you assume that? Just take a look at the most-voted answer to see that he had a valid point when stating that. – knocte Oct 20 '13 at 20:59
  • 2
    And of course his talk is basically a praise of Haskell's type system. The talk was on the pragmatic benefits of static typing systems like Haskell's system to the New York Haskell Users Group. Whether he's right or wrong about the benefits of that kind of static typing, that's what his talk was about. Also, you completely missed the point about nulls: in Haskell, there are no null pointer errors. There is a difference between a kind of error being rare, and that error being impossible. – Michael Shaw Oct 20 '13 at 23:00
  • 2
    @svick: An actual quote from the talk: "Most of what I say will apply to all of these ... I can actually say stronger things in Haskell than I can any of these others." Re-watch the video from 4:20 to 5:05. Compare the words you put in his mouth to what he actually said. – Michael Shaw Oct 21 '13 at 0:30

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.