You can model it as part of the type system if you want, but the argument that systems become brittle and harder to maintain if you do. There is less reuse of schemas. That’s what Hickey was saying, and that matches my experience with protobufs.

Hickey gives an example in his talk – the user/address one. It could sound trivial if you haven’t personally experienced this problem, but IME minor changes in the definition of core types have a big architectural effect on the system over time.

Protobufs are similarly central to nearly all Google code, certainly in search and ads, and to a lesser extent Chrome/Android. In a very real sense Google code doesn’t use the type system of C++ or Java; it uses the protobuf type system. I think of it as “extending your system over the network” (which has both good and bad properties).

I left a few years ago, but there are core types for log entries and search requests that have lasted 10-15 years. Maintaining these schemas well is important because there are terabytes/petabytes of data encoded in that format.

There are really two separate cases – when you’re persisting protobuf data, and when you’re sending it to another server as a message. Required fields are bad in both cases. Whether something is required shouldn’t be part of the schema. It’s an orthogonal concern to the shape of the data, because every binary has different requirements.

The schema is universal, but optional/required is relative to a particular piece of code, which you may write and deploy at different times. You can’t upgrade every binary atomically. It has to be done with backward compatibility for years and years. The point of the schemas is to share some information between different binaries operating on the same data, of course.

The issue with protobufs is perhaps a worse version of what happens in Clojure, but it sounds like the use case of “long-lived information systems that model the real world” is very close. What I’d say is that the design decision after ~15 years of using them ended up being the same as what Hickey proposed: in proto1 and proto2 you were forced to specify whether a field was required, optional, or repeated. In proto3 the concept of optional/required went away after some debates.

You can think of it as “every field is optional”, which how Clojure works. Every field of a map is optional, although this doesn’t necessarily characterize the way you write code. There are higher-level conventions than that.

And as I noted in my other comment, the applicability of types is very domain-specific. So I’m not saying Maybe is bad in all cases – just that you have to think about it. People seem to get a lot out of the type system in Elm, in its very different domain of single-page apps.

It makes a very “closed world” assumption and the benefits outweigh the costs in many those cases. (Although honestly I’m hearing a lot about the downsides of this strictness too, probably from people with more open problems.)

If you have an open world, which lasts over many years, then you should be careful about using every bell and whistle of the type system to model the world in a fine-grained / strict fashion. I don’t think it is even limited to Maybe or required/optional, but that is a great example, and he explained it well.

I realized I could have said this in a more concisely… Basically the idea is the the shape is a global property of the system. All binaries operating on the data share knowledge of the shape.

But whether an individual field is used or not isn’t a global property. Binary X might use field A and not B; the opposite is true for binary Y. So it’s better to handle optional/required at runtime in the code for that binary, rather than in the global schema.

This is not a pedantic point – it comes up a lot in practice. Some people are just writing a simple client-server architecture with protobufs, and it doesn’t come up then. But e.g. web search isn’t exactly client/server – there are dozens or even hundreds of binaries operating on the same protobufs. Often they look at a small subset of data and pass it on to other services.

This was several years ago, but as far as I remember, the person who argued the most strongly against putting “required” in schemas was Kenton Varda, author of proto2 and capnproto, who was working on such servers in search. I think he wanted to get rid of the idea of optional/required in proto2, but it was eventually removed in proto3 after he stopped working on it. capnproto doesn’t have this concept either.

The reason it’s a long argument is that there are workarounds for making things required, and probably slight (local) benefits… but the claim is that your code becomes messy over time, with duplicated schemas, bloat from required fields that aren’t actually required, generated schemas to express slight differences, etc.

So I would say there is a tradeoff between locally reasoning about code, and evolving systems in a global fashion. The latter is more important, but you may not realize it yet … :)

It’s all fuzzy to me. They’re both formal specifications. They get overlapped in a lot of ways. Many types people are describing could be pre/post conditions and invariants in contract form for specific data or functions on them. Then, a contract system extended to handle all kinds of things past Boolean will use enough logic to be able to do what advanced type systems do.

Past Pierce or someone formally defining it, I don’t know as a formal, methods non-expert that contract and type systems in general form are fundamentally that different since they’re used the same in a lot of ways. Interchangeably, it would appear, if each uses equally powerful and/or automated logics.

I see the distinction when we talk about pure values, sum and product types. I wonder if the IO monad for example isn’t kind of more on the contract side of things. Sure it works as a type, type inference algorithms work with it, but the sife-effect thing makes it seem more like a pattern.

wow, thanks for that, never really saw it that way but it totally makes sense. not a regular clojure user, but love lisp, and love the ML family of languages.

So? Theory is useless without usable and easy implementation

That wasn’t my point at all. I agree with what Rich says about Maybes in this talk, but it’s obvious from his bad Haskell examples that he hasn’t spent enough time with the language to justify criticizing its type system so harshly.

Also, what he said about representing the idea of a car with information that might or might not be there in different parts of a program might be correct in Haskell’s type system, but in languages with structural subtyping (like TypeScript) or row polymorphism (like Ur/Web) you can easily have a function that takes a car record which may be missing some fields, fills some of them out and returns an object which has a bit more fields than the other one, like Rich described at some point in the talk.

I’m interested to see where he’s gonna end up with this, but I don’t think he’s doing himself any favors by ignoring existing research in the same fields he’s thinking about.

I don’t think rich is nearly as ignorant of Haskell’s type system as everyone seems to think. You can understand this stuff and not find it valuable and it seems pretty clear to me that this is the case. He’s obviously a skilled programmer who’s perspective warrants real consideration, people who are enamored with type systems shouldnt be quick to write him off even if they disagree.

I don’t like dynamic languages fwiw.

I’d love to hear in a detailed fashion how Go has clearly benefited from “ignoring type theory research”.

Does changing the return type of a function from Maybe T to T not mean that you have to change code which uses the return value of that function?

It does in a way, but I think people sometimes over-estimate the amount of changes that are required. It depends on whether or not really really care about the returned value. Let’s look at a couple of examples:

First, let’s look at an example. Let’s say that we had a function that was going to get the first element out of a list, so we start out with something like:

getFirstElem :: [a] -> a
getFirstElem = head

Now, we’ll write a couple of functions that make use of this function. Afterwards, I’ll change my getFirstElem function to return a Maybe a so you can see when, why, and how these specific functions need to change.

First, let’s imagine that I have some list of lists, and I’d like to just return a single list that has the first element; for example I might have something like ["foo","bar","baz"] and I want to get back "fbb". I can do this by calling map over my list of lists with my getFirstElem function:

getFirsts :: [[a]] -> [a]
getFirsts = map getFirstElem

Next, say we wanted to get an idea of how many elements we were removing from our list of lists. For example, in our case of ["foo","bar","baz"] -> "fbb", we’re going from a total of 9 elements down to 3, so we’ve eliminated 6 elements. We can write a function to help us figure out how many elements we’ve dropped pretty easily by looking at the sum of the lengths of the lists in the input lists, and the overall length of the output list.

countDropped :: [[a]] -> [b] -> Int
countDropped a b =
  let a' = sum $ map length a
      b' = length b
  in a' - b'

Finally, we probably want to print out our string, so we’ll use print:

printFirsts =
  let l = ["foo","bar","baz"]
      r = getFirsts l
      d = countDropped l r
  in print l >> print r >> print d

Later, if we decide that we want to change our program to look at ["foo","","bar","","baz"]. We’ll see our program crashes! Oh no! the problem is that head doesn’t work with an empty list, so we better go and update it. We’ll have it return a Maybe a so that we can capture the case where we actually got an empty list.

getFirstElem :: [a] -> Maybe a
getFirstElem = listToMaybe

Now we’ve changed our program so that the type system will explicitly tell us whether we tried to take the head of an empty list or not- and it won’t crash if we pass one in. So what refactoring do we have to do to our program?

Let’s walk back through our functions one-by-one. Our getFirsts function had the type [[a]] -> [a] and we’ll need to change that to [[a]] -> [Maybe a] now. What about the code?

If we look at the type of map we’ll see that it has the type: map :: (c -> d) -> [c] -> [d]. Since both [[a]] -> [a] and [[a]] -> [Maybe a] satisfy the constraint [a] -> [b], (in both cases, c ~ [a], in the first case, d ~ a and in the second d ~ Maybe a). In short, we had to fix our type signature, but nothing in our code has to change at all.

What about countDropped? Even though our types changed, we don’t have to change anything in countDropped at all! Why? Because countDropped is never looking at any values inside of the list- it only cares about the structure of the lists (in this case, how many elements they have).

Finally, we’ll need to update printFirsts. The type signature here doesn’t need to change, but we might want to change the way that we’re printing out our values. Technically we can print a Maybe value, but we’d end up with something like: [Maybe 'f',Nothing,Maybe 'b',Nothing,Maybe 'b'], which isn’t particularly readable. Let’s update it to replace Nothing values with spaces:

printFirsts :: IO ()
printFirsts =
  let l = ["foo","","bar","","baz"]
      r = map (fromMaybe ' ') $ getFirsts' l
      d = countDropped l r
  in print l >> print r >> print d

In short, from this example, you can see that we can refactor our code to change the type, and in most cases the only code that needs to change is code that cares about the value that we’ve changed. In an untyped language you’d expect to still have to change the code that cares about the values you’re passing around, so the only additional changes that we’ve had to do here was a very small update to the type signature (but not the implementation) of one function. In fact, if I’d let the type be inferred (or written a much more general function) I wouldn’t have had to even do that.

There’s an impression that the types in Haskell require you to do a lot of extra work when refactoring, but in practice the changes you are making aren’t materially more or different than the ones you’d make in an untyped language- it’s just that the compiler will tell you about the changes you need to make, so you don’t need to find them through unit tests or program crashes.

He explicitly makes the point that “strengthening a promise”, that is from “I might give you a T” to “I’ll definitely give you a T” shouldn’t necessarily be a breaking change, but is in the absence of union types.

I’d argue that GC is a perfectly fine solution in vast majority of cases. The overhead from advanced GC systems like the one on the JVM is becoming incredibly small. So, the scenarios where you can’t afford GC are niche in my opinion. If you are in such a situation, then types do seem like a reasonable way to approach the problem.

He’s saying that any type signature doesn’t tell you what the function does

I’m kind of a static-typing weenie, but to be fair to Hickey, this is more true in Clojure than it is in Haskell, if you imagine a hypothetical version of Clojure that is statically typed but which still doesn’t track effects using the type system. (This is, admittedly, kind of a strawman.)

Take the type signature [a] -> [a]. In Haskell, there aren’t many possibilities for what this function could be; it could be id or reverse, and it could be something that selects/reorders elements of the list based purely on their indices, but it couldn’t be a random shuffle function, because that would have signature [a] -> IO [a] or similar. But in a language where you can have IO anywhere, [a] -> [a] could just as well be a shuffle function. So what I’m trying to say is, Haskell gives you more static guarantees than Clojure along multiple axes, not just in types ;-)

That being said, even a powerful type system does not excuse you from using descriptive names for your identifiers!

Sure, I’ll buy that, to a degree. Names are important.

However, he uses a function name reverse as his example. Funnily enough, the function you use to reverse a list in Haskell is called… reverse.

Furthermore, he goes on to say that modelling the real world with types doesn’t work in practice, and that you need tests instead. Since when are these two tools mutually exclusive? Does he not know that we also write tests in Haskell?

he’s emphasizing that to humans, information in the name >> information in the type signature.

I’d say this is certainly true of people who haven’t invested any time in learning what types mean and what constraints they enforce. To the people who have though, it provides a wealth of information, e.g., that the first type signature example that slipped out of Hickey’s mouth — a -> a — is an incredibly specific signature that can only have one possible implementation.

That name has no programmatic use. It can’t be referred to in the body of the function. It has no special semantics. It is simply documentation.

I find this surprising and interesting! There are some languages that let you name the output parameter for use in verification, such as to say “the returned z is going to be between inputs x and y.” This is the first I’m hearing of using it purely for documentation.

I’m not providing a default value, just an action on success. If the closure is called, it can do anything or nothing with the value (head) it receives.

Head is a contrived example. The more typical way that this works in OO is to just pass along your results on success to another object. If there’s a problem, you just don’t pass them along. There is no need to check for an error at the other end.