4 ms·

> People believe static typing catches bugs. People believe static typing helps document code. People believe static typing makes IDEs work better and therefor

> People believe static typing catches bugs. People believe static typing helps document code. People believe static typing makes IDEs work better and therefore save time, etc. BUT … those are all just beliefs not backed up by any data Yeah... no. It's backed up by data. Mathematics, even. Types enable safe automatic refactorings. Without types, refactorings can break your code if not supervised by humans.

jwdunne 11y ago
It's not that it can make just IDEs 'work better'. The compiler can work better with a great static type system. Haskell, for instance, is mind blowing. Perhaps the problem is that static typing is confused with how some languages implement it. It can, and has, been implemented such that it dramatically improves compilation, correctness, static analysis and documentation without making code horrendously verbose.
- vvanders 11y ago
  Yup, type inference really feels like the sweet spot to me. Nice code "feel" with the backing of a static type system.
- madflame991 11y ago
  > Haskell, for instance, is mind blowing. Mind blowing is the amount of output and obscurity of the error message you get from the type checker. It's harder to understand the error message than to debug the program if compiled "unsafely".
  - agumonkey 11y ago
    It's a threshold I guess. My formal proof teacher said he thinks in type checking unification all the time. To him a program is a proof tree construction. With time the way I approach code is also much more and abstract. You look at diagonal invariants more than code itself.
  - odonnellryan 11y ago
    This isn't true. It is hard to understand (definitely) if you're new to Haskell and what the error is actually saying. As you get more familiar the errors become more clear.
- PeCaN 11y ago
  Heck, Idris can in some cases write code for you based on solving the types you provided. Powerfully-typed languages also work much better for structured editing. http://docs.idris-lang.org/en/latest/tutorial/interactive.html#proofsearch http://docs.idris-lang.org/en/latest/tutorial/interactive.ht...
- ionforce 11y ago
  > Perhaps the problem is that static typing is confused with how some languages implement it. Most of the time what people hate with static languages is type annotations. What will blow their minds is a language that is both a) type safe and b) easy to type (i.e. what gives dynamic languages their flavor). Luckily we're getting to a point (Scala) where this is mainstream.
  - virtualwhys 11y ago
    As a Scala user I think the MLs have a leg up on Scala wrt to a & b. Scala can be quite concise but we do have to be explicit with type signatures, and that only increases as we go up the abstraction ladder. A strict Haskell with a decent module system, or a modern SML that borrows some nice-to-haves from Haskell and Scala would be my ideal language.
pekk 11y ago
With static types, refactorings can break your code if not supervised by humans. Dynamic typing doesn't mean there are no types, by the way.
- WatchDog 11y ago
  > With static types, refactorings can break your code if not supervised by humans. The opposite is true, with static typing your code is supervised by the compiler, with dynamic typing you need to rely on humans or runtime errors.
- viraptor 11y ago
  What do you consider a refactoring? By wikipedia it's "Code refactoring is the process of restructuring existing computer code – changing the factoring – without changing its external behavior." By definition if some operation breaks code, it's either not refactoring, or it's due to a bug. Have you got some examples for your issue? I'd say that with static typing you can apply refactoring and with with dynamic you can try and hope you applied refactoring (because everything about your variables could change at runtime).
  - incepted 11y ago
    I think the keyword you missed is "automated". You can refactor anything but refactoring can only be performed automatically and safely with types around. Without types, a human is required to verify that the tool didn't break the code with its refactoring, because it's just guessing at this point. With types, there is no guessing.
    - viraptor 11y ago
      This is what I'm saying. Which is not what the parent (pekk) was saying. Are you responding to the right comment?
    - cle 11y ago
      There is no guessing, there is just a false sense of security. I have seen plenty of bugs introduced by refactoring in static languages. Static typing cannot verify correct behavior. I sit on the fence in the dynamic vs. static typing debate, but I think the uncertainty of a dynamic language is often an advantage because you are much more likely to pay attention to the behavior of the system and not just the types. And at the end of the day, it's the behavior we're interested in, not the types! I've seen multiple times when bugs have been pushed to prod due to a false sense of security because "it compiled".
deleted 11y ago
[deleted]

jwdunne 11y ago

It's not that it can make just IDEs 'work better'. The compiler can work better with a great static type system. Haskell, for instance, is mind blowing. Perhaps the problem is that static typing is confused with how some languages implement it. It can, and has, been implemented such that it dramatically improves compilation, correctness, static analysis and documentation without making code horrendously verbose.

vvanders 11y ago
Yup, type inference really feels like the sweet spot to me. Nice code "feel" with the backing of a static type system.
madflame991 11y ago
> Haskell, for instance, is mind blowing. Mind blowing is the amount of output and obscurity of the error message you get from the type checker. It's harder to understand the error message than to debug the program if compiled "unsafely".
- agumonkey 11y ago
  It's a threshold I guess. My formal proof teacher said he thinks in type checking unification all the time. To him a program is a proof tree construction. With time the way I approach code is also much more and abstract. You look at diagonal invariants more than code itself.
- odonnellryan 11y ago
  This isn't true. It is hard to understand (definitely) if you're new to Haskell and what the error is actually saying. As you get more familiar the errors become more clear.
PeCaN 11y ago
Heck, Idris can in some cases write code for you based on solving the types you provided. Powerfully-typed languages also work much better for structured editing. http://docs.idris-lang.org/en/latest/tutorial/interactive.html#proofsearch http://docs.idris-lang.org/en/latest/tutorial/interactive.ht...
ionforce 11y ago
> Perhaps the problem is that static typing is confused with how some languages implement it. Most of the time what people hate with static languages is type annotations. What will blow their minds is a language that is both a) type safe and b) easy to type (i.e. what gives dynamic languages their flavor). Luckily we're getting to a point (Scala) where this is mainstream.
- virtualwhys 11y ago
  As a Scala user I think the MLs have a leg up on Scala wrt to a & b. Scala can be quite concise but we do have to be explicit with type signatures, and that only increases as we go up the abstraction ladder. A strict Haskell with a decent module system, or a modern SML that borrows some nice-to-haves from Haskell and Scala would be my ideal language.

pekk 11y ago

With static types, refactorings can break your code if not supervised by humans. Dynamic typing doesn't mean there are no types, by the way.

WatchDog 11y ago
> With static types, refactorings can break your code if not supervised by humans. The opposite is true, with static typing your code is supervised by the compiler, with dynamic typing you need to rely on humans or runtime errors.
viraptor 11y ago
What do you consider a refactoring? By wikipedia it's "Code refactoring is the process of restructuring existing computer code – changing the factoring – without changing its external behavior." By definition if some operation breaks code, it's either not refactoring, or it's due to a bug. Have you got some examples for your issue? I'd say that with static typing you can apply refactoring and with with dynamic you can try and hope you applied refactoring (because everything about your variables could change at runtime).
- incepted 11y ago
  I think the keyword you missed is "automated". You can refactor anything but refactoring can only be performed automatically and safely with types around. Without types, a human is required to verify that the tool didn't break the code with its refactoring, because it's just guessing at this point. With types, there is no guessing.
  - viraptor 11y ago
    This is what I'm saying. Which is not what the parent (pekk) was saying. Are you responding to the right comment?
  - cle 11y ago
    There is no guessing, there is just a false sense of security. I have seen plenty of bugs introduced by refactoring in static languages. Static typing cannot verify correct behavior. I sit on the fence in the dynamic vs. static typing debate, but I think the uncertainty of a dynamic language is often an advantage because you are much more likely to pay attention to the behavior of the system and not just the types. And at the end of the day, it's the behavior we're interested in, not the types! I've seen multiple times when bugs have been pushed to prod due to a false sense of security because "it compiled".

deleted 11y ago

[deleted]