1. 38

  2. 16

    I’m on the record of not really buying into Rich’s discourse about things, but I think he’s not wrong as much as telling a story in a way I’m not enthusiastic about.

    Types are one of many forms of static verification. They are a certain kind of logical framework (of which there are many) with certain sorts of nice properties. Often these properties are valuable as they work in concert with the kinds of questions you must ask and answer while programming. Additionally, they can sometimes turn local verification into global verification—a very, very nice super power and the sort of thing that makes them compare favorably against testing.

    But they have some assumptions.

    Anyone who’s ever written serialization types—one set for your API, one set for your domain, one set for your database row—can instantly recognize the pain of “essentially the same data” showing up in multiple forms. Modern statically typed systems fail to capture something here. They correctly note that these three types are different, but often fail to note how they’re the same.

    One way to style the desiderate of this use case is that we’d like for many subjects at different locations to be able to have different views of some interface/datum which are compatible. What comes to mind is the story of the 5 blind men and the elephant. Usually the moral is how people who only see part of the picture can be very wrong… but you can also turn it on its head and see it as showing 5 perspectives can be simultaneously different and correct.

    Another metaphor is the entire CRDT program. We recognize that due to the “speed of light” it is impossible for multiple disparate actors to agree completely about a changing topic and instead ask for something less demanding—even if they disagree, they should at least be able to converge. This is a much weaker thing to ask for, so we lose some and gain some in the process.

    Finally, as I’ve been thinking about this it reminds me a little of sheaf theory and coherence spaces (and really model theory at large). These are all to some degree or another methods for talking about how many “partial observation” can be combined to all be valid, consistent views of something large and interesting.

    This is a really important idea and I think most type systems are built in a formalism where it doesn’t exist. They assume locality (more or less).

    Finally, the moment I wrote the above line I caught myself as of course ML-like modules are one form of non-locality! A very well studied and understood one based on existential types. So of course standard type systems have this in the bag—quantification, things like row types, subtyping. These technologies exist. But I also can hear Rich’s talk as saying “sure, but they’re just not good enough yet”. I think it’s an interesting question to try to figure out what “good enough” would mean.

    1. 7

      Using polymorphic variants you can strengthen the return type. For example:

      match foo 2 with 
        | `Y y -> y 
        | `Z -> 0

      will continue to compile with both

      let foo y = if y == 0 then `Z else `Y (y + 1)

      and the strengthened

      let foo y = `Y (y + 1)
      1. 8

        A possibly-interesting angle: bare union types as you sometimes see in progressive and/or structural type systems, e.g. TypeScript, could afford you part of this as well—because you can broaden the type signature allowed without breaking callers.

        For the primary motivating example, assuming you have some kind of Maybe type in TS (insert shameless plug here):

        type Maybe<T> =
          | { tag: 'just', value: T }
          | { tag: 'nothing' };
        type f1 = (a: number) => number;
        type f2 = (a: number) => Maybe<number>;

        You can trivially perform the first transformation:

        type f1 = (a: number | Maybe<number>) => number;

        You cannot update f2 this way, because you have something that isn’t null or undefined as your way of handling optionality/nullability/nothingness. This means that for Hickey’s purposes, a non-Maybe-typed definition would work better:

        type f2 = (a: number) => number | undefined;

        This can be trivially strengthened in just the way Hickey wants:

        type f2 = (a: number) => number;

        The downside, and I’ve never seen him acknowledge this, is that now Zalgo undefined is loose in your system, unless you have something like TS to check you everywhere with strictNullChecks: true or something like that. (If you do, though, you can in principle—though not in TS—have a sound type system even with this.)

        The one thing I’ll add is that you can write an abstraction that properly deals with this and is relatively elegant… if and only if you embrace a pure functional style in TS, and of course you still have the demons of null and undefined running around, so better hope nobody just coerces it instead of checking it.

        type Maybe<T> = T | null | undefined;
        // you could curry this with lodash or manually or whatever
        function map(fn: (t: T) => U, m: Maybe<T>): Maybe<T> {
          return t ? fn(t) : undefined;
        let f: Maybe<string> = 'hey';
        let g: Maybe<string> = null;
        const len = (s: string): => s.length;
        map(f, len); // 3
        map(g, len); // null

        You can’t do it with wrapping types (as in my library) for the reasons outlined above, and in the context of TypeScript as it stands today (without some kind of pipeline operator), that makes for a much less ergonomic approach. However, it strongly suggests the utility of a structurally typed functional programming language for getting at the kinds of things Hickey wants—even if they might not be the same things other programming communities want, as other comments here have noted.

        …I may need to turn this into a full-on blog post.

        1. 1

          I immediately thought of union types in TypeScript as well when watching this. You mention strict mode in TypeScript (which is now the default), but for those less familiar with the language I think it’s worth highlighting that assuming you’re using it, the ideal Hickeyian Maybe type can be expressed very simply without having null-safety issues:

          type Maybe<T> = T | null;

          A function that previously accepted T can be broadened to allow Maybe<T> without breaking callers unlike in Haskell (or Rust), and similarly a function that previously returned Maybe<T> can be narrowed to simply return T as well without breaking callers or requiring automated refactoring tools.

          In strict mode the compiler will force you to do a null check before using a possibly-null variable, so you don’t have safety footguns in using it. Ditto for undefined.

        2. 3

          Take the following code:

          match f () with | Some v -> … | None -> …

          If f is modified such that it always returns a value, named v in this case, what does that match mean?

          In a language with subtyping, roughly the same thing this does.

          match 2 with
          | 2 -> "guaranteed"
          | _ -> "won't match"
          1. 1

            I guess the obvious question is why would you want to have that in your code? Isn’t it just confusing to the reader to have code which looks like it’s handling an optional value but isn’t? If, as described in the article, you can change f2 from int -> int option to int -> int without altering the call site, you’ll just end up with a buildup of legacy cruft throughout your code which has to be cleaned up manually.

            1. 6

              On the other hand, what if you have a function that takes int -> int option as a parameter? Should you be able to pass in a function with signature int -> int?

              1. 2

                Personally, I would rather the the type system disallow that. It’s not too much effort to write something like pure . f2 in place of f2.

              2. 2

                Why would it need to be cleaned up manually? Given a type system that allows such a thing, finding all locations with code that is dead after the signature change is trivial. You could even automatically remove that dead code (and review the automated changes of course).

            2. 5

              Rich has said a lot of nonsense about type systems over the years, but I think “you should be able to change a function so that it returns an Option without modifying the callers” takes the cake. Really glad I didn’t watch that keynote.

              1. 13

                He said that you should be able to modify a function so it can take an optional instead of a mandatory without modifying the callers. It’s a standard example of “weakening preconditions” that most languages support.

                1. 12

                  He said you should be able to modify a function from returning an option to returning a guaranteed non-null value. You have it backwards.

                  1. 6

                    Ah, OK; I misread the first example. Still wrong, but not blindingly, searingly wrong.

                    1. 7

                      I’m not sure I see how it’s wrong. It’s a semantically equivalent change and a small user interface boon. Tagged unions are not the only way to do unions.

                      1. 5

                        How is it semantically equivalent? It seems to me the former is widening the possible domain of result values, whike the latter is restricting the possible domain of result values. The former is, in general, impossible to safely accommodate without checking all callers, while the latter might conceivably not require any changes in callers.

                        1. 3

                          The comment I was replying to said that the example was “still wrong”.

                        2. 4

                          You’ll notice that on lobste.rs a suggestion that type systems may not be as useful in general is often conveniently interpreted as simply being ignorant about type systems :-)

                          1. 13

                            We’re talking about someone who has a long and well-documented history of straw-mans on this topic. If it were someone other than Rich I’d probably cut them more slack.

                    2. 1

                      I think what he’s proposing for spec is pretty interesting, independent of his ideology regarding types. That starts around 30 minutes in.

                    3. 2

                      Wow. I’m happily surprised about Hickey recognizing that his optional record-attributes correspond to Maybe. Then he goes on and gets the idea through that naming of attributes should be also subject to module scoping, and that we have generic need to work with partial information.

                      These ideas would be quite compatible with Prolog’s partial data structures and Haskell’s profunctor optics.

                      I wouldn’t want it with recursive types though, but otherwise it’s cool. Also handling this kind of set-objects would likely require MLsub’s subtyping inference.

                      1. 1

                        Another offshoot point is that Rich seems to appreciate unions more than sums. It is not the case that Maybe A is “A with one more value”. It’s a new type with canonical injections A -> Maybe A and () -> Maybe A and a universal property that makes it optimal among types “computations” which achieve that. It includes the ability to recognize which “side” it is on.

                        To push the intuition further, do you believe we should be able to weaken A -> B to Either[A, A] -> B? Why or why not?

                        1. 1

                          If you include commutativity, yeah. You see this all the time in APIs. Suppose I had union types. A | Nil is the return type in one place, B | Nil in another. Suppose I called both of these functions and returned the first if not nil, the second otherwise. The return type for my new function is now the union of these two. But A | Nil | B | Nil = A | Nil | Nil | B = A | B | Nil.

                          This gets much more interesting when instead of just nullability you are talking about exception types. If exceptions were meant to be handled by tagged unions, why did SML and Ocaml include exceptions?

                          1. 1

                            Yeah, that’s one possible equality and it is modeled by unions. My example of A | A versus Either[A, A] is aimed to tease apart when exactly you might want one over the other. Another model that pushes the issue is forall a. Maybe a -> R.