6 ms·

Static Typing Where Possible, Dynamic Typing When Needed (2004) [pdf]

25 points by jasim 9y ago

sgt101 9y ago
This reads like the Julia manual!
jnbiche 9y ago
Yeah, it was pretty clear from the outset that the author(s) had a biased view against static typing when they describe static type "fanatics" versus dynamic type "advocates", and go on to discuss all the ways static types are unfeasible whereas dynamic types are "indispensable". I enjoy programming in Python and JavaScript sometimes, but dynamic typing is never "needed". Furthermore, no static type aficionado that I know would go so far as to say "well-typed programs cannot go wrong", as this paper claims we say. However, a good compiler for a static-typed language can be a wonderful tool and ally for programmers who are serious about building robust programs. To take just one example, if I can get an OCaml program to compile, it's extraordinarily rare for there to be a runtime problem to occur that is not related to a conceptual or algorithmic error. Careless errors just aren't an issue when I use OCaml, Rust, etc.
- KMag 9y ago
  I'm a fan of static typing and I only have a cursory understanding of Godel's incompleteness theoroms, but > but dynamic typing is never "needed". my understanding is that it's not possible to construct a single static type system that simultaneously accepts all correctly typed programs and rejects all incorrectly typed programs. In practice, most sound static type systems minimize the corner cases where they reject correctly typed programs, and provide an escape hatch for subverting the type checker if necessary. The presence of the escape hatch is basically an admission that dynamic typing is (rarely) necessary.
  - jnbiche 9y ago
    Yes, it's not possible to construct a static type system that accepts all correctly-typed programs. They only accept correctly-typed programs within their type system. So just because you can't devise a type system that accepts all correctly-typed programs doesn't mean that a statically-typed language can't create equivalents to any dynamically-typed program, assuming it's Turing complete. That's a misconception. What falls under correctly-typed within most modern type systems is more than enough to write expressive programs. In fact, sometimes a static type system can be even more expressive than even the most expressive dynamic one (as is the case with Haskell, for example). As some evidence for this, I assert that one can re-create any dynamic type system within a Haskell program, using simple algebraic data types. That's what I meant about dynamic typing not being needed. Yes, even languages like Haskell have runtime typing "escape hatches" but they're never necessary except for use with FFIs (ie, other languages) and are definitely a major code smell if you use them for normal coding. They're just not necessary.
    - ridiculous_fish 9y ago
      What do you do about runtime environments that may diverge from the static environment? For example, your code may typecheck in the browser you tested, but it has to run in other browsers which have differences in their APIs. How would you gracefully handle that without dynamic types?
      - Retra 9y ago
        If the APIs are different, they are differently typed. You still don't need dynamic types, you need to correctly account for both APIs. Doing it gracefully requires that you say what 'graceful' means in this context. It may or may not mean doing it correctly.
        ridiculous_fish 9y ago
        Having a single static type system that captures all differences across all versions of all browsers is not realistic. But even if it were, there's a bigger problem: static type checking happens too early. The browser can rev and change its APIs after your static type checking is performed. You want to type check with the actual runtime environment, not just a static guess at it. I guess by "graceful," not segfaulting would be a good start.
- kazinator 9y ago
  A good compiler for a dynamic language can also be a wonderful tool and ally.
- yawaramin 9y ago
  Actually, my reading is that they are ultimately pretty set on static typing and want to use a strong static typing base and build in some dynamic components: Static typing is a powerful tool to help programmers express their assumptions about the problem they are trying to solve and allows them to write more concise and correct code. Dealing with uncertain assumptions, dynamism and (unexepected) change is becoming increasingly important in a loosely couple [sic] distributed world. Where they go wrong is that they are lax in their understanding of 'a well-typed program cannot go wrong' (at runtime). They use the example of reading query resultsets, but those resultset reader methods are wrongly typed because they don't account for the possibility of error. So that's really a strawman. But it's interesting to see their idea about what essentially became Scala's (and potentially OCaml's) typeclass machinery (using implicit witnesses). I guess a lot of people were thinking about typeclasses and implicits around that time.
sds2 9y ago
> Requiring explicit type declarations is usually unnecessary and always a nuisance. Except at function declarations and similar - they help to make the code more readable. It's not feasible to dig in code where the only clue about the nature of the input and output in a function are variable names. > Static typing provides a false sense of safety, since it can only prove the absence of certain errors statically. This sentence contradicts itself: if it proves the absence of certain errors, doesn't it provide a certain level of safety? Also, it seems like the author never heard about substructural and dependent typing... > Static typing fanatics try to make us believe that “well-typed programs cannot go wrong”. While this certainly sounds im-pressive, it is a rather vacuous statement. Static typechecking is a compile-time abstraction of the runtime behavior of your program, and hence it is necessarily only partially sound and incomplete. And dynamic typing fanatics want us to believe that the only thing we need is unit tests... Modern, statically and strongly typed programming languages are capable of making us forget many common errors like data races, incorrect resource management etc. The authors enumerate what "us" - the "fanatics" state about static types but what does dynamic typing gives us besides uncertainty? And how could they question the documentational value of static types? The authors of this "research" paper should do more research about contemporary PLT because it seems like they've only programmed in 10-20 years old OOP languages. Also, what is the case for dynamic typing in this paper? I'm really curious because it feels like they're just biased towards dynamic typing.
jlarocco 9y ago
The argument over static and dynamic typing is so boring at this point. It's semi-intellectual "bike shedding". Practically speaking it doesn't make much difference one way or the other. I wish the industry as a whole would get over it and focus on bigger issues.
- ridiculous_fish 9y ago
  It matters a lot! The fact that ObjC, Java, and JS have dynamic type system is what enables iOS, Android, and web browsers to be revved independently from the apps that use them. This is a key feature that languages without dynamic types cannot provide.
  - yoklov 9y ago
    JS is the only one of those that has dynamic typing, at least by the conventional meaning of the term.
    - ridiculous_fish 9y ago
      Do you mean it's the only one without static types? All three are dynamically typed to some degree. For example, in ObjC, messages dispatch on the dynamic type of the object.
      - sds2 9y ago
        Both Objective-C and Java are statically and strongly typed. What you're thinking about is probably a runtime-reflection mechanism. The JVM, java's host is capable of supporting dynamic languages through 'invokevirtual' but it doesn't make java dynamically typed.
mannykannot 9y ago
> Static typing provides a false sense of safety, since it can only prove the absence of certain errors statically. That is as blatant a straw man as I have seen recently. I have never met someone who mistook static types for a guarantee of correctness, though I have met several people who did not understand why testing to 100% statement coverage does not do that. The authors would be well-advised to remove this sort of thing if they want to be taken seriously, and in general, striving to "do our best to make it provocative" is not an effective way to influence people, no matter how smart it makes you feel.
- astrange 9y ago
  I constantly see people discuss Haskell as if it prevented you from writing incorrect programs. But in fact static typing as it’s usually implemented does nothing for numeric programs/math errors. It won’t even catch dividing by 0. Related: saying a program is correct because it’s been “security audited” (someone read the source once) or “formally verified” (someone wrote the program twice and didn’t make any typos).
  - mannykannot 9y ago
    Your dismissive characterizations of security auditing and formal verification are way off the mark.
rajangdavis 9y ago
Quick question: is it enough to create guards/checks in languages like Ruby or Javascript to make sure that a parameter that is passed in is the type you expect? I try to set default values in the method/function declarations to at least return an empty set if I can live with it. Only time I have had a dynamic language do weird things is with PHP, but that was due to my lack of understanding of how PHP handles empty strings.
- always_good 9y ago
  One problem with runtime checks is that they of course only work at runtime but you also must manually assert against them. A bulk of your test suite now exists just to execute runtime paths through your code to trigger your guards at all. Then your tests often have to duplicate the very assertions that you already specified in your guards. Another problem is that your runtime guards are often ad-hoc and can drift from your data model, turning into debt that you need to manually reevaluate and clean up. In my experience, there's nothing quite so permanent as a defensive nil guard that everyone is too timid to remove. But it's not clear what you mean by "is it enough". I definitely use runtime asserts in dynamically-typed languages like Javascript to try and fail as fast as possible in critical functions.
  - rajangdavis 9y ago
    I meant "enough" as to ask "do I need to do more than writing a check?". You do bring up a good point with testing (which I don't always do, but I try to at least do runtime checks). I follow you on the data model part. I think that's where a test framework is super handy.

25 points by jasim 9y ago

This reads like the Julia manual!

Yeah, it was pretty clear from the outset that the author(s) had a biased view against static typing when they describe static type "fanatics" versus dynamic type "advocates", and go on to discuss all the ways static types are unfeasible whereas dynamic types are "indispensable". I enjoy programming in Python and JavaScript sometimes, but dynamic typing is never "needed". Furthermore, no static type aficionado that I know would go so far as to say "well-typed programs cannot go wrong", as this paper claims we say. However, a good compiler for a static-typed language can be a wonderful tool and ally for programmers who are serious about building robust programs. To take just one example, if I can get an OCaml program to compile, it's extraordinarily rare for there to be a runtime problem to occur that is not related to a conceptual or algorithmic error. Careless errors just aren't an issue when I use OCaml, Rust, etc.

KMag 9y ago
I'm a fan of static typing and I only have a cursory understanding of Godel's incompleteness theoroms, but > but dynamic typing is never "needed". my understanding is that it's not possible to construct a single static type system that simultaneously accepts all correctly typed programs and rejects all incorrectly typed programs. In practice, most sound static type systems minimize the corner cases where they reject correctly typed programs, and provide an escape hatch for subverting the type checker if necessary. The presence of the escape hatch is basically an admission that dynamic typing is (rarely) necessary.
- jnbiche 9y ago
  Yes, it's not possible to construct a static type system that accepts all correctly-typed programs. They only accept correctly-typed programs within their type system. So just because you can't devise a type system that accepts all correctly-typed programs doesn't mean that a statically-typed language can't create equivalents to any dynamically-typed program, assuming it's Turing complete. That's a misconception. What falls under correctly-typed within most modern type systems is more than enough to write expressive programs. In fact, sometimes a static type system can be even more expressive than even the most expressive dynamic one (as is the case with Haskell, for example). As some evidence for this, I assert that one can re-create any dynamic type system within a Haskell program, using simple algebraic data types. That's what I meant about dynamic typing not being needed. Yes, even languages like Haskell have runtime typing "escape hatches" but they're never necessary except for use with FFIs (ie, other languages) and are definitely a major code smell if you use them for normal coding. They're just not necessary.
  - ridiculous_fish 9y ago
    What do you do about runtime environments that may diverge from the static environment? For example, your code may typecheck in the browser you tested, but it has to run in other browsers which have differences in their APIs. How would you gracefully handle that without dynamic types?
    - Retra 9y ago
      If the APIs are different, they are differently typed. You still don't need dynamic types, you need to correctly account for both APIs. Doing it gracefully requires that you say what 'graceful' means in this context. It may or may not mean doing it correctly.
      - ridiculous_fish 9y ago
        Having a single static type system that captures all differences across all versions of all browsers is not realistic. But even if it were, there's a bigger problem: static type checking happens too early. The browser can rev and change its APIs after your static type checking is performed. You want to type check with the actual runtime environment, not just a static guess at it. I guess by "graceful," not segfaulting would be a good start.
kazinator 9y ago
A good compiler for a dynamic language can also be a wonderful tool and ally.
yawaramin 9y ago
Actually, my reading is that they are ultimately pretty set on static typing and want to use a strong static typing base and build in some dynamic components: Static typing is a powerful tool to help programmers express their assumptions about the problem they are trying to solve and allows them to write more concise and correct code. Dealing with uncertain assumptions, dynamism and (unexepected) change is becoming increasingly important in a loosely couple [sic] distributed world. Where they go wrong is that they are lax in their understanding of 'a well-typed program cannot go wrong' (at runtime). They use the example of reading query resultsets, but those resultset reader methods are wrongly typed because they don't account for the possibility of error. So that's really a strawman. But it's interesting to see their idea about what essentially became Scala's (and potentially OCaml's) typeclass machinery (using implicit witnesses). I guess a lot of people were thinking about typeclasses and implicits around that time.

sds2 9y ago

> Requiring explicit type declarations is usually unnecessary and always a nuisance. Except at function declarations and similar - they help to make the code more readable. It's not feasible to dig in code where the only clue about the nature of the input and output in a function are variable names. > Static typing provides a false sense of safety, since it can only prove the absence of certain errors statically. This sentence contradicts itself: if it proves the absence of certain errors, doesn't it provide a certain level of safety? Also, it seems like the author never heard about substructural and dependent typing... > Static typing fanatics try to make us believe that “well-typed programs cannot go wrong”. While this certainly sounds im-pressive, it is a rather vacuous statement. Static typechecking is a compile-time abstraction of the runtime behavior of your program, and hence it is necessarily only partially sound and incomplete. And dynamic typing fanatics want us to believe that the only thing we need is unit tests... Modern, statically and strongly typed programming languages are capable of making us forget many common errors like data races, incorrect resource management etc. The authors enumerate what "us" - the "fanatics" state about static types but what does dynamic typing gives us besides uncertainty? And how could they question the documentational value of static types? The authors of this "research" paper should do more research about contemporary PLT because it seems like they've only programmed in 10-20 years old OOP languages. Also, what is the case for dynamic typing in this paper? I'm really curious because it feels like they're just biased towards dynamic typing.

jlarocco 9y ago

The argument over static and dynamic typing is so boring at this point. It's semi-intellectual "bike shedding". Practically speaking it doesn't make much difference one way or the other. I wish the industry as a whole would get over it and focus on bigger issues.

ridiculous_fish 9y ago
It matters a lot! The fact that ObjC, Java, and JS have dynamic type system is what enables iOS, Android, and web browsers to be revved independently from the apps that use them. This is a key feature that languages without dynamic types cannot provide.
- yoklov 9y ago
  JS is the only one of those that has dynamic typing, at least by the conventional meaning of the term.
  - ridiculous_fish 9y ago
    Do you mean it's the only one without static types? All three are dynamically typed to some degree. For example, in ObjC, messages dispatch on the dynamic type of the object.
    - sds2 9y ago
      Both Objective-C and Java are statically and strongly typed. What you're thinking about is probably a runtime-reflection mechanism. The JVM, java's host is capable of supporting dynamic languages through 'invokevirtual' but it doesn't make java dynamically typed.

mannykannot 9y ago

> Static typing provides a false sense of safety, since it can only prove the absence of certain errors statically. That is as blatant a straw man as I have seen recently. I have never met someone who mistook static types for a guarantee of correctness, though I have met several people who did not understand why testing to 100% statement coverage does not do that. The authors would be well-advised to remove this sort of thing if they want to be taken seriously, and in general, striving to "do our best to make it provocative" is not an effective way to influence people, no matter how smart it makes you feel.

astrange 9y ago
I constantly see people discuss Haskell as if it prevented you from writing incorrect programs. But in fact static typing as it’s usually implemented does nothing for numeric programs/math errors. It won’t even catch dividing by 0. Related: saying a program is correct because it’s been “security audited” (someone read the source once) or “formally verified” (someone wrote the program twice and didn’t make any typos).
- mannykannot 9y ago
  Your dismissive characterizations of security auditing and formal verification are way off the mark.

rajangdavis 9y ago

Quick question: is it enough to create guards/checks in languages like Ruby or Javascript to make sure that a parameter that is passed in is the type you expect? I try to set default values in the method/function declarations to at least return an empty set if I can live with it. Only time I have had a dynamic language do weird things is with PHP, but that was due to my lack of understanding of how PHP handles empty strings.

always_good 9y ago
One problem with runtime checks is that they of course only work at runtime but you also must manually assert against them. A bulk of your test suite now exists just to execute runtime paths through your code to trigger your guards at all. Then your tests often have to duplicate the very assertions that you already specified in your guards. Another problem is that your runtime guards are often ad-hoc and can drift from your data model, turning into debt that you need to manually reevaluate and clean up. In my experience, there's nothing quite so permanent as a defensive nil guard that everyone is too timid to remove. But it's not clear what you mean by "is it enough". I definitely use runtime asserts in dynamically-typed languages like Javascript to try and fail as fast as possible in critical functions.
- rajangdavis 9y ago
  I meant "enough" as to ask "do I need to do more than writing a check?". You do bring up a good point with testing (which I don't always do, but I try to at least do runtime checks). I follow you on the data model part. I think that's where a test framework is super handy.