[sklogic]

This is exactly the fallacy that dynamic proponents are constantly running into. Do not help them by reinforcing such claims.

Static typing bears important semantics far beyond a mere "validity checking" and compile time optimisations. And this fact is overlooked far too often.

[danbruc]

What then would be a better definition in your oppinion?

[sklogic]

In a static type system, all of the expressions and expression-like constructs of your language may have a constraint attached to them, which guarantees that a value this expression yields have certain properties; In a static type system there is a well defined set of rules, describing how such constraints are transformed when expressions are combined in a certain way.

In a dynamic type system, no such constraints exist (besides for the constant literals, of course) and there are no rules for combining the constraints.

These definitions should cover all the spectrum.

[ubernostrum]

These definitions should cover all the spectrum.

This gets close but I think it doesn't yield a conclusion that Java is statically typed, and I think most people want a definition that concludes Java is statically typed.

(unless you allow only fairly trivial "constraints" in which case you're no longer distinguishing between categories of languages, since essentially any language can satisfy a trivial-enough constraint on its expressions)

[dllthomas]

I think it's reasonable to draw the line somewhere between Java and, say, Python in the kind of constraints that a type system can enforce. Java does not have a particularly sophisticated type system, but I wouldn't be surprised if I could get some reasonable help from it (I haven't written any Java in years, much Java in longer...).

[ubernostrum]

Just remember that one of the reasons why the JVM does all sorts of fancy/mind-boggling runtime heuristics and optimizations is precisely because it's not possible, at compile time, to always determine a usefully-specific type.

(and to really go off the deep end, in Java it's not possible to determine even what the universe of possible types is at compile time, which is why I like it as a counterexample to people who think they can meaningfully define "statically typed" and have it manage to include Java)

[dllthomas]

> it's not possible, at compile time, to always determine a usefully-specific type.

You seem to be using "type" here to mean "runtime representation", which is a common use but is only one specific case of what is being discussed above. As I understand it (and remember that my Java is rusty), it is entirely possible to statically guarantee that whatever a given expression evaluates to, it satisfies a particular interface (moreover, it was deliberately labeled as doing so). That may not be "usefully-specific" for an optimizer (or more carefully, it may leave some vague that will be more usefully specified at runtime; we haven't established that the level of specification is of no use), but it certainly seems to be a constraint of the sort that sklogic was talking about above, and it seems like something that could be useful to me as a programmer.

I actually think that "representational types" - constraints that tell us explicitly about how the data is represented in memory - is the place where the dynamic typing languages got it right. As long as it's internally consistent, I don't care exactly how the data is laid out, and automatic systems can do a plenty good enough job figuring that out (except at system boundaries where I need to worry about interchange, or if I care an unusual amount about performance). If representation is not something I care about, I should not be wasting time/attention talking about it. Where, IMO, this goes wrong is overgeneralizing to say, "... and since that's all types are good for, types are not useful." That's not all types are good for.

> (and to really go off the deep end, in Java it's not possible to determine even what the universe of possible types is at compile time, which is why I like it as a counterexample to people who think they can meaningfully define "statically typed" and have it manage to include Java)

How is the same thing untrue of C? or Haskell? If I write code that interacts with data generated by a dynamically linked module, that data might include newly defined types. This isn't a problem for the theory - we've still internally verified the constraints we're checking in each module, and potentially also at the interface (depending a bit on ABI).