1. 25

  2. 6

    I think that the view that type systems exist to just enforce rules and check that your programs are correct is very incomplete: type systems are extremely powerful reasoning mechanisms that themselves allow you to express properties of your programs and are a space where you construct them, not just restrict them at the value level. I think Idris is the best example of this, although Haskell might be more accessible and serve as a bridge if you want to go in that direction. I suggest getting the Idris book, currently going through it and it’s extremely well-written!

    The central idea in Idris are dependent types: essentially they remove the distinction between a type variable and a regular variable, allowing you to say that for example a Matrix 3 4 is a wholly different type than Matrix 4 3, and when you have access to such specific types, a large part of your programming is lifted to the type level.

    The author still seems to think, for example, that good type systems don’t force you to write annotations unless you really must. In Idris, type annotations are enforced, because they aren’t merely annotations to help the compiler infer other types, but are just the place where you write a large part of your program (albeit dependent types make type inference harder so there’s a technical component to that).

    1. 1

      Well, nothing stops you from writing stringly typed code full of mutations using IORefs in Idris. The point with strong type systems is not that you have to write safe code, it’s that you can do so.

    2. 5

      Apropos of not much related to the actual article:

      I need to know the difference between int, long, uin8_t, size_t even if all I want is a goddamn integer.

      Use the fixed width integer types (uintX_t, intX_t and friends) and avoid the fundamental integer types (int, long, etc). It’s not as easy as “a goddamn integer”, but it’s easier than the fundamental types since you know the size.

      1. 1

        On the contrary, “Use int unless you’re interfacing with hardware” should be the rule of thumb. Yes, I know, the standard library makes it hard to use int because of the now we-never-should-have-done-that prevalence of size_t, but range-based for loops have made that mostly ok.

      2. 3

        A message veiled into a personal learning story to make it more palatable. I would not care much, but it scratches an itch.

        We got a slight tests vs. type checking going in the middle of the lines. These subjects should not be dumped together because you may also do Python without any tools and get along just fine.

        My opinion about types and type checking has changed as well, but it has grown to very different direction than the posters. I also have had some sort of enlightenment going along. I am a die-hard dynamic-typing proponent. I did not need a static type system, and I neither needed tests. The author had to work with something else than Python to form his opinion. I had to go into other direction, deeper into Python and finally into my own improved variation of Python.

        If type checking is sound, and if it is decidable, then it must be incomplete. I’ve realized this is really important as the set of correct and useful programs that do not pass a type checker is large. Worse, often these are the most important sort of programs that spares a person from stupid or menial work.

        “If it compiles, it works” and “type system make unit tests unnecessary” are hogwash. It doesn’t really matter how much you repeat them or whether you clothe them into a learning story. There was a recent post pointing out how difficult it is to construct a proof that some small program is actually correct. This means you cannot expect that program works or is correct despite that it types correctly in any language.

        There is an aspect that is required for making computation and logical reasoning possible in the first place. That is in recognizing variant and invariant parts of the program. I’ve realized that spamming variants is the issue in modern dynamically typed languages. That cannot be solved by adding type annotations because you still have tons of variables in your code that could theoretically change. And you really have to check whether they do, otherwise you have not verified that your program is correct.

        Statically typed languages commonly do better in keeping variances smaller, but they are also stupid in the sense that they introduce additional false invariants that you are required to satisfy in order to make the type checking succeed. And you cannot evaluate the program before the type checker is satisfied. This is an arbitrary limitation and I think people defending this for any reason are just dumb. Type checker shouldn’t be a straitjacket for your language. It should be a tool and only required when you’re going to formally verify or optimize something.

        During working on software I’ve realized the best workflow is to make the software work first, then later validate and optimize. Languages like Python are good for the first purpose while some ML-variants are good for the middle, and for the optimization C and similar are good. So our programming languages have been written orthogonal, to cross with the workflow that makes most sense.

        1. 20

          the set of correct and useful programs that do not pass a type checker is large

          If it’s large then you should be able to give a few convincing examples.

          1. 5

            I haven’t had the problem the quote implies. The basic, type systems were about enforcing specific properties throughout the codebase and/or catching specific kinds of errors. They seem to do that fine in any language designed well. When designers slip up, users notice with it becoming a best practice to avoid whatever causes protection scheme to fail.

            Essentially, the type system blocks some of the most damaging kinds of errors so I can focus on other verification conditions or errors it can prevent. It reduces my mental burden letting me track less stuff. One can design incredibly-difficult, type systems that try to do everything under the sun which can add as many problems as they subtract. That’s a different conversation, though.

            1. 1

              This set includes programs that could be put to pass a type checker, given that you put extra work into it, or use a specific type checker for them. Otherwise that set is empty: For every program you can construct such variation where the parts that do not type check are lifted outside from the realm of the type checker. For example. stringly typed code.

              The recipe to construct a program that does not pass a type checker is to vary things that have to be invariant for the type checker. For example, if you have a function that loads a function, we cannot determine the type for the function that is produced. If the loaded function behaves like an ordinary function, it may result in a dilemma that you may have to resolve either by giving it some weird different type that includes the idea that you do not know the call signature, or by not type checking the program.

              Analogous to the function example: If you define creation of an abstract datatype as a program, then you also have a situation where the abstract datatype may exist, but you cannot type the program that creates it, and you will know the type information for the datatype only after the program has finished.

              And also consider this: When you write software, you are yourself doing effort to verify that it does what you want. People are not very formal though, and you will likely find ways to prove yourself that the program works, but it does not necessarily align with the way the system thinks about your program. And you are likely to vary the ways you use to conclude the thing works because you are not restricted to just one way of thinking about code. This is also visible in type systems that themselves can be wildly different from each other, such that the same form of a same program does not type in an another type system.

              I think for the future I’ll try to pick up examples of this kind of tricky situations. I am going to encounter them in the future because in my newest language I’ll have a type inference and checking integrated into the language, despite that the language is very dynamic by nature.

              There is some work involved in giving you proper examples, and I think people have already moved to reading something else when I finish, but we’ll eventually resume to this subject anyway.

              1. 6

                Looking forward to seeing your examples, but until then we don’t have any way to evaluate your claims.

                About your function loading example, that may or may not be typeable, depending on the deserialisation mechanism. Again, can’t really say without seeing an example.

                1. 6

                  When you write software, you are yourself doing effort to verify that it does what you want.

                  That’s exactly why I find type systems so useful. I’m doing the effort when writing the code either way; types give me a way to write down why it works. If I don’t write it down, I have to figure out why it works all over again every time I come back to the code.

              2. 6

                A message veiled into a personal learning story to make it more palatable.

                Why do you think this is veiled message instead of an actual personal story?

                1. 5

                  If type checking is sound, and if it is decidable, then it must be incomplete.

                  Only if you assume that some large set of programs must be valuable. In my experience useful programs are constructive, based on human-friendly constructions, and so we can use a much more restricted language than something Turing-complete.

                  1. 1

                    If type checking is sound, and if it is decidable, then it must be incomplete.

                    That’s not a bug. That’s a feature.

                    If you can implement a particular code feature in a language subset that is restricted from Turing completeness, then you should. It makes the code less likely to have a security vulnerability or bug. (See LangSec)

                  2. 1

                    “all you need to annotate are function parameters and return values” - true in C++ now too, it’s not just Rust.

                    “gtest sucks” - it does, but there are far better alternatives. I agree that pytest rocks. I’m curious as to whether dependency injection and mocking are better in Rust than in C++, especially given the lack of compile-time reflection.

                    1. 3

                      In my experience C++ generally requires more annotation of types within a function body, so it is still fair to call out annotating only function parameters and return values as a strength of Rust in particular.

                      For example in Rust:

                      // Within the same function body we push a `&str` into the vector
                      // so compiler understands this must be a `Vec<&str>`.
                      let mut vec = Vec::new();

                      versus C++:

                      // Vector element type cannot be inferred.
                      std::vector<const char *> vec;
                      1. 1

                        C++17 has constructor template argument deduction, so you can just say auto vec = vector({"str"}) now. Though Rust’s type inference is obviously more powerful.