4 ms·

> And static typing is great, as long as it doesn't require you to type variables and anonymous or small utility functions/methods... eg. it sucks without infer

> And static typing is great, as long as it doesn't require you to type variables and anonymous or small utility functions/methods... eg. it sucks without inference! > Some languages work better with types, some don't gain much from them... When you have proper type inference (which has been around for literally decades), what advantages do dynamic languages really have? I don't see any significant benefits personally. If you you're having trouble justifying at compile type a property holds, more than likely you've got a bug that's going to bite you later.

yorwba 9y ago
When you're having trouble justifying at compile time that a property holds, it's not always because you don't know why it holds, but frequently a problem with the type system you have to write the justification in. Some type systems are so limited that you can't even express the conditions under which the property holds, let alone prove them. Others are powerful enough to prove anything, but that makes type inference intractable, because the inferencer might have to prove arbitrary theorems. The advantage of dynamically typed languages is that you are not glued to one specific proof language and don't have to provide proofs for trivial properties, or one-off programs you only need to run once. There are some type systems that attempt to provide similar benefits, e.g. success typing puts the burden of proof on the compiler which will only reject a program if it can prove that the program is incorrect [1]. But as far as I know, that approach has not been included in any mainstream programming languages. [1] https://arxiv.org/abs/1502.01278 https://arxiv.org/abs/1502.01278
- kazinator 9y ago
  > e.g. success typing puts the burden of proof on the compiler which will only reject a program if it can prove that the program is incorrect That describes any dynamic language that does type inference. Type is taken into account for diagnosis and better code, but not as an excuse for rejecting the program just because it isn't fully analyzed.
- seanwilson 9y ago
  > When you're having trouble justifying at compile time that a property holds, it's not always because you don't know why it holds, but frequently a problem with the type system you have to write the justification in. Do you have any realistic concrete examples of this? I find this happens very rarely myself (maybe once every few thousand lines of code) and just involves adding a small amount of code along the lines of "throw 'Unexpected error' // this should never happen because ...". > The advantage of dynamically typed languages is that you are not glued to one specific proof language and don't have to provide proofs for trivial properties, or one-off programs you only need to run once. For me, type errors for where you've mixed up e.g. string, number or object variables or where you've forgotten to check if a variable is null/undefined before you use it are incredibly common compared to the rare times the type system gets in your way. You would have to (and most wouldn't) write many automated tests to catch all those potential errors if you weren't using a type system for similar robustness. Throwing all that away because of the rare case the type system obstructs you doesn't make any sense to me. I still think if you're regularly writing code that is hard to justify to a mainstream type checker you're more than likely doing something very wrong and writing code that is hard for others to understand. I'd love to see a realistic counterexample.
  - yorwba 9y ago
    I did not intend to imply that I'm regularly writing code that's hard to justify to a type checker. In fact, most of the code I write is in statically typed languages (I'm not some kind of dynamic typing zealot), so I tend to avoid situations that could never typecheck before they occur. However, I like to use Python for small single-purpose utilities, and in those cases I don't even bother with the optional type annotations, let alone checking them with mypy. Since those programs are so simple that a handful of test cases is enough for 100% path coverage, if the program runs correctly on one case, it's almost guaranteed to run correctly for all others. (Similar to Haskell's "if it compiles, it runs".) Statically checking for type correctness would be pointless, because you can just run the program to find out. It then becomes quite natural to e.g. apply type-modifying transformations in-place, which most type checkers wouldn't allow, since they assume a single fixed type rather than a progression of different types during different stages. (You can get around that, of course, but it requires constantly recreating essentially identical objects to give them a new type.) For an example of a project (not written by me) where the type checker's rejection of a correctly working program precluded the use of a type checker, see http://www.oilshell.org/blog/2016/11/30.html http://www.oilshell.org/blog/2016/11/30.html
- denisw 9y ago
  > success typing puts the burden of proof on the compiler which will only reject a program if it can prove that the program is incorrect [1]. But as far as I know, that approach has not been included in any mainstream programming languages. Dialyzer, the optional static typing system that is of part of the Erlang distribution, is based on success typing. Here is an accessible introduction: http://learnyousomeerlang.com/dialyzer http://learnyousomeerlang.com/dialyzer
kazinator 9y ago
One benefit is a more robust execution model, in which objects know what type they are. Given a machine word and a RAM dump, I can tell you the type of the object in that word or the location that the word points to. I don't need to know the address of the piece of machine code which is manipulating that word, which, in turn, I don't need to correlate to the matching source code via debug info. Type inference is compatible with dynamism. Infer all you want. Optimize and diagnose, just don't strip type from my objects, please, and don't say I can't try running something because it wasn't completely checked.
nnq 9y ago
> When you have proper type inference [...] what advantages do dynamic languages really have? You can quickly prototype by repl-ing around half-working pieces of code until you get to something that you can conceptualize. Sometimes you start from "how to" knowledge, but you don't really have the "what is" knowledge. You "know how to make it work" but you don't yet have any idea of "what it actually does". You'll get to that stage, but you need a prototype you can play with in the meantime. Mathematicians have the hardest time groking this, so I give them the example of drawing an ellipse: let's say you start with a "working definition" of "an ellipse is that ovalishy thinggy that I get by dragging a pencil on a loop of string tied to two nails set at some distance". You know how to produce it, you want to play with it, but have no idea how to define it yet. A dynamic language gives you the higher level equivalent of being able to "draw the damn ellipse even if you have no idea what it is"... later you can look at the code for drawing the ellipse and extract from it that "aha, it is what you get by constraining the sum of distances from 2 points to be constant!". But some people (like me), are not very good at abstract thinking, so we need to play with half-formed stuff on screen, like "let's do this api call" and "do that and that to the returned data" and "pass it to the other thing" that "maybe someone forgot to document" and "see what it does"... and reverse engineer the abstractions from working code and maybe later properly generalize them. I've never seen a static language with a good interactive prototyping experience so far. Though I'm playing with OCaml/Reason now, and its REPL seems quite powerful, though the language is more verbose/pedantic than I'd like it...

yorwba 9y ago

When you're having trouble justifying at compile time that a property holds, it's not always because you don't know why it holds, but frequently a problem with the type system you have to write the justification in. Some type systems are so limited that you can't even express the conditions under which the property holds, let alone prove them. Others are powerful enough to prove anything, but that makes type inference intractable, because the inferencer might have to prove arbitrary theorems. The advantage of dynamically typed languages is that you are not glued to one specific proof language and don't have to provide proofs for trivial properties, or one-off programs you only need to run once. There are some type systems that attempt to provide similar benefits, e.g. success typing puts the burden of proof on the compiler which will only reject a program if it can prove that the program is incorrect [1]. But as far as I know, that approach has not been included in any mainstream programming languages. [1] https://arxiv.org/abs/1502.01278 https://arxiv.org/abs/1502.01278

kazinator 9y ago
> e.g. success typing puts the burden of proof on the compiler which will only reject a program if it can prove that the program is incorrect That describes any dynamic language that does type inference. Type is taken into account for diagnosis and better code, but not as an excuse for rejecting the program just because it isn't fully analyzed.
seanwilson 9y ago
> When you're having trouble justifying at compile time that a property holds, it's not always because you don't know why it holds, but frequently a problem with the type system you have to write the justification in. Do you have any realistic concrete examples of this? I find this happens very rarely myself (maybe once every few thousand lines of code) and just involves adding a small amount of code along the lines of "throw 'Unexpected error' // this should never happen because ...". > The advantage of dynamically typed languages is that you are not glued to one specific proof language and don't have to provide proofs for trivial properties, or one-off programs you only need to run once. For me, type errors for where you've mixed up e.g. string, number or object variables or where you've forgotten to check if a variable is null/undefined before you use it are incredibly common compared to the rare times the type system gets in your way. You would have to (and most wouldn't) write many automated tests to catch all those potential errors if you weren't using a type system for similar robustness. Throwing all that away because of the rare case the type system obstructs you doesn't make any sense to me. I still think if you're regularly writing code that is hard to justify to a mainstream type checker you're more than likely doing something very wrong and writing code that is hard for others to understand. I'd love to see a realistic counterexample.
- yorwba 9y ago
  I did not intend to imply that I'm regularly writing code that's hard to justify to a type checker. In fact, most of the code I write is in statically typed languages (I'm not some kind of dynamic typing zealot), so I tend to avoid situations that could never typecheck before they occur. However, I like to use Python for small single-purpose utilities, and in those cases I don't even bother with the optional type annotations, let alone checking them with mypy. Since those programs are so simple that a handful of test cases is enough for 100% path coverage, if the program runs correctly on one case, it's almost guaranteed to run correctly for all others. (Similar to Haskell's "if it compiles, it runs".) Statically checking for type correctness would be pointless, because you can just run the program to find out. It then becomes quite natural to e.g. apply type-modifying transformations in-place, which most type checkers wouldn't allow, since they assume a single fixed type rather than a progression of different types during different stages. (You can get around that, of course, but it requires constantly recreating essentially identical objects to give them a new type.) For an example of a project (not written by me) where the type checker's rejection of a correctly working program precluded the use of a type checker, see http://www.oilshell.org/blog/2016/11/30.html http://www.oilshell.org/blog/2016/11/30.html
denisw 9y ago
> success typing puts the burden of proof on the compiler which will only reject a program if it can prove that the program is incorrect [1]. But as far as I know, that approach has not been included in any mainstream programming languages. Dialyzer, the optional static typing system that is of part of the Erlang distribution, is based on success typing. Here is an accessible introduction: http://learnyousomeerlang.com/dialyzer http://learnyousomeerlang.com/dialyzer

kazinator 9y ago

One benefit is a more robust execution model, in which objects know what type they are. Given a machine word and a RAM dump, I can tell you the type of the object in that word or the location that the word points to. I don't need to know the address of the piece of machine code which is manipulating that word, which, in turn, I don't need to correlate to the matching source code via debug info. Type inference is compatible with dynamism. Infer all you want. Optimize and diagnose, just don't strip type from my objects, please, and don't say I can't try running something because it wasn't completely checked.

nnq 9y ago

> When you have proper type inference [...] what advantages do dynamic languages really have? You can quickly prototype by repl-ing around half-working pieces of code until you get to something that you can conceptualize. Sometimes you start from "how to" knowledge, but you don't really have the "what is" knowledge. You "know how to make it work" but you don't yet have any idea of "what it actually does". You'll get to that stage, but you need a prototype you can play with in the meantime. Mathematicians have the hardest time groking this, so I give them the example of drawing an ellipse: let's say you start with a "working definition" of "an ellipse is that ovalishy thinggy that I get by dragging a pencil on a loop of string tied to two nails set at some distance". You know how to produce it, you want to play with it, but have no idea how to define it yet. A dynamic language gives you the higher level equivalent of being able to "draw the damn ellipse even if you have no idea what it is"... later you can look at the code for drawing the ellipse and extract from it that "aha, it is what you get by constraining the sum of distances from 2 points to be constant!". But some people (like me), are not very good at abstract thinking, so we need to play with half-formed stuff on screen, like "let's do this api call" and "do that and that to the returned data" and "pass it to the other thing" that "maybe someone forgot to document" and "see what it does"... and reverse engineer the abstractions from working code and maybe later properly generalize them. I've never seen a static language with a good interactive prototyping experience so far. Though I'm playing with OCaml/Reason now, and its REPL seems quite powerful, though the language is more verbose/pedantic than I'd like it...