1. 14
  1.  

  2. 5

    Defenders of dynamically typed languages sometimes counter that these pitfalls do not matter when runtime failures are mostly harmless. If you want to find errors in your program, just run the program!

    … We do?

    1. 2

      Gabriel qualified the statement (“sometimes”) and gives an example (Nix). Is it not a reasonable accusation? What else can one do with a dynamically typed program, except running it?

      1. 2

        An non exhaustive list:

        • unit tests against your code
        • property tests against your code
        • runtime type pattern matching
        • runtime type conditionals
        • contracts
        • other compile-time checks besides a type system
        • defensive coding (for instance, calling int(x) BEFORE opening a file handle, not after)

        I love type systems, and even more so I love compile time guarantees, but any static typing advocate should be able to speak about the value of typing as a trade-off against other techniques and paradigms. On the other hand, no advocate of dynamic typing would (or should, I suppose) claim that, in the absence of the tangible and often productivity-enhancing benefits of strong static typing, “just run the program” is an acceptable alternative.

        1. 2

          An non exhaustive list:

          unit tests against your code property tests against your code runtime type pattern matching runtime type conditionals contracts other compile-time checks besides a type system defensive coding (for instance, calling int(x) BEFORE opening a file handle, not after)

          All but one of these is a variant on running the code.

          ** EDIT ** Well, the formatting didn’t stay and I’m on mobile so I’m just going to leave this as is for now…

          1. 4

            All but one of these is a variant on running the code.

            In that sense, one can say that even compilation is just a variant on running the code.

            1. 2

              I disagree. The compiler, a linter, or another static analyzer is another program operating on your program.

              Though, I suppose you could argue the same about unit tests and property tests. I think the difference is that they exercise your code whereas your code may not execute with a compiler. Things get a bit weird with compile time execution/macros/whatever.

              I don’t feel completely satisfied with my response.

              1. 6

                A typed program is two programs at once; the type system’s annotations themselves form a second program which is intertwined with the original program’s shape. This second program is the one which is run by the type-checker, and this is what gives us Rice’s Theorem for type systems, where e.g. GHC has some extensions that allow for type-checking to be undecideable.

                This also justifies why static type systems cannot possibly replace runtime testing of some sort; in order to complete in a reasonable time, the typical type system must be very simple, because its expressions are evaluated by the type-checker.

                I waffled over whether to post this at the top or the bottom of the thread, since I feel that this fact is at odds with how the discussion progressed. After all, what else can one do with a statically-typed program (that is, a pair of interleaved programs where one is not Turing-complete and is either sound or conservative over the second program). except running it or running just the type-checker portion? Similarly, it is not just obvious that compilation is a variant on running the code, in that is is an evaluation of one entire layer of the program’s code which produces a residual single-layer program, but also that compilation must run the code.

                1. 2

                  A typed program is two programs at once; the type system’s annotations themselves form a second program which is intertwined with the original program’s shape. This second program is the one which is run by the type-checker…

                  Okay, I am reasonably convinced by this. My major hang ups might have been implementation details: the distinction between your program and a program running your program can be blurry in some environments (e.g., Dr. Racket).

                  Given that there are two interleaved programs that may be run, the typed program’s advantage is that it is side effect free by it’s nature. Unit tests, property tests, fuzzers, etc. are running arbitrary code and could trigger arbitrary effects. I think that is ultimately the distinction that matters: how protected are you from mistakes in your program?

                  (Side note: running property tests on a function that sends email could be hilariously bad.)

                  I waffled over whether to post this at the top or the bottom of the thread, since I feel that this fact is at odds with how the discussion progressed.

                  Well, I appreciate being called out on my position.

                  1. 2

                    On this view, what makes the type annotations the second and final program? Could it be three+ programs, since the linter/documentation generator also operate on a language that is intertwined with your program? This is a serious question, btw. I feel like I can think of some answers, but I don’t know that I can reason through them precisely.

                    1. 2

                      You’re quite right. There’s the view that syntax and semantics are the only two components to consider, and it’s a compelling view, rooted in the typical framing of Turing’s and Rice’s Theorems. There’s also the view that dependently-typed theories are at the ceiling of expressive power, and that our separation of types and values is just a happenstance due to choosing weak type systems, which also is tantalizing because of the universal nature of cubical and opetopic type theories. And to answer your point directly, there’s nothing stopping one syntax from having multiple different kinds of annotations which are projected in different ways.

                      I suppose I’m obligated to go with a category-oriented answer. Following Lawvere, syntax and semantics are adjoint and indeed form a Galois connection when viewed in a certain way. So, when we use Rice’s framing to split the properties of a program along such a connection, what we get is a pair of adjoint functors:

                      • On the left, semantics is a functor from programs to families of computer states
                      • On the right, syntax is a functor from families of computer states to programs
                      • The left side of the adjunction: the semantics of a program can include some particular behaviors, if and only if…
                      • The right side of the adjunction: those behaviors are encoded within the syntax of that program

                      And this is a family of adjunctions, with many possibilies for both functors. Rice’s Theorem says that we can’t decide whether most of the left-hand functors are computable, but the right-hand functor is not so encumbered; we can compute some properties of syntax, like well-typedness.

                      We can use the free-forgetful paradigm for analysis too: Semantics freely takes any of the possible execution paths, and syntax forgets which path was taken.

                      There is another functor which is left adjoint to semantics, the structure functor (discussed further here).

                      • On the left, structure is a functor from families of computer states to programs
                      • On the right, the same semantics as before
                      • The left side of the adjunction: the structure of some computations can all be found in a particular program, if and only if…
                      • The right side of the adjunction: the semantics of that program can reach all of those computations

                      In the free-forgetful paradigm, structure freely generates the program which it embodies, and semantics forgets structure.

                      Rice didn’t forbid us from analyzing this structure functor either! As a result, we have two different ways to examine a program without running it and invoking the dreaded semantics functor:

                      • We can study syntax backwards: Which machine states are possibly implied by our program? We can logically simplify the program text if it would help.
                      • We can study structure backwards: Which machine states do our program require or assume? We can simplify the states if it would help.

                      This means that analyzing structure is abstract interpretation! Or I’ve horribly misunderstood something.

                      Now I’m quite sorry to have not posted this at the top of the thread! Oh well.

                    2. 1

                      How does this interpretation handle fully inferred types? Is that not truly an analysis pass on the program, I.e. running a program on the source code, not running the source code itself?

                      I’m not sure if there’s any value in making the distinction… But it feels like there must be, because static types are qualitatively different from dynamic types.

                      1. 1

                        The inference is usually syntactic and doesn’t require examining the semantics of the program. This is the sense in which the second program is intertwined with the first program.

                        For example, in many languages, 42 has a type like Int. This fact could be known by parsers. Similarly, (\x -> x + 1) has a type like Int -> Int. Parsers could know this too, since function types are built out of other types. In general, syntactic analysis can discover both the concrete parse tree and also the inferred type.

                  2. 2

                    Types categorise values, they don’t run code.

          2. 2

            As somebody who is implementing a dynamically typed programming language, I don’t agree with the author. Generating high quality error messages is a lot of work regardless of what kind of language you are implementing. You don’t automatically get high quality errors in a statically typed language. High quality errors are not categorically impossible in a dynamically typed language (as claimed), it’s just an engineering problem. It looks to me that the GHC team has invested more effort in producing good errors than the Nix team, that is all.

            1. 1

              High quality errors are not categorically impossible in a dynamically typed language (as claimed), it’s just an engineering problem.

              Engineering effort can certainly improve error messages in dynamically typed languages, resulting in high quality errors in certain cases. But I have trouble believing that dynamically typed languages can always produce an error as good as one from a statically typed language.

              Consider how a dynamically typed language could possibly produce an error as useful as this hypothetical Nix static type error from the article:

                  { option = [
                      "max-jobs=5"
                      "cores=4"
                      enable "fallback"
              #       ~~~~~~
              #       This element of the list is not a string
                    ];
              

              One of the article’s key points is the convenience of seeing where the error is in your actual code. How could dynamically-typed Nix provide that?

              If it tracked function names better, its error message could have “enable” in place of “<λ>”, resulting in ‘generators.mkValueStringDefault: functions not supported: enable’. But that’s still not as useful as the above error. Knowing the unexpected function’s name is enable wouldn’t be much help if you had many instances of enable in the list, but you forgot to parenthesize only one of them.

              An additional problem with that dynamic error message is that it says the error is within the function generators.mkValueStringDefault. The user’s code never explicitly called that function, so they might have to read their whole program to locate the problem. This could be mitigated by displaying the stack trace along with the error:

              generators.mkValueStringDefault: functions not supported: enable
              something.blah
              something.foo
              pkgs.lib.cli.toGNUCommandLine
              something.processOptions
              

              But that still forces the user to scan the list until they find a function in their actual code, then read all parameters they pass to that function (and that’s assuming global state didn’t cause the error). The example static type error above skips those steps by highlighting the exact line the error was on.

              Now, I could imagine some hybrid type system that doesn’t raise errors until a runtime problem is encountered, and then parses the source code to find all the values that contributed to the problematic value existing. That could be neat… but at that point the work has already been done to implement a static type system. At that point, it would be better make the language also do static type checking, allowing users to sometimes be notified of problems before they happen.

              It looks to me that the GHC team has invested more effort in producing good errors than the Nix team, that is all.

              Above I was describing how creators of a dynamically typed language could invest extra effort to replicate something the hypothetical statically typed language got almost for free. To get the type error “This element of the list is not a string”, the hypothetical static-typed-Nix team only had to annotate function return types. If that team tried to invest as much effort as the hypothetical dynamic-typed-Nix team, they might improve the type error further to this:

                      enable "fallback"
              #       ~~~~~~
              #       This element of the list should be a string, but is a function.
              #       
              #       The formatting of your source code makes me think you might
              #       have wanted this line to be a function call, like this:
              #           (enable "fallback")
              #       That would produce a string.
              

              Could you produce an error message like this with a dynamic type system?

              1. 1

                Racket is dynamically typed and this is how you can get similar error messages in it:

                #lang racket
                 
                (module+ server
                  (provide (contract-out [foo (-> (listof (and/c string? lower?)) number?)]))
                  (define (lower? s) (sequence-andmap char-lower-case? s))
                  (define (foo l) (length l)))
                 
                (module+ main
                  (require (submod ".." server))
                  (foo (list 'enabled "baz")))
                

                will produce:

                foo: contract violation
                  expected: string?
                  given: 'enabled
                  in: an and/c case of
                      an element of
                      the 1st argument of
                      (-> (listof (and/c string? lower?)) number?)
                  contract from: (/tmp/c.rkt server)
                  blaming: (/tmp/c.rkt main)
                   (assuming the contract is correct)
                  at: /tmp/c.rkt:4.26
                

                In fact as you can see, Racket is able to enforce not only simple type level properties (is it a string?) but also much more interesting properties about values - does the list contain only lower case strings? (foo (list "baZ")) will produce:

                foo: contract violation
                  expected: lower?
                  given: "baZ"
                  in: an and/c case of
                      an element of
                      the 1st argument of
                      (-> (listof (and/c string? lower?)) number?)
                  contract from: (/tmp/c.rkt server)
                  blaming: (/tmp/c.rkt main)
                   (assuming the contract is correct)
                  at: /tmp/c.rkt:4.26
                
                1. 1

                  The error message in your first example is certainly more useful than error-checking in most dynamically typed languages. However, I think you missed the point of my comment, because that example doesn’t really address any of these problems that I noted Nix’s dynamically-typed message has and the statically-typed error message wouldn’t have:

                  • Your example’s error message does show the incorrect value, “given: 'enabled”. But would this still work if the incorrect value were an anonymous function rather than a symbol? Or would Racket just say “given: <λ>” like the Nix example unhelpfully does?
                  • Your example’s error message doesn’t include the stack trace at the point the incorrect value 'enabled was found. So if your example program used 'enabled correctly many times within the list but uses it wrongly once, you would have to manually scan all your program’s usages of it.
                  • Even if Racket outputted the stack trace when 'enabled was found, that’s still not as helpful as knowing exactly where in your code 'enabled is written. By “exactly where”, I mean outputting a range of characters in the user’s source code, which is often rendered as an underline in an IDE. Your Racket example does include similar output with /tmp/c.rkt:4.26 in its last line, but this points to the contract that failed (library code), not to the code that broke the contract (the user’s code).

                  In my previous comment, I showed why I thought the article was correct by explaining the above three ways that static type errors can give more relevant information than dynamic type errors.

                  Regarding your second example, being able to assert things about run-time types can indeed catch errors that can’t be caught with static typing. I agree that this can be a useful feature. However, there’s no technical barrier to a statically-typed language supporting runtime-checked contracts as well. Assertions can usually be implemented as a library that throws an exception or returns an error type.

                  I would guess that statically typed languages are less likely to have support for contracts in their standard libraries, due to static types covering some of their use cases. I acknowledge that this could be seen as a bad thing about statically typed languages if you want an ecosystem of programs that often make use of run-time contracts.

            2. 2

              This program contains a type error, but by the time we find out it’s too late: our program will have already wiped the contents of counter.txt by opening the file as a writable handle:

              Wait, how would you fix that in a static type system? Nothing’s stopping you from using the wrong IOMode in Haskell.

              1. 3

                The fact that incorrect use of Haskells IO functions may still compile is not necessarily a fault of Haskells type system, it may just be a badly designed API. If you like the Idris “state-machine in a type system” approach, I guess you could consider the lack of dependent types a problem with Haskell.

                This is orthogonal to the argument made in the article, which is that the method write getting called with an int is an error that could have been caught before.

                1. 1

                  Ohhhh, he meant that type errors happen after side effects, not “the problem is you clobbered the file”. That’s a really confusing example then!