4 ms·

> Static type systems will typically require you to state the full type of o. This is not the case for languages with support for structural typing (as the art

> Static type systems will typically require you to state the full type of o. This is not the case for languages with support for structural typing (as the article mentions in the appendix), and most modern statically typed languages have some degree of support for abstract interfaces of some sort which also support writing functions with only partially known information about the type. I think one of the core insights in the article is that your code will always make at least some assumptions about what it is processing (unless you're implementing the identity function, or a function which does not inspect its argument at all), and these assumptions are your type. So if you expect "o" to have a field called "f", and this field should return something on which a "+" operator is defined, then these properties form your type (in structural typing this is easy and boilerplate-free to express, with interfaces there's some boilerplate but it's definitely expressible). In that light, the difference between static and dynamic typing isn't how many assumptions you make in your code, but rather how explicit you are about them, and to what extent you make your assumptions amenable to automated reasoning.

sparkie 7y ago
The difference between static and dynamic typing isn't about how explicit you are about the assumptions in your code. You can be equivalently explicit in dynamic and static languages. The fundamental difference lies in when you want the types to be verified. In static typing, that is before the program is run. In dynamic typing, that is before the code is executed if you are explicit, or when the code is executed if you are not explicit enough. An example of dynamic typing being used pervasively in what we commonly call statically typed languages is the downcast. (SubType)superTypeObject is a dynamic typing construct. It is saying "defer unification of these types until runtime," because there is insufficient information at compilation type to determine the real type of superTypeObject. Of course, such downcasts are discouraged in statically typed languages without explicitly checking the type of superTypeObject before performing the downcast, but not all type systems are capable of asserting these checks are all in place at compile time. Some statically typed languages don't even have a downcast. You can be completely explicit about checking types before using them in a dynamically typed language, and have the proper error handling in place in the case that the type unification you're expecting doesn't happen.
- ookdatnog 7y ago
  Yes, you're right, it's not about how explicit you are, or even how explicit you have to be. You can write "stringly typed" code in a static language where none of your assumptions are apparent in the type system. Conversely, regardless of your typing discipline, you can be completely explicit about your assumptions just by writing comments. This fits in a larger point that, in the end, the technical qualities of a language in many ways matter less than the culture surrounding the language. Even Haskell has unsafePerformIO which means that none of its guarantees about referential transparency actually hold, in theory. In practice, the culture of the language ensures that, when you pull in a library, you can be pretty sure that it's not riddled with unsafePerformIO, and you can almost always treat code as if referential transparency is guaranteed. A language may facilitate certain habits and discourage other habits. I feel that statically typed languages do not force me to be explicit about my assumptions, but they certainly encourage it by providing immediate benefits to doing so (automated reasoning), and through the culture that surrounds these languages.
pizlonator 7y ago
Structural typing doesn’t save you unless you add other stuff to it. Example: var o = ...; // Value comes from somewhere, doesn’t matter where so long as it’s opaque if (p) ... = o.f else ... = o.g In dynamic typing, we only assert that o has f on the then, and only assert that o has g on the else. Structural typing or abstract base classes or whatever would only save you here if you were very careful about giving o some top type and then casting. But that’s more work - so the tendency is that the static types version of this program will assert that o has both f and g at the point of assignment. And that represents a tighter coupling to whatever produces o.
- ookdatnog 7y ago
  Yes, for that situation you additionally want sum types.

sparkie 7y ago

The difference between static and dynamic typing isn't about how explicit you are about the assumptions in your code. You can be equivalently explicit in dynamic and static languages. The fundamental difference lies in when you want the types to be verified. In static typing, that is before the program is run. In dynamic typing, that is before the code is executed if you are explicit, or when the code is executed if you are not explicit enough. An example of dynamic typing being used pervasively in what we commonly call statically typed languages is the downcast. (SubType)superTypeObject is a dynamic typing construct. It is saying "defer unification of these types until runtime," because there is insufficient information at compilation type to determine the real type of superTypeObject. Of course, such downcasts are discouraged in statically typed languages without explicitly checking the type of superTypeObject before performing the downcast, but not all type systems are capable of asserting these checks are all in place at compile time. Some statically typed languages don't even have a downcast. You can be completely explicit about checking types before using them in a dynamically typed language, and have the proper error handling in place in the case that the type unification you're expecting doesn't happen.

ookdatnog 7y ago
Yes, you're right, it's not about how explicit you are, or even how explicit you have to be. You can write "stringly typed" code in a static language where none of your assumptions are apparent in the type system. Conversely, regardless of your typing discipline, you can be completely explicit about your assumptions just by writing comments. This fits in a larger point that, in the end, the technical qualities of a language in many ways matter less than the culture surrounding the language. Even Haskell has unsafePerformIO which means that none of its guarantees about referential transparency actually hold, in theory. In practice, the culture of the language ensures that, when you pull in a library, you can be pretty sure that it's not riddled with unsafePerformIO, and you can almost always treat code as if referential transparency is guaranteed. A language may facilitate certain habits and discourage other habits. I feel that statically typed languages do not force me to be explicit about my assumptions, but they certainly encourage it by providing immediate benefits to doing so (automated reasoning), and through the culture that surrounds these languages.

pizlonator 7y ago

Structural typing doesn’t save you unless you add other stuff to it. Example: var o = ...; // Value comes from somewhere, doesn’t matter where so long as it’s opaque if (p) ... = o.f else ... = o.g In dynamic typing, we only assert that o has f on the then, and only assert that o has g on the else. Structural typing or abstract base classes or whatever would only save you here if you were very careful about giving o some top type and then casting. But that’s more work - so the tendency is that the static types version of this program will assert that o has both f and g at the point of assignment. And that represents a tighter coupling to whatever produces o.

ookdatnog 7y ago
Yes, for that situation you additionally want sum types.