SBTB 2023: Tikhon Jelvis, Better Code Design with Types and Concepts.
Recording: SBTB 2023: Tikhon Jelvis, Better Code Design with Types and Concepts.
Today I'm going to talk about something that I think is really informed how I approach programming. Um and and that is really that types and and and static types can be a as much a tool for better design as they are a tool for correctness. And but to get into that I think we need to start by figuring out, you know, what do we even mean when when we talk about code design, right? And this is one of those ideas that I think isn't particularly well defined. There's a lot of different books written about programming that that that touch on various aspects of design and and and people take a lot of different approaches. Um but for me I found recently I I I found one book that that that helped crystallize the way I was already thinking and which was this book the the essence of software where the key idea for me at least was that when we're designing software, we have some set of sort of, you know, concepts in our minds to represent what we're trying to do or how we're thinking about the system. And trying to do a good job of designing these concepts and and having code that can map to those concepts is a way to, you know, design better software both from the user's point of view, but also from the programmer's point of view. Um but to do this let's throw together a a very simple mental model of how we can approach programming. And one way to approach programming and and this is something I've actually, you know, seen when I you mentor people who are complete beginners, is this sort of very direct approach where you sort of write the thing, right? You you you write some code, you see if it works, if it doesn't work you change it
And the problem with this is that you quickly end up with code that sort of works incidentally, right? Like it happens to do to do the right thing now, not because it's designed or built in a way where, you know, the right thing is the natural result, but just because, you know, you've got it to line up at this specific moment in time. And as things get more complex and and people get more experience, right? Um it starts being impossible to just sort of write code without thinking at all about how to sort of simplify what you're doing and how to come up with some some some sort of sort of abstract concepts that let you tame the amount of details that you have to deal with. And so, a basic model of of how to approach programming is something like, you know, you have, you know, the world or or whatever you're doing, then you have some some kind of mental model that, you know, some ideas and then concepts that you're using to understand the world and to understand uh what you're building. And then, you know, finally you have the code. And ideally, the code should be informed by these concepts. Uh However, there. Sorry. Yeah, uh And one thing I like about having the the this very clear separation between concepts and code, right? Be- because at the end of the day, there's always going to be a difference between, you know, the sort of idealized ideas, you know, you have in your mind, which might be a bit fuzzy, but also more adaptable to to deal with the sort of infinite complexity of the world, and then this very specific code that you've written, which might be over specified, right? It might be a bit off
Is that this model lets us separate the ways in which, you know, we can have code problems or or or technical debt and the ways in which we can improve the code base. For example, some problems are going to be purely about the code. They're not really about the design at all, right? Maybe you just need to run a linter and then clean things up. Uh other problems are going to be at the level of the sort of conceptual design. Right? Perhaps the way you're thinking about something doesn't really make sense. Like the concepts might be inconsistent, they might be incoherent, they might just be too complicated. And I've actually seen a lot of systems where the fundamental design wasn't a problem because the code was poorly written, but it was a problem because it was written based on some set of ideas that was not very well thought out or not really fit for purpose. But I actually think there's an even more subtle and I think more important way for for things to go wrong, which is in sort of the distance between, you know, reality and your ideas about it, so your concept, and also very importantly, the the distance between the concepts that you and other people use to think about the code and the code itself
So, like how easily can you map from the specific artifacts and constructs in your program to these ideas? And when you have this kind of uh mismatch, right? You get a lot of bugs that are very distinctive in the sense that fundamentally, they should not even be meaningful, right? But they they happen, right? I I found a really cute example on on Reddit at some point, which was this idea about how you can accidentally delete all your files with rsync. And the story goes something like this, right? When we run a command line argument command line command, we have this idea of how it works, right? We have a command, then we have these command line flags, which are are little toggles that tell the command to do different things. And then we have the the arguments to the command, the the file paths, they they represent files, right? And there is a qualitative difference between flags and files, right? Flags are controls and and files are inputs, right? Unfortunately, at the code level, the way Unix sees this and the way the program that gets the command line arguments sees this is basically a list of strings. There's a bit of a special case for the command itself and everything else is just undifferentiated strings. So, when you're writing system some command and use a little shell glob, right? As a person, you're still thinking, "Hey, this list of files is going to be a bunch of inputs to my program and it's going to copy all those files into this other directory." But, what happens, right? Somebody makes a little directory and then creates a file called {dash} {dash} delete, right? Um it it it it reads the file name as a flag and deletes deletes the code. And the problem here is that in some sense, this isn't really a problem with rsync. This is a fundamental design issue because there's no way within the system for rsync to know whether some random string was meant to be a command line argument or was meant to be a file path. We just don't make that distinction in the code even though obviously there is a very important distinction there kind of conceptually
So, that's a good example of bad design. Uh but the question is, well, so where do types come in, right? What is the point uh of static types? Um and I I kind of stole stole this title um from a a really good talk title by Conor McBride, which is, you know, what are what are types for or are they just against? And the the question I I I have is a sort of a like do we need static types for good design? And I think there the answer is no, right? Like any sort of abstraction will let us build up good design in our code, right? So, if we don't strictly need types for design, right? Like what are they going to be for? And I I've seen kind of three different models that the people have for how to think about types, right? There's a model of types being sort of bug preventers. There's a model of types providing code structure. And then there's the model that that I'm kind of advocating here, which is thinking of types fundamentally as a sort of a tool for thought and a tool for design. You know, if you're just thinking about types as a way to catch mistakes, it inherently means you have a kind of a limiting view of types. And I I I feel like this often comes from languages that have very limited type systems, or maybe from people who really prefer dynamic typing, right? This is where people say things like, well, you know, I'm never going to confuse an int and a string, so what's the point of of types at all? And the problem with this view is that if this is the approach you take to static types, they'll only ever be useful for problems within purely the code and not any of the problems in the design, right? They won't help your code better match or track your concepts, and they won't help the concepts themselves. Right, so that is very limited. Um other people have this view of types as sort of interfaces or or or modules or modularity, so ways to organize a large code base
And that is you know, again, substantially more than just preventing, you know, confusing two arguments or something. But there's still kind of a a limit to this view in the sense that the types are kind of still seen as separate from the core of the code. And and and and this is something like like where in Java, I think you can and I think a lot of people do, imagine being able to program in Java just with no types. And it would feel kind of more or less the same except you don't have, you know, type errors. Right? And I think this is where a lot of discussions come up where people treat, you know, static versus dynamic as like a single bit, like a binary question. And that's because if your types are there to help you get structure, whether you check them statically or dynamically doesn't really change anything. Um that's it, you know, once you're caring about structure, the types do start helping you with the design to some extent because you can use the types to kind of push the rest of the code base to stick to a pre-planned structure, right? The types form the skeleton, and if you set the skeleton up correctly, it can help keep your code aligned with the conceptual model that you uh you want. However, as I was saying, for me and I think for a lot of people who use kind of, you know, typed functional languages or or languages with more expressive type systems, the type system itself becomes a tool for refining and you know, actually changing the design of the code base or even changing the way you think about whatever you're doing, that is changing your actual conceptual model
And with that approach, you you you can really see types kind of becoming uh qualitatively different tool than kind of the first two two views. So, as I'm saying, we have these three views and I think the first two are maybe more common, but it's this third view of types as a design that I think is is very interesting. But that brings us to an interesting uh to an important question here, which is well, why do we need static types? And I guess if we pop back to to to these three types uh of uh uh sorry, three views of type systems, right? If you just care about preventing bugs, then, you know, static typing helps a little bit, but you can do tests and you can catch errors at run time, that's fine. If you care about code organization, well, you can still have classes and modules and and whatever else you want. And again, like it might be nice to check statically, but it doesn't give you anything fundamentally new compared to having run time checks. But if you're looking at for design, right? Well, that becomes a different situation because what do we want from a design tool? Well, one of the biggest things is we want to be able that to use that tool when we're designing. And that also means that we want a tool that, you know, where the computer can give us useful feedback, right? And and it can do useful work before we have working code, right? Potentially before we've written any kind of real code at all. And for that, you really do need static types because um you know, to do things with dynamic types, you really need to run the code, otherwise the computer can't help you much and you're just thinking in your head
Um And the other thing that uh is also very relevant for static types specifically is that they give us a different way to abstract over the systems that we're building, right? Like as programmers I think we're all very familiar with uh building code abstractions that abstract over implementation details, right? So so information hiding. But types actually abstract a little bit differently where you can use types to provide a kind of a simplified and kind of intentionally limited model of how the program actually runs. So you're sort of hiding details about the actual semantics of your code, right? So that you can reason about them in a way that's a lot easier than dealing with all of the possible complexity of your running program. And there's kind of a classic way to visualize this where you can imagine um your code running along different traces, right? So you you you have some input and then the code runs and it hits different states and it it it it could really be arbitrarily complex. And for real code, right? There's an infinite number of ways the code could run and you know, because of the halting problem, because of Rice's theorem, we know that we can't ever fully reason like reason about every possible trace of a program uh in a way that's precise. And even if you could, even if the program was very restricted, right? Uh the full runtime behavior of even seemingly simple code can be very complex and very hard to keep in your head. So we need some tools, some kind of abstraction that lets us take this very complex runtime behavior and have a view that is simple enough that we can think about it, keep it in our head, that you know, we we don't have to overstrain our working memory to figure out what's going on, but is also still capable enough and useful enough to to to do things with, right? Um and that's kind of one of the things that the that uh type systems get us, right? A A good way to imagine it is if we have this very complex set of possible traces, then a type system carves out a simple shape in the space of all possible program behavior that's conservative. So, it says, "I'm going to cover every single possible way for this program to run." And that's going to include a bunch of possible states and then traces that will never happen
And and maybe it'll include traces that are logically a bug, right? But by being conservative, we can get something that that's kind of simple. And we can also make this guarantee that this type safety guarantee that, "Hey, you know, you're never going to see a state or a trace that is out of bounds of what the the types guarantee." And so, this kind of simplification is the other thing that that that you only really get with static types, right? Because with dynamic types, all of the behavior and checking happens at runtime, and you're back at dealing with all of the individual possible traces that you have in your code. So, uh So, yeah, my the reason that I think it is specifically static types that are so good as a design tool is because they give you this kind of fast feedback, right? Even before you have working code. So, you you you can, you know, write a bunch of Haskell, not fill in any of the definitions, but see like do your type definitions fit together? Do your functions do what you expect them to do, right? And in fact, that's often how I start programming. And so, you get a bunch of quick ideas, and often you start refactoring before you've written code because you realize, "Hey, my original approach, you know, wouldn't work, wouldn't make sense." And we can do this because again, the checking happens without needing to run code. Um and then uh the types also give us a simple way to think about the behavior of different parts of our program when we don't need to fully understand all the details, right? But we just want some idea of how things fit together. And this is also where the expressiveness of a type system becomes pretty important because the extent to which we abstract over the runtime is up to us as as programmers, right? We're the ones choosing how precise of a type to write. And so, on the one hand, having more precision lets us have types that are kind of closer to the full behavior
But the problem is that that isn't always a good thing, right? It might make it more precise, but it also makes it more complex. And sometimes this is a problem just because the encoding of your your your logic in the type system is awkward, but it's also a problem because one of the goals of having types is to have this kind of simplified summary that's easy to hold in your head. And if you expose too much of the sort of real behavior of the program, then the summary becomes sort of insufficiently simplified to keep in your head as easily, and you lose that advantage of having this this specific sort of abstraction over the runtime behavior of your code. So, I I figured we we can jump in and then look at a couple of couple of little examples. And one problem I had with with coming up with examples here is that it was really hard to find things that that didn't require at least a bit of context and background that's hard to supply in in a short talk, but one little project I've been kind of working on, I had a friend who wanted to do this little learning exercise of implementing a JPEG encoder. And it turn turns out that, you know, encoding JPEG is reasonably straightforward, but it has a bunch of steps and you have to do a bunch of different transformations of of the original image. And so, as soon as we started this, right, the first thing I did was I said, "Okay, well, we can start by outlining the the the top-level type that that we're trying to accomplish and then kind of working down, adding more types, right? And writing the types as a way for us to understand how the whole JPEG process works and figure out what the different steps entail and, you know, what we have to do." And you can see kind of like the the the top level type is something like you go from an image that's in RGB and that that's already giving you some ideas about how we see things, right? Because we're talking about color spaces right away right away. And then you know, eventually you you you create a byte string that should be in valid JSON format
And then you know, as as we went through it, you know, we we'd read up on how how JPEG works and then take the ideas we saw and and turn them into types. And I found that this exercise really helped me understand uh you know, some things that you know, maybe are obvious in hindsight but that I I arrived to faster by you know, starting with this type exercise. And a good example here is like, you know, one of the steps that that you do in um the the the the JPEG process is, you know, after switching to this um awkwardly named color space that the which um you know, YCbCr, you do this this down sampling step. And when I started reading about this, right? In my mind I thought oh, well, you know, a down sampled image is just kind of really the same thing as a normal image maybe you just like sample some of the pixels. But the key thing that makes JPEG work is that you sample these different channels separately. Right? And in particular, the Y channel, which is the the sort of the chroma channel, the brightness, uh you you you keep 100% of the the information and then you down sample the the blue and the red channels. And that is one of the core ideas that that sort of makes JPEG work. It's like, you know, humans are good at seeing brightness
They're less good at appreciating, you know, a little bit more, a little bit less red. And so um what happened there is I found that hey, even just without writing any code yet, in the types I can see that hey, we can very easily represent an image as just like a vector of you know, some kind of pixel, you know, like some object that represents a pixel. But you can't ever do that for a down sampled image because the different channels are going to require different um different numbers of pixels. And then because they have different numbers of pixels, they're going to require different sorts of indexing arithmetic and we really have to be able to treat them separately. And the types not only help me kind of see this earlier, right before I got into writing a bunch of code with a bunch of indexing and confuse myself and then you know, ran into all these off-by-one errors. But also in the code, it kind of made it very explicit when we're going from sort of one mode to the other and gave me these sort of touch points where to figure out, you know, what kind of indexing do I do? Um and then another example I have is, you know, for a couple like last year I was working on this book which was it it it sorry, it it is an introduction to reinforcement learning and dynamic programming. And it it seemed at um sort of applied math people. So, the code is in Python
But one of our goals with the book was very much to sort of demonstrate code design, but also have code examples where the structure of the example reflected the structure of the algorithms and and and the processes that that we were modeling. Um and the thing with Markov decision processes is the way they're usually presented sort of in in in math is kind of fiddly. There's a lot of little moving pieces uh and you know, the the details don't matter for this example. But the point is it's not done like it's it's done in a way that doesn't highlight some of the most salient aspects of what makes a Markov decision process a Markov decision process. And then you also have to have, you know, there's other definitions you need before before you get to that one. And the thing I did is before jumping into Python, I actually sat down in in Haskell kind of sketched out some types for what these things would look like. And one thing that helped that helped me immediately was even the first, the simplest version of these types kind of made it a lot simpler for me to to to to kind of see how these things worked. And in particular, if you see the the sort of the the the function specifically for like Markov process, um unlike the math definition, this version kind of with, you know, the state mapping to the distribution of states makes it really clear how these things compose
Like, how do you go from a single step to, you know, a whole chain? Like, what makes it a process? And then also, and then and this may be a bit less obvious, but this S to MS construction also just happens to be a really kind of classical way to model automata. And again, like if you've spent a bunch of time working with Markov chains, I'm sure that thinking of it as a special kind of automaton makes sense. But to me, at least, it was much easier to appreciate what that meant by seeing a kind of a simplified representation like this. And then later on, I actually figured out that, you know, because we're parameterizing over how we represent the the distributions, um we don't even have to deal with all this extra bookkeeping around rewards. And in in the Python version, this was actually a big headache because we didn't have an easy way to do it. Uh but here, we can actually factor it out and have a smaller set of concepts. And again, like, what this ended up doing is the types really reminded me that when you have like a Markov process, um you can think about the process as having rewards and an objective function, but sometimes, it's a very useful perspective to just see these sort of state dynamics of the system and not worry about the rewards at all. And in math, people are used to kind of seeing the same thing from multiple sides simultaneously
Um but I think again, I found it's nice to to be able to do that in in code. Um and again, like, it it made it really easy to figure out like, oh, you know, how you go from like a Markov decision process to just a Markov process or something. But I think maybe a better example here is that we didn't like these three type variables all actually play a very important role, which is that when you have uh different different reinforcement learning or dynamic programming algorithms, they need different properties from like the actions and the state space and so on. And by having these parameters, we get essentially a single concept that covers all of them. It's very explicit about which requirements you need for which algorithm, but you also don't have to make up distinct names and concepts for each kind of process, right? And I think that's pretty powerful and only works because again the the types are pretty expressive. So, in this instance, right, what did static typing get us? Well, it helped in in both cases, it really helped kind of simplify, but also kind of reify, make concrete the the the the the conceptual model we needed to understand uh you know, the domain, whether it's, you know, JPEG and image processing or it's Markov decision processes and reinforcement learning. It let me get some feedback before I had runnable code, right? I could actually see like, "Hey, if I do it this way, uh will it make sense? Will will I be able to like run a simulation of this Markov chain if I organize the code this way or or this other way?" Um then as we're programming, you know, the types give us some interactive feedback. You know, we can do this kind of goal-oriented programming where we you know, leave holes in the code and then and work towards types
And then finally, once we're done, the types serve as a high-level guide to our conceptual model. And my goal for for for code bases is always that, you know, reading the code base should work well as an education in whatever the code is doing. Um and I've I've found the types tend to be very good about that. Like a cute example is like there's this Haskell package called color, uh spelled with an o u, which also ends up working with its types and functions as a pretty good introduction to color spaces in general. So, you know, once we start thinking in terms of designing our code in this way and then and using types like this, right? Uh you know, what do we get from that? Well, the first thing is is is is is that we can just start practicing, you know, essentially type-driven development, right? Um when you're approaching something and you're using a typed language, you can sort of first carefully think about the the concepts you want your code to to to refer to and to represent. Then design types around that, and then you know, get the code from there. And this is both a very productive way to to design and and write code. Uh And it's also I think more likely to produce, you know, higher quality and then easier to understand programs
And the other thing is that this is not so much normative as the this is just the way that uh typed typed programmers work, right? I I I saw this this study recently which was, you know, an observational study of a bunch of um you know, typed functional programmers, and essentially it it it saw that they did pretty consistently use this sort of type-driven approach. Um so, uh the the the same time, all of these ideas fit really well into doing things like domain-driven design. And it turns out that while domain-driven design I think has has this connotation of being very objecty and object-orienty, um it it is actually very nice to be able to take your sort of domain glossary and domain concepts and and translate them into these high-level types, and and you know, it fits into your your functional world. But for me at least, thinking about types in in in this way also really changed the way I think about and evaluate the idea of dependent types. Because originally, right, uh it seemed like everybody was excited for dependent types only kind of if they really wanted to be able to like verify code or prove things that are hard to prove. But what I've realized is that a lot of the times what dependent types will let us let us do is write simpler, more expressive types that on the one hand are closer to the concept you want to represent and do a better job of expressing the way we're thinking about something, but on the other hand, don't have this sort of complicated overhead of bending over backwards and then in in coding them in terms of, you know, type-level features like Haskell has that aren't really designed to be flexible or to do these things, right? So, in some sense, I kind of think that you know, magically moving from Haskell to let's say like a dependently typed Haskell might actually lead to a bunch of types getting simpler just because the type system becomes kind of more flexible and expressive, and people can use that not to make more precise types, but to make the types they already have much nicer and and kind of easier to write and easier to understand. And then I think this is also kind of a very topical uh topical idea because, you know, we're kind of entering this this this this world of of LLM code generation, right? And you know, if you take a step back and we think about what these new uh code generators do well and and and and what they don't, right? And and today what they do well is they design, you know, they can spew out large amounts of bad code. And I honestly, one of the things I'm kind of worried about is that you know, we already kind of live in a world where there's too much bad code, and making it easier to make more of it won't help
Um but, you know, that that's the state today. And so, we kind of want to take a step back and and and and think like, well, can we have some kind of better tools, right? And And no, I'm I'm really saying better tools rather than the better models, right? Because I'm not convinced that there's any easy way to go from the LLM code generation we have today to something that's really good. But I am convinced that there are ways to build tools that let us work at a higher level, right? Have a clean high-level design that, you know, a human came up with and that makes sense and that works really well. And then, you know, rely on code generation to actually fill in fill in the gaps and and and make it all work. And then as a bonus, right? One of the reasons you might want to use a a a a a type system for this, or for that matter like a a specification language, is that you can actually get some level of verification and and make sure that the LLM isn't just you know making up nonsense that that looks plausible, right? And in my ideal world at least, uh you know, LLM code generation will enable us to focus more on design and spend less time on, you know, boring code unless I'm debugging. But I think unless we take an approach like this, it it'll just end up, you know, spending 90% of our time debugging and then the remainder uh well, I I I don't know. Anyway, yeah, and then ultimately I think this just comes down to something I kind of believe in general about programming tools and that is, you know, good tools should should should really help us think. And I think treating types as as as a design tool is is is one way to do that
Um but I think the same principle definitely generalizes. Okay, yeah, and uh I think that's it.