1. 10
  1. 9

    Interesting article, but the author’s understanding of the Halting Problem (and Turing completeness) is… poorly aimed. Yes, the Halting Problem means that there are some properties of programs that cannot be, in general, determined. However:

    • This does not mean that these ‘unknowable’ properties are necessarily useful to us (type systems are already able to prove an enormous number of useful things about program behaviour, even when those type systems are themselves Turing Complete)

    • This does not mean that validation/test-driven development are better than a type system at checking these properties, even in the general case

    In general, I wish folks would stop using the Halting Problem as an argument for things like this. It’s throwing the baby out with the bathwater. Pretty much all useful type systems are Turing Complete, and they’re no less useful because of it! If you’re going to talk about weaknesses in a type system, then talk about those weakenesses: don’t coerce the mere existence of the Halting Problem into a catch-all argument against type systems!

    1. 3

      I definitely get what you’re saying. But the halting problem is an upper bound, and knowing that bound is still useful. It doesn’t mean that we should give up on types and decideability of both weaker properties and weaker logics. But, it is practically a problem that does affect our daily life.

    2. 6

      No, they can’t. The more that we can do with types, the better, in my opinion - I’m super on board with any amount of static type checking. But beyond what we can do with types, there’s the question of how much we should be doing with types.

      For example, these discussions always end up with: “dependent types solve this problem.” Dependent types are basically the end goal of typing maximalism - the thinking that types are the answer to everything, and we should use them for everything.

      Another less extreme viewpoint is to determine which parts of an application make sense to type, and which parts make sense to verify by other means. This is the position that I hold, though I totally see the appeal of wanting to use dependent types for everything. I just think it’s not always practical or even desired - just look at Quicksort in Idris. Yes, it’s awesome that the correctness properties of sorting can be shown in the type system so that the program is correct by construction. But, this is not always code that I want to write.

      A simply-typed program (i.e. basic Haskell or ML types) plus a corresponding test suite for proxy-correctness is almost always less effort to create, but of course the tradeoff is that we’re not actually showing “correctness,” we’re just showing that the program is correct in the cases we’ve observed so far. But that tradeoff is often worth it.

      You even see this tradeoff in proof assistants. There’s a holy war there just as ubiquitous as Emacs vs. Vim, and that’s dependent vs. simple types in the proof assistant logic, most exemplified by Isabelle/HOL on the simply-typed side and Coq on the dependently-typed side. Coq users sometimes can’t even comprehend how serious math can be done without dependent types, but I (and many others) find it much more natural.

      Xavier Leroy himself, the lead of the darling of all formal verification projects CompCert even had this to say in a talk about the virtue of dependent types in proving:

      Dependent types work great to automatically propagate invariants

      • Attached to data structures (standard);
      • In conjunction with monads (new!).

      In most other cases, plain functions + separate theorems about them are generally more convenient.

      All this to say, I personally feel that we want to treat types as a panacea, but we’ll always need to reason about the actual execution of programs. Types cannot replace validation.

      1. 3

        This matters because understanding that a normal type system is not Turing-complete means that there are truths it can’t express

        Yeah, but it’s pretty rare in production software to want to be Turing complete. It’s more common to want restrictions on space and time usage, for example. Such restrictions are typically implemented in such a way that proofs of restriction should be straightforward, and totally doable in a dependently typed language, if not in a much simpler type system. But, so far, such type systems are quite rare to non-existent in production software.

        1. 3

          Such a requirement may look difficult until inspiration hits. Then one day you may realise that it’d be as simple as a list of pairs (two-tuples). In Haskell, it could be as simple as this:

          newtype EvenList a = EvenList [(a,a)] deriving (Eq, Show)

          With such a constructive data model, lists of uneven length are unrepresentable. This is a simple example of the kind of creative thinking you may need to engage in with constructive data modelling.

          Ah, but that’s not quite the same as a List! How do you get the seventh element? For a list it’s xs !! 6, for an EvenList it’s fst(xs !! 3). That’s one of the big disadvantages of constructive data over predicative data: it’s not interchangeable with the general type.

          1. 1

            It wouldn’t be a particularly difficult stretch to implement the list interface over this storage mechanism however. E.g.

            get(index) => index % 2 == 0 ? underlyingList.get(index/2).first : underlyingList.get(index/2).second;

            I’ve been reading Mark’s stuff for years. It’s likely intentional that though the blog article elides some information so as not to expand beyond the necessity.

          2. 2

            My views on tests and typing changed when I started using Clojure after using Rust for a while. Some types are just really a pain in the ass to write down or represent even with a really good type system.

            With Clojure’s spec or third-party alternatives like malli you have the full power of Clojure to express the constraints or shape of your data without losing sight of the type of the underlying data e.g. string, int, etc.

            That said, these two languages are operating at different levels of abstraction and I don’t know you would use spec or malli to represent smart pointers, for instance.

            1. 1

              Describing routes at the type level is used in the servant Haskell package to type check an entire API, and parsing routes can be extended to include regular expressions. So I guess yeah, they can! Most Languages’ type systems can’t express that much, tho.

              Annotating record fields with dependent types can do this validation too, but building up all proofs along the way so you can prove any interest fact about the values. Perhaps a parser combinator library in a dependent typed language could hold and compose proofs easily along the way, in the same manner as they can hold state that is useful for pushing and popping names in the context. Essentially describe the validation as parsing with dependent typed parser combinators.