1. 26

  2. 5

    I find the biggest cases are limitations of specific static type systems rather than inherent to the concept. In particular, constructs like { foo: "blah", bar: 1} often have a perfectly good static type, it’s just difficult to express it given the limited state of record systems. Once I switched to Scala with lightweight case classes, a lot of the things I thought I needed dynamicity for in Python disappeared. Most of the remaining cases are covered by shapeless records (e.g. “this case class plus a UUID called "id"”), but the syntax is much more clunky than I’d like.

    When it comes to partiality, this is adequately solved by casts, which almost every static language offers - though again perhaps not with a syntax that’s as light as it should be. In practice most static language users tend to find themselves avoiding casts, I think rightly, but making them more available might help with onboarding dynamic language users if nothing else.

    1. 1

      I’ve never actually used Elm, but I believe their records are designed to deal with this phenomenon: http://elm-lang.org/docs/records.

    2. 3

      The benefits of the idioms discussed can be summarized as 1) less boilerplate code and less noise, which leads to 2) a ad-hoc DWIM approach to designing components. These factors lead to less friction while writing down “COMPUTER, I command you to do X!” I don’t think this sentiment is controversial, and identifying particular pain points in other languages is good for when you have to decide amongst them.

      That said, I personally prefer static languages simply because they fit my use cases more: 1) applications that chew through huge amounts of data, where feedback latency is important, and 2) toolsets that prefer to be integrated/interfaced through other low-level statically types languages.

      1. 3

        Hi @wcrichton, thanks for the post.

        That part about automatically inferring types of a heterogenous map in OCaml is incorrect. You can create constructors out of nowhere (polymorphic variants), but OCaml will never do this for you and declaring that is also completely typesafe with no runtime errors happening. Also, your link to Stackoverflow is broken (because I wanted to check out what made you conclude such a thing).

        1. 2

          Ah, that was a misleading edit, I’ve clarified the article text. Originally I had OCaml in the explicit sum type category with a note about polymorphic variants, but I realized that was similar to Ceylon so I moved it to the implicit sum type category without appropriately updating the pros/cons. Ultimately, I realized that a more nuanced description of the design space around sum types is warranted, which you can now find in the article (i.e. sum types can be broken down as named vs. anonymous, declared vs. inferred, and matched vs. casted).

          1. 1

            Very good, I think this is a nice improvement. I realize my original comment to a good article was unnecessarily grumpy, so I’ll just wish you a nice weekend instead now.

        2. 2

          Opened the blog and saw the box about how dynamic typed languages are easier to use (as in what people think).

          Dynamically typed languages don’t enforce any type checking and hence anything could happen. I love static typing and have never felt underpowered whilst using it.

          1. 13

            There’s a spectrum here. I’m guessing that when you use static typing, you’re probably not using SPARK, Dafny, or Liquid Haskell. Compare to them, most statlangs are pretty weak in what they can actually tell you. In those languages, you can also statically verify behavior, like “this procedure always terminates” or “this function is always called with a nonempty list and returns the same list, but sorted.”

            The problem is that they’re a lot harder to use. It’s the standard expressiveness vs legibility tradeoff here: the more valid expressions you can write in a language, the fewer properties they all share in common. Statically-typed languages have more expressiveness and less legibility than formally verifiable languages, and dynlangs have more expressiveness and less legibility than statlangs. In return for losing static typechecking, you get the ability to leverage the complete runtime language for defining types. For example, in Python you can define the type of all classes with an odd number of letters in their name, and in J you can define the obverse (quasi-inverse) of a function.

            I think most popular dynamics end up too expressive with not enough legibility. My justification is how rapidly gradual type-checkers are spreading. It implies that the parts of the dynlangs being used aren’t the bits that require the crazy expressivity dynamic typing gives you, so it’s worth adding legibility. But there’s still a lot space left to explore.

            1. 14

              Opposite experience here. I’ve worked with many kinds of statically typed languages, including Java, Haskell, and Scala for nearly a decade. I ultimately found that static typing introduces a lot of mental overhead in practice, and limits the way you’re able to express yourself. Many dynamic patterns such as Ring middleware become difficult in static languages. I’ve been working with Clojure about 8 years now, and I don’t miss types in the slightest. If I did, I would’ve gone back to a typed language a long time ago.

              Dynamic typing tends to be problematic in imperative/OO languages. One problem is that the data is mutable, and you pass things around by reference. Even if you knew the shape of the data originally, there’s no way to tell whether it’s been changed elsewhere via side effects. The other problem is that OO encourages proliferation of types in your code. Keeping track of that quickly gets out of hand.

              What I find to be of highest importance is the ability to reason about parts of the application in isolation, and types don’t provide much help in that regard. When you have shared mutable state, it becomes impossible to track it in your head as application size grows. Knowing the types of the data does not reduce the complexity of understanding how different parts of the application affect its overall state.

              My experience is that immutability plays a far bigger role than types in addressing this problem. Immutability as the default makes it natural to structure applications using independent components. This indirectly helps with the problem of tracking types in large applications as well. You don’t need to track types across your entire application, and you’re able to do local reasoning within the scope of each component. Meanwhile, you make bigger components by composing smaller ones together, and you only need to know the types at the level of composition which is the public API for the components.

              REPL driven development also plays a big role in the workflow. Any code I write, I evaluate in the REPL straight from the editor. The REPL has the full application state, so I have access to things like database connections, queues, etc. I can even connect to the REPL in production. So, say I’m writing a function to get some data from the database, I’ll write the code, and run it to see exactly the shape of the data that I have. Then I might write a function to transform it, and so on. At each step I know exactly what my data is and what my code is doing.

              Where I typically care about having a formalism is at component boundaries. Spec provides a much better way to do that than types. The main reason being that it focuses on ensuring semantic correctness. For example, consider a sort function. The types can tell me that I passed in a collection of a particular type and I got a collection of the same type back. However, what I really want to know is that the collection contains the same elements, and that they’re in order. This is difficult to express using most type systems out there, while trivial to do using Spec.

            2. 2

              Programmers mental model changes while he learns and is very flexible. Statically typed languages cannot match to this.

              Many statically typed languages still allow you to do really bad errors and botch it in numerous multiple ways despite their type system. Very classic example of this would be the whole C language. But it is not the only statically typed language ridden full of foxholes. For example, you may use variables before you’ve set their contents in some corner-case that the language designer did not manage to solve. Then you got a surprise null, despite that careful use of Maybe or nullable-property.

              Another example of this kind of failure would be the introduction of corruption bugs. Too many popular statically typed languages do not protect you from data corruption bugs when handling mutable data, and do not provide tools to protect your mutable data from corruption bugs.

              I think that dynamically typed languages are easier to use because they genuinely let you decide afterwards on some design problems that you face. They are polymorphic without work, and programmers who use them naturally produce more abstract code. I also think that you can prove dynamically typed programs correct, and you don’t need full type annotations for that which means it can still be dynamically typed after that.

              They are simply, just better programming languages.

              1. 4

                Most of these arguments are unrelated to static vs dynamic typing. It sounds like you’re arguing that dynamic languages are easier to quickly prototype ideas, however, which I agree with.

                1. 2

                  In such situations, I like to bring up Strongtalk and Shen w/ Sequent Calculus & Prolog. Both add typing to high-productivity, dynamic languages/environments.

              2. 1

                Somewhere out there, there is an exchange where Matthias Felleisen says something along the lines of dynamic languages allow a programmer to fruitfully apply two mutually incompatible, or at least hard to reconcile, typing disciplines to a program at once. I thought it was on Bob Harper’s blog, but I can’t find the source.