9 ms·

Chris Smith - who wrote the original piece years ago - added a current prologue to the text. I think part of it is an excellent summary so I quote this part her

Chris Smith - who wrote the original piece years ago - added a current prologue to the text. I think part of it is an excellent summary so I quote this part here: > If pressed for an answer, though, yes I still do believe in the central conclusions of the article. Namely: > That “static typing” and “dynamic typing” are two concepts that are fundamentally unrelated to each other, and just happen to share a word. > That “static types” are, at their core a tool for writing and maintaining computer-checked proofs about code > That “dynamic types” are, at their core, there to make unit testing less tedious, and are a tool for finding bugs. > That the two are related in the way I outline: that one establishes lower bounds on correctness of code, while the other establishes upper bounds, and that questions about their real world use should come down to the possibility and effectiveness of addressing certain kinds of bugs by either computer-checked proof, or testing. EDIT: When I wrote this comment the post linked to Steve Klabnik's 'reprint' of the temporary lost original article. Currently it links to the original. The 'reprint' missed the prologue.

draw_down 8y ago
> ... “dynamic types” are, at their core, there to make unit testing less tedious, and are a tool for finding bugs. I don't think this is a good description of dynamic typing. I'd probably go with something more like, dynamic typing is a way to defer until runtime typing aspects of the program's implementation. I suppose dynamic typing does make unit testing easier, among other things, but it feels wrong to say it's "for" that. A car is for getting one or more people from point A to B. It also has a radio, but a car is not "for" listening to the radio.
- naasking 8y ago
  > I suppose dynamic typing does make unit testing easier, among other things, but it feels wrong to say it's "for" that. The summary is trying to say that that's dynamic typing's primary advantage. Any other advantage you'd care to ascribe to dynamic typing is not intrinsic to dynamic typing itself.
  - ridiculous_fish 8y ago
    The whole article seems concerned with the testability and bug-finding nature of types. But the main strength of dynamic types is the ability to defer decisions until runtime. JS isn't dynamically typed to make testing easier. JS uses dynamic types because you couldn't build the web any other way.
    - naasking 8y ago
      > But the main strength of dynamic types is the ability to defer decisions until runtime. That's not a strength. Deferring until runtime only that which must be deferred is a strength, but that's not one exhibited by dynamically typed languages. It is one that's available to statically typed languages though, like C# and now even Haskell has a deferred typing mode. > JS uses dynamic types because you couldn't build the web any other way. That's patently false. The whole engine running every browser is statically typed. There are libraries for working with the full DOM in HTML documents for Java, C# and other typed languages.
      - ridiculous_fish 8y ago
        Obviously the ability to defer decisions to runtime is a strength - how could you possibly dispute that? And yes statically typed languages have this strength if they use dynamic types. The article's point is that static and dynamic types are fundamentally unrelated to each other. Many languages can and do use both. When you make a web page you have no idea what "only must" be deferred. There's no way to enforce that the JS you write today will be statically compatible with the libraries and browsers that it touches tomorrow. That's why JS uses dynamic types. > That's patently false. The whole engine running every browser is statically typed My point is not about building web browsers, it is about building the web. The web has JS which must coexist with arbitrary other JS, running on many different browsers with many more versions. How could you possibly build this without dynamic typing?
        naasking 8y ago
        > The article's point is that static and dynamic types are fundamentally unrelated to each other Not unrelated. You can embed dynamic types into a statically typed language, but not vice versa. Formerly dynamically typed languages that pull in static types, like Racket or TypeScript, become statically typed languages with embedded dynamic types. > There's no way to enforce that the JS you write today will be statically compatible with the libraries and browsers that it touches tomorrow This has nothing to do with dynamic types but with standardisation. C# is a language that is considerably different from its first release, and yet v1.0 C# still compiles on the latest compiler. The converse is not true, for either JS or C#. Dynamic types don't help with this problem. > The web has JS which must coexist with arbitrary other JS, running on many different browsers with many more versions. How could you possibly build this without dynamic typing? How do all the arbitrary programs on your computer coexist? The programs that interact do so via protocols or standard interfaces, and the ones that don't interact are isolated. This is no different than any other software.
- dllthomas 8y ago
  > dynamic typing is a way to defer until runtime typing aspects of the program's implementation That's more of a "how", where the bit you quoted seemed to be speaking to "why", IMO.
msla 8y ago
>> That “dynamic types” are, at their core, there to make unit testing less tedious, and are a tool for finding bugs. To the extent this is true, it's true because modern dynamic type systems are fairly strong. They enforce a contract about what operations are valid on a given type, and you can't usually get out of the contract. If you can cast in Python like you can cast in C, I don't know about it. Part of the problem is that we've lost a whole quadrant of languages in the static-dynamic weak-strong graph: Weak dynamic typing is nonexistent these days. We used to have it. B and Bliss were both weakly dynamically typed languages. Extremely so, in that they only had one datatype: The machine word. Since literally any operation was valid to perform on a machine word, there was no way for the type system to disallow anything, so it faded into irrelevance. Much like Bliss, in fact. That's taking it to an extreme, shoving the "weak" part of weakly-typed so far that the language is untyped, like assembly language is usually regarded as being.
- saghm 8y ago
  > Weak dynamic typing is nonexistent these days Is JavaScript not considered to be at least partially on the weak side of the spectrum? Things like using the `+` operator on arrays and objects and getting back numbers and integers seems to be to be weak typing.
  - michaelsbradley 8y ago
    JS facilities such as `typeof`, `instanceof`, `Array.isArray`, and built-in support for protocol checking (e.g. `Symbol.iterator`), and many related runtime facilities — despite their warts and limitations — place the language's dynamic typing in the strong camp.
    - DonaldPShimoda 8y ago
      I don't think the presence of these facilities grants a type system a "strong" classification. None of them actually enforce anything on their own — they're just functions and expressions that are provided to the programmer to implement their own dynamic type-checking via introspection/reflection. They do not, on their own, constitute a strong type system. Python is strongly typed because you cannot use a value of type X in a position where a value of type Y is expected. But Python doesn't check in advance — it just tries to go and do the thing. The trick to this is that Python's type system is actually structural instead of nominal; it doesn't care what the name of anything is, so long as it's got the right fields. (This is where we get "duck typing" from.) But you can't, for example, have Python do `"3" + 2`. A runtime error will result, because the language does not perform any implicit coercions. JS is different. There are some native implicit coercions from certain types to other types. The presence of these makes JS's type system weaker than Python's, so in general I see it grouped as "weakly typed".
DiseasedBadger 8y ago
Maybe I agree? To me, the purpose of those proofs, is to tell the compiler about all the programs I'm not writing. So that it doesn't emit them. Also: documentation.
VectorLock 8y ago
"Dynamic types are, at their core, there to remove the incredible tedium of things like generics or templated types."
- jimmaswell 8y ago
  I've never felt like templated types or generics are tedious.
  - viraptor 8y ago
    Considering the time when it was written, it could mean for example Java's ridiculously long generic declarations which couldn't be inferred or aliased. Things are much better and more ergonomic these days. Specific example - some languages will allow you to do: fun f(x: int): // return type inferred var foo = something(x) return foo While others need (including type erasure getting in the way): Complete<Version<Of<Generic, Foo>>>> f(int x) { Complete<Version<Of<Generic, Foo>>>> foo = (Complete<Version<Of<Generic, Foo>>>>) something(x); return foo; }
    - dvlsg 8y ago
      I agree, I quite enjoy them in TypeScript where I rely heavily on inference. I suppose it helps that the types aren't strictly required too, so you can side-step them if necessary.
    - jimmaswell 8y ago
      Type erasure was one of the worst decisions in Java, yeah. Generics and working with types in general is great in C#.
      - zzygan 8y ago
        Disagree. Type erasure is actually one of th best possible decisions made by the java designers. Languages that have higher kinded types (Haskell, Scala)are virtually impossible to implement without type erasure. This is why the .net runtime doesn’t have languages with HKT
StefanKarpinski 8y ago
Doesn’t hold water, imo. If dynamic and static typing were really independent concepts, then why are languages only one or the other, never both? I explained my take on dynamic versus static typing here: https://stackoverflow.com/a/28096079 https://stackoverflow.com/a/28096079 > The primary difference between static and dynamic languages, in my view, is this: in static languages, expressions have types; in dynamic languages, values have types. Read the rest of the answer for more details in the context of Julia, which, as a dynamic language with a sophisticated type system, really crystallizes the distinction.
- andrewflnr 8y ago
  > in static languages, expressions have types; in dynamic languages, values have types This kind of agrees with OP in practical terms, despite using opposite terminology. A type applied to an expression (syntax) is expressed as a proof about that syntax, and a type of a value at runtime is expressed in code that can safely crash in the face of an ill-typed operation. They both constrain program behavior, but do it with such radically different mechanisms that it's easy to argue they're fundamentally different. It depends on whether "fundamental" should be about mechanism or purpose. Let us know when you've solved that problem. :) Julia's type inference can be seen as finding proofs of the properties of certain expressions and, if it finds them, using them to optimize the dynamic typing code, basically eliminating dead branches for type checks that can't fail. I'm tempted to think of languages with nominal subtyping as being hybrids as well: the base class is the static type, and the runtime class is the dynamic type.
- sgeisenh 8y ago
  Who said languages were only ever or the other? All languages have some notion of static types and dynamic types. They're most easily bucketed by whether they consider more than one type. C is statically multityped but dynamically unityped. Python is statically unityped but dynamically multityped. Haskell, since it uses lazy evaluation, is statically multityped and dynamically multityped. The main issue with static unityping is that insufficient testing can easily lead to type errors in production (or worse). And static multitypes help static analysis tools reason about code more easily. Introducing a new type that is intended for use in a specific context that can easily be tracked is tremendously useful when programming at scale.
deleted 8y ago
[deleted]
namelosw 8y ago
> That “static types” are, at their core a tool for writing and maintaining computer-checked proofs about code > That “dynamic types” are, at their core, there to make unit testing less tedious, and are a tool for finding bugs. They are not rival. Imagine a gradual typing design, it has a statically typed system, but it won't stop you from running it. The type errors would only be suggested in IDEs and stop building on CI environment but you can run it anyway. Then you can have both checked proofs and debugging advantages. (Dialyzer for Erlang is an example but there could be more strict typing) Another similar topic is 'compiled' and 'interpreted', instead of static and dynamic types. 'Compiled' is runtime favored because the code was compiled is ready to be executed a lot of times, while 'interpreted' was executed once on demand because you may change your code at any time, so there's no point compile it for one person. Plus source code is much easier to debug than byte code. It would be interesting to see languages could have solid static/dynamic/compiled/interpreted at the same time. Elixir/TypeScript/F#, etc. are good examples but this idea can definitely go further.

draw_down 8y ago

> ... “dynamic types” are, at their core, there to make unit testing less tedious, and are a tool for finding bugs. I don't think this is a good description of dynamic typing. I'd probably go with something more like, dynamic typing is a way to defer until runtime typing aspects of the program's implementation. I suppose dynamic typing does make unit testing easier, among other things, but it feels wrong to say it's "for" that. A car is for getting one or more people from point A to B. It also has a radio, but a car is not "for" listening to the radio.

naasking 8y ago
> I suppose dynamic typing does make unit testing easier, among other things, but it feels wrong to say it's "for" that. The summary is trying to say that that's dynamic typing's primary advantage. Any other advantage you'd care to ascribe to dynamic typing is not intrinsic to dynamic typing itself.
- ridiculous_fish 8y ago
  The whole article seems concerned with the testability and bug-finding nature of types. But the main strength of dynamic types is the ability to defer decisions until runtime. JS isn't dynamically typed to make testing easier. JS uses dynamic types because you couldn't build the web any other way.
  - naasking 8y ago
    > But the main strength of dynamic types is the ability to defer decisions until runtime. That's not a strength. Deferring until runtime only that which must be deferred is a strength, but that's not one exhibited by dynamically typed languages. It is one that's available to statically typed languages though, like C# and now even Haskell has a deferred typing mode. > JS uses dynamic types because you couldn't build the web any other way. That's patently false. The whole engine running every browser is statically typed. There are libraries for working with the full DOM in HTML documents for Java, C# and other typed languages.
    - ridiculous_fish 8y ago
      Obviously the ability to defer decisions to runtime is a strength - how could you possibly dispute that? And yes statically typed languages have this strength if they use dynamic types. The article's point is that static and dynamic types are fundamentally unrelated to each other. Many languages can and do use both. When you make a web page you have no idea what "only must" be deferred. There's no way to enforce that the JS you write today will be statically compatible with the libraries and browsers that it touches tomorrow. That's why JS uses dynamic types. > That's patently false. The whole engine running every browser is statically typed My point is not about building web browsers, it is about building the web. The web has JS which must coexist with arbitrary other JS, running on many different browsers with many more versions. How could you possibly build this without dynamic typing?
      - naasking 8y ago
        > The article's point is that static and dynamic types are fundamentally unrelated to each other Not unrelated. You can embed dynamic types into a statically typed language, but not vice versa. Formerly dynamically typed languages that pull in static types, like Racket or TypeScript, become statically typed languages with embedded dynamic types. > There's no way to enforce that the JS you write today will be statically compatible with the libraries and browsers that it touches tomorrow This has nothing to do with dynamic types but with standardisation. C# is a language that is considerably different from its first release, and yet v1.0 C# still compiles on the latest compiler. The converse is not true, for either JS or C#. Dynamic types don't help with this problem. > The web has JS which must coexist with arbitrary other JS, running on many different browsers with many more versions. How could you possibly build this without dynamic typing? How do all the arbitrary programs on your computer coexist? The programs that interact do so via protocols or standard interfaces, and the ones that don't interact are isolated. This is no different than any other software.
dllthomas 8y ago
> dynamic typing is a way to defer until runtime typing aspects of the program's implementation That's more of a "how", where the bit you quoted seemed to be speaking to "why", IMO.

msla 8y ago

>> That “dynamic types” are, at their core, there to make unit testing less tedious, and are a tool for finding bugs. To the extent this is true, it's true because modern dynamic type systems are fairly strong. They enforce a contract about what operations are valid on a given type, and you can't usually get out of the contract. If you can cast in Python like you can cast in C, I don't know about it. Part of the problem is that we've lost a whole quadrant of languages in the static-dynamic weak-strong graph: Weak dynamic typing is nonexistent these days. We used to have it. B and Bliss were both weakly dynamically typed languages. Extremely so, in that they only had one datatype: The machine word. Since literally any operation was valid to perform on a machine word, there was no way for the type system to disallow anything, so it faded into irrelevance. Much like Bliss, in fact. That's taking it to an extreme, shoving the "weak" part of weakly-typed so far that the language is untyped, like assembly language is usually regarded as being.

saghm 8y ago
> Weak dynamic typing is nonexistent these days Is JavaScript not considered to be at least partially on the weak side of the spectrum? Things like using the `+` operator on arrays and objects and getting back numbers and integers seems to be to be weak typing.
- michaelsbradley 8y ago
  JS facilities such as `typeof`, `instanceof`, `Array.isArray`, and built-in support for protocol checking (e.g. `Symbol.iterator`), and many related runtime facilities — despite their warts and limitations — place the language's dynamic typing in the strong camp.
  - DonaldPShimoda 8y ago
    I don't think the presence of these facilities grants a type system a "strong" classification. None of them actually enforce anything on their own — they're just functions and expressions that are provided to the programmer to implement their own dynamic type-checking via introspection/reflection. They do not, on their own, constitute a strong type system. Python is strongly typed because you cannot use a value of type X in a position where a value of type Y is expected. But Python doesn't check in advance — it just tries to go and do the thing. The trick to this is that Python's type system is actually structural instead of nominal; it doesn't care what the name of anything is, so long as it's got the right fields. (This is where we get "duck typing" from.) But you can't, for example, have Python do `"3" + 2`. A runtime error will result, because the language does not perform any implicit coercions. JS is different. There are some native implicit coercions from certain types to other types. The presence of these makes JS's type system weaker than Python's, so in general I see it grouped as "weakly typed".

DiseasedBadger 8y ago

Maybe I agree? To me, the purpose of those proofs, is to tell the compiler about all the programs I'm not writing. So that it doesn't emit them. Also: documentation.

VectorLock 8y ago

"Dynamic types are, at their core, there to remove the incredible tedium of things like generics or templated types."

jimmaswell 8y ago
I've never felt like templated types or generics are tedious.
- viraptor 8y ago
  Considering the time when it was written, it could mean for example Java's ridiculously long generic declarations which couldn't be inferred or aliased. Things are much better and more ergonomic these days. Specific example - some languages will allow you to do: fun f(x: int): // return type inferred var foo = something(x) return foo While others need (including type erasure getting in the way): Complete<Version<Of<Generic, Foo>>>> f(int x) { Complete<Version<Of<Generic, Foo>>>> foo = (Complete<Version<Of<Generic, Foo>>>>) something(x); return foo; }
  - dvlsg 8y ago
    I agree, I quite enjoy them in TypeScript where I rely heavily on inference. I suppose it helps that the types aren't strictly required too, so you can side-step them if necessary.
  - jimmaswell 8y ago
    Type erasure was one of the worst decisions in Java, yeah. Generics and working with types in general is great in C#.
    - zzygan 8y ago
      Disagree. Type erasure is actually one of th best possible decisions made by the java designers. Languages that have higher kinded types (Haskell, Scala)are virtually impossible to implement without type erasure. This is why the .net runtime doesn’t have languages with HKT

StefanKarpinski 8y ago

Doesn’t hold water, imo. If dynamic and static typing were really independent concepts, then why are languages only one or the other, never both? I explained my take on dynamic versus static typing here: https://stackoverflow.com/a/28096079 https://stackoverflow.com/a/28096079 > The primary difference between static and dynamic languages, in my view, is this: in static languages, expressions have types; in dynamic languages, values have types. Read the rest of the answer for more details in the context of Julia, which, as a dynamic language with a sophisticated type system, really crystallizes the distinction.

andrewflnr 8y ago
> in static languages, expressions have types; in dynamic languages, values have types This kind of agrees with OP in practical terms, despite using opposite terminology. A type applied to an expression (syntax) is expressed as a proof about that syntax, and a type of a value at runtime is expressed in code that can safely crash in the face of an ill-typed operation. They both constrain program behavior, but do it with such radically different mechanisms that it's easy to argue they're fundamentally different. It depends on whether "fundamental" should be about mechanism or purpose. Let us know when you've solved that problem. :) Julia's type inference can be seen as finding proofs of the properties of certain expressions and, if it finds them, using them to optimize the dynamic typing code, basically eliminating dead branches for type checks that can't fail. I'm tempted to think of languages with nominal subtyping as being hybrids as well: the base class is the static type, and the runtime class is the dynamic type.
sgeisenh 8y ago
Who said languages were only ever or the other? All languages have some notion of static types and dynamic types. They're most easily bucketed by whether they consider more than one type. C is statically multityped but dynamically unityped. Python is statically unityped but dynamically multityped. Haskell, since it uses lazy evaluation, is statically multityped and dynamically multityped. The main issue with static unityping is that insufficient testing can easily lead to type errors in production (or worse). And static multitypes help static analysis tools reason about code more easily. Introducing a new type that is intended for use in a specific context that can easily be tracked is tremendously useful when programming at scale.

deleted 8y ago

[deleted]

namelosw 8y ago

> That “static types” are, at their core a tool for writing and maintaining computer-checked proofs about code > That “dynamic types” are, at their core, there to make unit testing less tedious, and are a tool for finding bugs. They are not rival. Imagine a gradual typing design, it has a statically typed system, but it won't stop you from running it. The type errors would only be suggested in IDEs and stop building on CI environment but you can run it anyway. Then you can have both checked proofs and debugging advantages. (Dialyzer for Erlang is an example but there could be more strict typing) Another similar topic is 'compiled' and 'interpreted', instead of static and dynamic types. 'Compiled' is runtime favored because the code was compiled is ready to be executed a lot of times, while 'interpreted' was executed once on demand because you may change your code at any time, so there's no point compile it for one person. Plus source code is much easier to debug than byte code. It would be interesting to see languages could have solid static/dynamic/compiled/interpreted at the same time. Elixir/TypeScript/F#, etc. are good examples but this idea can definitely go further.