4 ms·

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 ty

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.
        sds2 9y ago
        > Having a single static type system that captures all differences across all versions of all browsers is not realistic. Why? Standards and abstractions are useful. > 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. At that case your program's behaviour may become inconsistent > You want to type check with the actual runtime environment, not just a static guess at it. That's not typechecking and there's no guarantee that your program will work with dynamic typing if the API changes. > I guess by "graceful," not segfaulting would be a good start. Is runtime type error better? If the type of your value changes and your assumption was false about the type then it can fail anyway with an incorrect function call.
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.

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.
      - sds2 9y ago
        > Having a single static type system that captures all differences across all versions of all browsers is not realistic. Why? Standards and abstractions are useful. > 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. At that case your program's behaviour may become inconsistent > You want to type check with the actual runtime environment, not just a static guess at it. That's not typechecking and there's no guarantee that your program will work with dynamic typing if the API changes. > I guess by "graceful," not segfaulting would be a good start. Is runtime type error better? If the type of your value changes and your assumption was false about the type then it can fail anyway with an incorrect function call.

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.