Transcript
Lucas Dohmen: Hello, listeners, and welcome to a new Conversation about Software Engineering. Today on the CaSE Podcast I have a guest, Lars Hupel. Hi, Lars.
Lars Hupel: Hi, Lucas.
Lucas Dohmen: Today we will talk about algebraic design. Lars is well-known for his contributions on the Scala language, on the Typelevel project. His Ph.D. thesis was the formal proof of compiler correctness, and he's a senior consultant at INNOQ.
Lucas Dohmen: For the listeners that don't know Scala, we will not go deep into Scala in this podcast, no worries, but just say a few words about Scala. What kind of language is it?
Lars Hupel: Scala is a hybrid functional and object-oriented language, which initially started out targeting the JVM, but has since also gained a JavaScript back-end. It is quite similar to Java syntax-wise, but extends it in many different ways. For example, there's multiple inherited traits, some things borrowed from Ruby... There's obviously lambda expressions and many other things, and also it's got a much more advanced type system than Java.
Lucas Dohmen: Okay. Typelevel already sounds like type systems, or something... Can you say a few words about the Typelevel project?
Lars Hupel: Yes. Typelevel basically got started because I initially thought that the name sounded cool, and the creator of Scala, Martin Odersky, and a few other people had recently founded a company called Typesafe, so I thought Typelevel would also be a cool name.
Lars Hupel: The idea behind Typelevel is that we want to bring strong functional programming to the JVM, borrowing some principals from (for example) Haskell, but at the same time we wanted to make it idiomatic for Scala. We didn't just want to copy Haskell, or turn it into Scala, or the other way around; we wanted to enable the kind of programming you do in Haskell, and then make that amenable force for Scala.
Lucas Dohmen: So is it a library, or is it a set of libraries?
Lars Hupel: It started out as a collection of three libraries that sort of work together in nice ways. Now, I forgot numbers, but we have probably about 30 libraries now under this umbrella. And since we got started, we also have organized conferences about these topics, and we're working together with Scala Days, for example, with the collocated event... So it's both a set of libraries, but it's also a community for Scala people who want to do functional programming.
Lucas Dohmen: So is it fair to say that in Scala there are some people that program in an object-oriented way and some people that program more in a functional way, or is it a hybrid approach for everyone?
Lars Hupel: It's kind of a mix and match approach, and it is fair to say that different parts of the community prefer different approaches. For example, there's also a strong part of the community that uses Akka, for example, which has this actor-based programming notion... Which of course you can mix and match with functional programming if you want to, but there are a few people who are migrating their codebase from Java, and for them it's very attractive to keep doing the more object-oriented, more imperative style of programming, and then maybe gradually change over to Scala, for example, starting out with their tests...
Lars Hupel: So Scala - there's not really one style of programming, and I guess a lot of people find it very attractive, but a lot of people also criticize that, because it's not like in Python, where there's one way to do things, which is pythonic; in Scala there's not really anything like scalanic, or scalactic, or whatever... There are multiple different ideas about that.
Lucas Dohmen: So would you say that the Typelevel project tries to find an idiomatic way to do one style of Scala programming?
Lars Hupel: Yes, I think that's fair to say. A functional way of programming that makes the most use of Scala's idioms. We try to not work against the language, we try to work with the language, and then kind of improve on the developer experience.
Lucas Dohmen: Cool. In today's podcast we will not go deep into the Typelevel project; instead, I wanted to go a little bit more meta than that, by exploring the differences in the OO style and FP style, but from an entirely new lens. We want to do that by talking about the expression problem. Can you maybe tell us what the expression problem is?
Lars Hupel: Yeah, it's one of my favorite problems.
Lucas Dohmen: Okay... Do you like problems?
Lars Hupel: Of course. That's why I did a Ph.D. thesis... So the expression problem can be described as you have data, and that data can come in multiple different forms. On one hand, you might want to add more forms of data, but on the other hand you may also want to add more operations on that same data. The expression problem basically describes that we always have to make a trade-off. So either we choose a design approach of our data, that makes it easy to add more kinds of data at a later point. That's usually what can be modeled with subclasses very easily. You have an interface, and you can always add more classes that implement this interface.
Lars Hupel: Or the other trade-off would be you can also implement it in such a way that it's easy to add more operations later on. The set of data is fixed, and then you can add more operations, which in the object-oriented way would usually be called a visitor pattern. So you can always add more operations; not more kinds, but also the other way around. The expression problem basically says that you always have to do some kind of trade-off between those two things.
Lucas Dohmen: Let's try to revisit that with an example. Let's say I want to do something like a painting program. We have different shapes, like squares and circles, and I want to get the size of one of the shapes, and that's what I have now. What does the expression problem say now? What's my problem now?
Lars Hupel: Let's say you have implemented it in a purely object-oriented way, so you have maybe an interface that's called Shape, and that interface provides exactly one method, which would be called "get size" or "compute size", and that returns a floating-point number, for example.
Lars Hupel: Now, in this object-oriented way you could then add more subclasses, you could say "I have a subclass 'rectangle' to implement shape", and then it computes to size based on the length of both sides. Then you could have a circle or an ellipsis, which kind of depends on Pi to some extent, and then you could also add more of these shapes - triangles, whatever other things.
Lars Hupel: If you want to add another method, for example that moves or scales a shape, you have a problem... Because you have a bunch of classes that already are in this interface, but now if you want to add this scaling function, for example, you would need to touch all of these different classes. That's a problem with modularity. In a new module, you can always add more (different) shapes, but you couldn't add another operation without touching all the existing implementations.
Lucas Dohmen: So the problem doesn't state that it's impossible, it just states that it's a lot more work, because you have to touch more kinds of code, right?
Lars Hupel: Exactly. And the reversed trade-off for that is if you would be modeling that in a functional programming language, you would usually specify the kinds of data that you have upfront. So you would have a data type that has particular cases, and then any kind of operation is just a function derived on these cases. Then you can always implement more functions that work on the cases that you already know, for example by using pattern-matching.
Lars Hupel: But if you want to add more cases... Let's say you have already rectangle and circle, and you want to add a triangle - you would have to touch all the different pattern-matching constructs in your code, otherwise you may have a problem because your function receives a shape that it doesn't know about how to deal with. So that would be the other end.
Lars Hupel: In a new module, you could always define more functions on the same data, but you couldn't just add more different shapes. For that, you would have to touch all the existing functions on that shape.
Lucas Dohmen: Just to be clear about it, does the expression problem already state that the one approach is functional and the other one is object-oriented, or is it more nuanced than that?
Lars Hupel: I would say it's more general than that. It's just that, for example, the object-oriented way with subclasses, and for example the Haskell way with serial types - it's just two very succinct illustrations of these opposing ends of this trade-off. But you can make that design work in any language, no matter what approach you choose.
Lars Hupel: In particular, I think the term "expression problem" or the problem behind it is probably older than many other programming terms, and it's been described quite a while ago... In fact, the original definition by Philip Wadler, who's one of the creators of Haskell - in his description he doesn't even mention functional or object-oriented programming, at all. He just talks about adding more cases or adding more operations without recompiling existing code, and that's about it. He doesn't really make any point about the paradigm behind it.
Lucas Dohmen: If we are looking into the approach -- let's just say that we go the approach of using interfaces in Java. Are there approaches where people tried to solve the expression problem without leaving the approach with interfaces in an object-oriented language, or is it because it's unsolvable, we can't do anything about it?
Lars Hupel: All of these problems are solvable, it just depends on how much boilerplate code you're willing to write. And in particular, there are ways to work around this in Java, for example. One such possibility is called object algebras, where you would be using much more interfaces than usual. So instead of working with subclasses, concrete subclasses like 'circle' or 'rectangle', you would have an interface that defines methods for constructing and deconstructing rectangles and circles.
Lars Hupel: All of that is possible, however it requires a lot of boilerplate in Java. But after Java 8, where the language also learned lambdas in its syntax, it's become much better to work with... Although I'm not entirely clear if anyone has been using it that much. You do see the visitor pattern sometimes, but the visitor pattern is kind of like the opposite end of the trade-off. But these object algebras - I think they're mainly of academic interest.
Lucas Dohmen: What do you think is the reason for that? Are people that go with this classic Java OO approach - are they just not feeling the pain of the problem? Is it too academic, or...?
Lars Hupel: It's maybe just a different mindset, and also many people are not acutely aware that this is a problem that has a name, that has been talked about in research. People are very content with modeling their objects and their domains in this interface and classes style, that maybe it doesn't even occur to them that there could be a different way of doing these things.
Lucas Dohmen: On the other hand, let's say we are programming in Haskell... Do I have a chance to escape the expression problem there, into the other direction?
Lars Hupel: Yes, so in Haskell what people would typically use is a construct that's called type classes. Type classes have nothing to do with classes as you know from Java, so you have to completely forget about what I've just said earlier; it's got nothing to do with interfaces or classes. Type classes are essentially a way of adding more operations on existing types. If you are used to maybe Kotlin or C#, you may have heard that concept called extension methods... Although Haskell did that before them, so they have pioneered type classes.
Lars Hupel: What it basically means - it's like an interface, but it's an interface that you can implement after the fact. So you can define the data type, you can design an interface, and then you can make an implementation of this interface for a data type, but you can do it at an arbitrary point. If you want to add such an implementation, you don't have to touch the interface or the data type; it's just something that's completely decoupled from these two things.
Lars Hupel: It's kind of interesting that some other languages are also moving towards this stuff, for example in Rust, where you have these traits and then impls for these traits; that works in a similar way.
Lars Hupel: There's still a bit of a problem in Haskell, because usually you wouldn't abstract over different types that have the same interface. So you would usually talk about one type at the same time that has this interface implementation, but for example in Haskell you wouldn't really have a list of objects; this notion doesn't really make any sense. In Java if you have a list of objects, you can at runtime look what class it is, and then do something with it. In Haskell you can't really do that. That's what these type classes are for. That also means that you would probably have a list of things that are shapes. If you want to abstract all these types, you always need a little bit more structure that you can work with.
Lars Hupel: For example, if you have a list of shapes, then you can say "Well, I want to scale all of these shapes." But you couldn't necessarily look at what kind of shape it is, because you have discarded that information. It's not there in a type.
Lucas Dohmen: Let's go into this example again... Let's say that I have a collection of some kind, like an array or a list of shapes, and I want to get a list of all their sizes. How would this work in this kind of way?
Lars Hupel: Well, you could imagine that you would have a type class that has a size operations that takes in the shape of that particular type, and then returns a floating-point number. Then you could just map this function over the list, and then you would get a list of floating-point numbers.
Lucas Dohmen: Okay, and each of them is of this same type class.
Lars Hupel: Yeah.
Lucas Dohmen: Okay. Interesting. From a basic perspective, it looks a lot like they all just adhere to the same interface.
Lars Hupel: Exactly.
Lucas Dohmen: Even though it has some more possibilities, from this point of view it's basically the same.
Lars Hupel: Yes. But I do want to point out that in Haskell code you very rarely see these kinds of abstracted collections. You would usually have a collection, like a list of one concrete type. It really doesn't happen that often that you would do that... And that's also a different mindset. People would tend to model their type just at once. They'd say "I have a data type shape, and I give these five different possibilities of what that shape could be", and then you'd just have a list of these things. But you wouldn't frequently have that kind of extensibility there, in that direction.
Lucas Dohmen: Okay.
Lars Hupel: So it's just a completely opposite way of thinking about modeling data.
Lucas Dohmen: So the typical approach to modeling in Haskell would not say that we have triangles and circles, they would just say they are shapes?
Lars Hupel: I would say in Haskell you would try to break these things down to their bare components. For example, you would probably have a data type that can store polygons, because then you can construct triangles and many other things based on these polygons.
Lars Hupel: Of course, you also need something for arcs and curves in order to get circles, but in principle, you would try to break down these components to their bare minimum, so that you can describe their structure once and for all, and then you can compose those small structures into bigger structures, like rectangles for example.
Lucas Dohmen: Oh, okay. Interesting. Let's get back to the title of the episode. We said something about algebras... What is an algebra?
Lars Hupel: Right. So if you ask a mathematician what an algebra is, it's basically just a list of objects and a list of operations you can do on these objects, which sounds like it can be any number of things. It's not very concrete.
Lucas Dohmen: It could, for example, be some kinds of shapes and operations on those shapes?
Lars Hupel: Exactly, yes. And what's most important about these algebras is they usually come equipped with some laws that those operations have to adhere to. So you can't just manipulate some objects in that algebra, but you also need to make sure that these operations follow some kind of laws. For example, one law would be idempotence. If you apply an operation once, and then you apply it once more, then it should be the same thing as applying it once. And I believe in particular in the field of databases, in distributed systems, this is a property you very often want. An algebra basically says you have a structure, you have operations on them, and then these operations satisfy some kinds of laws.
Lucas Dohmen: But something being an algebra doesn't imply any specific laws. It just says that there could be laws.
Lars Hupel: If you say "I'm going to design an algebra", it's kind of the intention to make some laws about these, so that you can reason about these algebras abstractly. And this is the purpose why algebra exists in mathematics, because mathematicians don't like to talk about concrete things; I mean, some mathematicians do, but I'm a formal methods person, so I like to talk about abstract things.
Lars Hupel: Instead of talking, for example, about real numbers, we would talk about some kind of algebra that abstracts over that, so we can talk about real numbers, natural numbers, complex numbers and other things at the same time, without having to be very specific about the concrete object. But we can talk about addition, for example, because we know that addition has some particular properties for all the different structures that are out there. We can say that addition on integers satisfies similar laws like the addition on real numbers, for example; it doesn't matter where you put the parentheses, and in what order you do the operation... So commutativity and associativity.
Lars Hupel: This is the same for integers, for real numbers, for complex numbers, for example... So by talking about these abstract algebras, you try to remove all the concrete details that are irrelevant to your problem. Instead, you focus on the laws that these operations satisfy.
Lucas Dohmen: I imagine that some people need some additional information about that, so let's unwrap that. Is summing up numbers an algebra? Is addition an algebra?
Lars Hupel: You wouldn't call addition being an algebra, you would give it a different name. We would be talking about monoids here. I'm not actually sure where the term monoid comes from. It's just something that you learn very early on in university when you study algebra.
Lars Hupel: A monoid is an algebra that says there must be one operation - and we would usually call that operation addition, for example - and then we say "This operation must have one property, which means it doesn't matter where we put the parentheses." So if you have a+b+c, it doesn't matter if you add a and b first, and then you add c on top, or if you first add b and c, and then add a on top.
Lars Hupel: A monoid also requires that there has to be a zero of some kind, and that zero must be neutral with respect to the addition operation. So you have 0+a=a, and a+0=a. So it should be neutral with respect to the operation.
Lucas Dohmen: If we go back to fifth grade or sixth grade, we learned some of those laws in school, right?
Lars Hupel: Yes, of course.
Lucas Dohmen: But we don't talk about algebra in that sense, we just get concrete laws for addition, for example.
Lars Hupel: Exactly. And very often that's how the human brain works. You talk about different concrete examples that follow the same property, and then our brain is very good at extracting the general patterns from that. That's what the mathematicians did; they said "Okay, we have these integers, we have these rational numbers, they have a similar operation, they work similarly, so maybe we should just abstract it and call it a monoid, for example."
Lars Hupel: But there's also completely different examples of monoids, in real life, if you consider trains, for example. You can describe trains as a monoid. But we have to use old-school trains for that; old-school trains, that consist of multiple different carriages and maybe locomotives. All of these carriages have couplers, where you can merge two trains together, you can attach one to the other... That's also a monoid, because the attaching operation is a monoid operation, and you can also say it doesn't matter in which order you do the coupling. You can first attach all the carriages, and then add it at the end the locomotive, or you can also first add one after the other carriage to the locomotive, for example... And you can also have multiple locomotives in between. If it's a long train, you need multiple cars that drive the train... So that's a real-life example of monoids.
Lucas Dohmen: And if we go back to things that we do in programming, like lists, and concatenating them - that's also an algebra?
Lars Hupel: It would be an example of a monoid. It's a specific instance of this monoid algebra.
Lucas Dohmen: Okay. This now is pretty abstract... What does it have to do with the expression problem?
Lars Hupel: Oh, yes. Interesting question. So in algebraic design approach you would try to break down your data into the most atomic parts. What I've also mentioned before - for example, you would try to express shapes as polygons, and then you would try to describe all the operations you can do on these polygons, and you would then try to build a much richer API based only on those primitives. Other clients of your library - they can define their own composite/complex shapes based on your primitives.
Lars Hupel: All of that works out, because you have thought about the laws that you want to offer to clients, what they should expect. For example scaling, where it doesn't matter if you scale twice or you scale just once, with a larger scaling factor. For example, if you scale twice with a scaling factor of two, then you could also scale once with a scaling factor of four. So you also have similar properties like in monoids, for example, because it really doesn't matter in which order you do the scaling. If you do multiple scalings in order, you can just collapse them to just one.
Lars Hupel: It also reflects in, for example, the Java Stream API, where you have multiple operation you can do on these streams. For example, if you map twice, you can also just map once with a compose function. All of these things come from the fact that somebody has thought very hard what the primitive operations are, and what kind of laws you can provide on these operations.
Lucas Dohmen: So if we are following algebraic designs, do we always think about those rules in the back of our minds (the rules of composition), or is this just very natural to you, to think in this way?
Lars Hupel: Well, for me it's quite natural, because again, I come from a methods place; what we do is we basically write specifications, and then we try to prove that our implementations satisfy these specifications. So to me it comes very natural, but also only because I've been working with this for many years. So I wouldn't expect someone who just started out with programming to do that. In particular, I think people who are new to that still tend to think about concrete examples, which you also see in unit tests, for example; it's most about concrete examples and the outputs, instead of describing actually relationships between input and output, no matter what the concrete value is.
Lucas Dohmen: Before we get into specifications - because that's another topic I want to talk to you about - do you have an example where you would say that you get to a different result when using algebraic design than the "OO" (in big quotes) approach?
Lars Hupel: Yes, I could think of one such example, and it's something that's become relatively popular in the past few years, which is this distributed data structure that's called CRDTs. That stands for conflict-free replicated data types. Those have been around for a while now. Basically, the idea is that you have some kind of data structure, and that may be distributed among different systems, and then you want to find some kind of consensus of what the shared view of these things are.
Lars Hupel: Those can be stuff like you have a CRDT for JSON documents, or you could have something simpler, like a CRDT just for set. There are many different CRDTs, but what's common to all of them - they have a very fixed set of shapes that the data can have. For example for JSON you know it can be an object, it can be an array, for example, but you can't extend that.
Lars Hupel: There's also a set of operations you can do. For example, you can insert some values, you could move around some values, and it's very clear that these operations behave in a particular way.
Lars Hupel: For example, for many classes of these CRDTs, these operations are commutative; that means you can swap them in any order, which is very nice if you're working in distributed systems, where messages may get delayed, they may get dropped or reshuffled in some way... So you could, for example, just send those messages out (these operations) as they come in, and then no matter in what order they arrive at a different system, the other system will be able to reconstruct the same state.
Lars Hupel: A very simple CRDT would be a counter. You have a counter, and every time someone clicks on a platform, click on Like, you want to have a shared understanding. So you just send a +1 operation. This is obviously commutative. It doesn't matter in which order those plus-ones arrive, you will always arrive at the same result. A counter would be a very simple example, but of course, there are more complex ones, like (as I said) JSON documents.
Lars Hupel: The cool thing is because of this commutativity property, you are always guaranteed that you will eventually converge to a consistent view of your world. Eventually, all the nodes will agree on what the current state is. You also don't need a central coordinator. All of these are peers, and they can send a message to each other, and they will converge. This is a result of thinking very hard what the data looks like and what kind of primitive operations you could do. So that's what I would call algebraic design.
Lars Hupel: On the other hand, if you would do non-algebraic design, you would think about for example user stories. The user wants to do this kind of operation/process, and then you have a bunch of things that need to happen. You would, for example, have an API that says "Do this operation", like "buy a house", or I don't know... It sounds like a very big operation, but... And then the implementer of that API would then take care of doing all of these steps in one atomic way. So it kind of shifts the responsibility a bit around... And I think this is the beauty of the algebraic design - by talking about these laws, you get these primitive operations, and then clients of your library can compose them in a way they see fit, without getting an API that prescribes how you have to think.
Lucas Dohmen: The way that you describe that sounds a lot like in this approach to programming you have to have a bigger effort of thinking upfront and thinking through the entire problem before you start working on it. It sounds more like "big design upfront"; that has a bad name in the Agile fields. Would you say that this is a fair assessment, or is this not fair?
Lars Hupel: I would say it's totally fair, and depending on what your domain is, you may be required to do that, because it could be (for example) too costly if you make mistakes, and they're too costly to change.
Lars Hupel: If you have some kind of smartphone app that's for entertainment purposes, it doesn't really matter; you can just change things. But for example if you're designing a medical device, you are in a domain anyway where you have to think very hard upfront, because the mistakes are very costly. I think depending on your domain, it may even be required or it can be very worthwhile to think very hard about your design upfront.
Lucas Dohmen: Let's say that I design a plane. Then maybe the cost is very high if something goes wrong, right?
Lars Hupel: Right, exactly. Although these are kind of like too orthogonal things. I just wanted to make the point that there are legitimate domains where you have to do an upfront design.
Lucas Dohmen: Yes. What it reminds me of - there is this way of thinking, that some people want to do iterative information processing, and some want to do comprehensive information processing. They want to gather as much information beforehand, and then solve the problem, while others want to be iterative. Do you think that this is a different style of thinking, that maybe some people would prefer to go this way because their thinking style is different?
Lars Hupel: Yes, totally. Different people think in different ways, they have a different perspective on the world. For example, I'm the kind of person who would like to collect as much information beforehand as possible... But I can see how others would prefer a different way.
Lucas Dohmen: So it's not only a question about the problem, but also maybe about the people that want to solve it, right?
Lars Hupel: Exactly. Also, if you're building a software system, there may be subparts of this that you may want to solve in one particular way - for example the core of the system, the data processing bit of it - and other parts, like maybe the user interface, you may do it in a different way, because you can't even envision right now how the user is going to interact with the system. On the other hand, the core might as well be rock-solid; you already have a very clear picture of what it would look like.
Lars Hupel: In particular, the domain-driven design approach also can be construed in thinking very hard about the domain objects that you have in the first place. Then you have these value objects, you describe in very clear detail what the objects from your domain are. Then you have, for example, the aggregates, where you have to describe what the relationship between those things is, how they can interact with each other... And this is also kind of a similar thing - you have to think upfront about your domain objects and their interactions/relationships. Nobody prevents you from changing that at some point; you should still be able to change this... But still, the methodology is the same way, I would argue.
Lucas Dohmen: Okay. But just to understand that, in a lot of projects we have to make assumptions about our users, about how they want to interact with our product, and those assumptions might be wrong, because users behave differently than we assume... In this scenario, would you say that this approach that needs a lot of design upfront has a disadvantage, because we have to make too many assumptions and don't know enough?
Lars Hupel: Yes, I think that's a fair summary. Again, I think this is a matter of splitting up, or trying to segregate the core, where you have a very clear idea to maybe some other parts that may be completely in flux. For example, when you're talking about assumptions - when you make assumptions about users, they're usually wrong... So you build the product, and then it gets user-tested, and then they may be doing something completely different.
Lars Hupel: On the other hand, if you (for example) talk to someone in accounting, what an invoice looks like - you can be very sure that these requirements are probably going to stay the same, because it's very unlikely that a tax accountant will say next month "Actually, I've changed my mind. The value added tax works completely differently now." This is probably a nice example there - you have some domain areas where you can be very sure upfront, and others maybe, like UI, that may change very frequently.
Lucas Dohmen: Okay, that sounds reasonable. So if we look into this and we move our focus to testing, I can imagine that the way that we probably do testing in this more iterative style (TDD style) is maybe different than the way we would test it in this approach. Can you talk a little bit about testing in this mindset?
Lars Hupel: Yes. I agree, these algebraic design patterns really don't like TDD, and vice-versa. In TDD you always have the approach of thinking with the examples first. So you write a piece of test code that would say, for example, "I'm calling this function with the number 5, and the string hello, and then I get a result that's maybe 8." While writing the tests, you only have the rules in your mind, but what you type are concrete examples, and the relationships basically get lost in translation. So you have something in your mind, but you have something else in the code. Then you write the code in such a way that it reconstructs these rules, and then make sure the tests pass.
Lars Hupel: On the other hand, when you do this algebraic approach, you would think about the laws. And the laws don't care about specific values. The commutativity law for integers would be x+y=y+x. The order doesn't matter. But when talking about this law, you don't think about 5 or 3, you think about x and y. So your tests would be much more abstract. Your tests would not be talking about concrete examples, the tests would be talking about variables. And then you would be using some kind of framework that would be able to fill in examples for these variables.
Lars Hupel: For example, the test literally says "For all x and y, ensure that x+y=y+x". And then you would use some kind of framework - those frameworks are known as property testing frameworks - that would then look at the type of x and y and then figure out some examples, and then just test 100 instances of this. So I would argue that this is completely different, because in TDD people are very specific about testing edge cases and documenting very clearly "This is a test about this particular part, and this is a test about this particular zero, and empty string, whatever." And in testing for algebraic design, you would offload that to the property framework. So you would say "Just give me any x and y. I don't care. Just check that the relationship that I had in mind holds, and I don't care about the specifics."
Lucas Dohmen: But it's hard for me to imagine how this works in the addition case. So I would just say "Generate examples for me", but how does the framework know that the result is correct?
Lars Hupel: Well, you would say, for example for all x and y, and then you would make an assertion. You would do this in the same way as in unit testing, where you expect that this thing equals that other thing. You would do the same in this property testing style. You would also make an assertion, but you don't care where the input values come from.
Lucas Dohmen: But it sounds a little bit like I am implementing everything twice. I'm writing the way tests work, and then I'm implementing it the same way. How does that fit together?
Lars Hupel: That might very well be the case in a lot of examples... But I have a very nice counter-example to this, where the specifications for the tests look very different from the implementation, which is sorting algorithms. It is very simple to write an efficient function that checks if a list is sorted. You would just look at one element after the other, and check if the next element is larger than the previous element. So that would be a specification; this is what being sorted means.
Lars Hupel: On the other hand, writing an efficient sorting algorithm is very hard. The JVM has this Timsort algorithm which had a bunch of bugs in there, and now they're sure it's correct... But anyway, it's a big function, it does a lot of things, it is very performance-optimized. The point is the specification in this case is very simple; you give a list in, you expect a list back, which has the same elements, but now sorted. That is very easy to write down, but the implementation is very hard.
Lars Hupel: This is actually a prime example for how you can use property testing... Because instead of writing five different lists as input that you want to get sorted, just say "Give me any list, pipe it through the sort function, and check if the result is sorted." That's obviously very different from a basic implementation.
Lars Hupel: Now, if you talk about addition, for example, of course that might be sometimes difficult, because very often operators are trivial to implement, and then you would just be duplicating this... So I think this is another case of thinking very hard about what the actual properties are, so that you don't have to repeat yourself in the test, because that would be an anti-pattern. And if the specification is the same as the implementation, that's no good.
Lucas Dohmen: Yes, okay. It reminds me a little bit of the P versus NP problem. You have problems where it's very easy to check if the result is correct, but it's not easy to get to the result, right?
Lars Hupel: Exactly. And most of the time when we implement our business code we don't have to solve these big problems; we don't tend to have to solve the satisfiability problem, or anything that's in NP. But what we have to do is we have to solve stuff efficiently, so one fallback option that you could always do is very often when you think about a problem you have a very simple implementation that's super-slow - maybe it just tries out things - and then you have an implementation that's smart, but very hard to figure out if it's correct. So you could just compare these two things. When you test, you could just write a simple implementation, that's very short, and maybe slow, and you can compare that to the actual...
Lars Hupel: I would still think that's like a second-class test, it's not something I would prefer, but if there's nothing else that you could come up, it's still something very nice to be doing.
Lucas Dohmen: It reminds me a little bit of the -- GitHub has a gem called Science [correction: scientist], which allows you to do refactorings in production. Say you have an old implementation of the code and you know that it works, but you want to make it faster. What they do is basically they run the new implementation and the old implementation, and they compare results, to just understand if the new better implementation is really correct.
Lars Hupel: Yes. That sounds like a strategy of dealing with legacy systems, I'm assuming...
Lucas Dohmen: Yes, right.
Lars Hupel: I would argue that's not exactly algebraic design, because in algebraic design you really want to talk about the relationships. For example you have a currency type, and then you know "Well, adding these is a monoid", because it shouldn't matter in which order some balance operations happen on the currency amount. I would argue this is more of an algebraic design pattern, and you use property testing to enforce this, but you can also use property testing in different ways that are maybe not strictly speaking algebraic.
Lucas Dohmen: Okay. But you're probably also taught that style of thinking at university, so I can imagine that it's hard to get into this mindset of uncovering the attributes of your system, the rules of your system, to write the correct property tests.
Lars Hupel: Yes. Yes, it's very hard, and in fact, writing specifications is something that I think takes a lot more time to learn than writing implementations. But I think it's worth investing the effort in there, because very frequently just thinking about the specification uncovers problems with your implementation. There are few universities that actually teach only specification, without proof. So they teach students how to write specifications without actually giving them the tools to check if the specification or the implementation is correct.
Lars Hupel: But just thinking about the specification makes us think very hard about corner cases upfront, and just that is a tool by itself to improve software quality. You don't even need to write these tests, even just in the process of writing down or thinking about these properties; you think "Oh, actually - what happens if I have an empty list here? Maybe I didn't think of that..."
Lars Hupel: Of course, you can also get there with TDD, but TDD in my experience is always much more example-driven. When you think about these specifications, they are usually much more abstract, and people tend to think about a wider variety of different inputs or conditions.
Lucas Dohmen: Yes, interesting. The way that a lot of people do TDD - me included - is you always write the test and write the smallest piece of code that satisfies this test. You try to trick yourself, basically... But this doesn't work with this implementation, and this implementation, and you would do--
Lars Hupel: Yes, exactly.
Lucas Dohmen: So would you say that it's fair to say that this approach is more focused on the problem, while the TDD approach is more focused on the solution maybe?
Lars Hupel: Yes, I think that's a fair assessment. I think someone famous - I forgot who it was - once said "How to solve any problem... Step one, think very hard. Second, there's the solution."
Lucas Dohmen: Okay, interesting. While we are at it, let's talk about model checking. How does this play into this framework?
Lars Hupel: Model checking - maybe for people who don't know it - is a technique that also originates from this formal methods area in computer science research... Basically, it's kind of property testing on steroids, because it tries to explore a much larger state space. Whereas in property testing usually the frameworks are set up in a way that they would try 100 random examples maybe, in model checking what you can do is you can write down the specification - maybe for example for a distributed system - and then you can invoke a tool, and then the tool... You could say "Try this out for up to five agents", and the tool would try to exhaustively find all the states in that system, up to five agents, and then try to figure out if there's something that's breaking it.
Lars Hupel: Or for example you could say "I have some kind of code that has loops", and then you could say "Try to find all the states with up to five loop iterations", and then it would try to find problems in the implementation there.
Lars Hupel: So it's a much more exhaustive way of testing things, because it looks at the actual state space of some code. And there's a lot of people who actually use it in practice, for example Microsoft.
Lars Hupel: Let's say you're a device vendor and you want to ship your driver with Windows. I think at some point (Windows 7, or something like that) they started to enforce that those drivers pass these model checking suites. They would for example check there is no null pointer dereference or no division by zero or something and of course, it's very hard to prove that in general. It's actually very difficult and expensive to prove that... So you will have these model checking tools which will then try to explore the state space up to a reasonable boundary, like saying "I'm going to look at up to five agents, up to ten loop iterations", or something like that.
Lars Hupel: Usually, this works hand-in-hand with the specification. You would say, for example, "My specification for device drivers would be: I don’t have null pointer dereference and also I don't want to be stuck in an infinite loop", something like that. Of course, it's a very different domain from what we have talked about before, but for distributed systems it's also very interesting. And if you have distributed databases, you want to assert that it takes only that amount of cycles to arrive at a consensus, for example, and these model checking tools are very useful for that.
Lucas Dohmen: I think the number of states will get very big, very fast... Does it take days to simulate it then, or...?
Lars Hupel: That's why you have to give an upper bound of the state. Property testing just says "Give me 100", and then you know exactly how long it's going to take; it's actually 100 iterations.
Lucas Dohmen: Interesting.
Lars Hupel: But for model checking - yes, you have to find a reasonable boundary. Because if you ask for like a list of operations for 50 agents, you're going to have to wait until the heat death of the universe. It's not going to finish until then.
Lucas Dohmen: So how is the connection to formal proofs then? We know them from math... Is it similar to formal proofs?
Lars Hupel: Yes, I mean -- if you look at the progression from unit testing to property testing to model checking, then the end would be a formal proof, where you would argue about all the different states. And you can't do that just by enumerating all the different states, because there are infinitely many states. For example, when you sort lists, there are infinitely many lists that you could be sorting, so it doesn't really make sense to say "Try all the lists". You can't. Instead, you have to look at the actual implementation.
Lars Hupel: All the other things before - they treat the implementation as a black box. Your unit testing library cannot look at the implementation, it will just run the implementation. And most of the times, it's also similar for model checking; it just treats that as a black box.
Lars Hupel: In formal proof you actually have to open the black box, you actually have to look inside at what makes these things work, what are the invariants that you have to satisfy in loops, for example.
Lars Hupel: Sorting is, again, a nice example. For merge sort you would have the invariant that you always split a list in two, and then you sort the smallest, and then those sub-lists are sorted, and then you can merge them together. So you actually have to argue about the concrete implementation, what's happening there. This takes a long time, because you have to actually think about what's happening there.
Lars Hupel: If you say that an implementation is simple and the specification is harder, then the formal proof would be an order of magnitude even harder than the specification, so... This requires a lot of careful thinking there.
Lucas Dohmen: Interesting. In distributed systems there's this problem of consensus, that we also already mentioned. Leslie Lamport wrote a lot of papers about it, and he came up with this system called TLA+ to show that his implementation is right. On which level of this scale that you explained would TLA+ be? Would it be a formal proof, or...?
Lars Hupel: TLA+ itself is just a language, it's a specification language, and there are model checkers for TLA+. I believe there may be tools that you can write formal proofs on TLA+ specifications, but I'm not sure how widely they are being used. But in principle, I think most people will be using it for model checking.
Lucas Dohmen: Okay. So we could write a model checking test with TLA+ for our sorting algorithm, or distributed problem?
Lars Hupel: Yes, I think most cases for TLA+ would be more in the distributed systems domain. I'm not sure how many people use it for sorting.
Lucas Dohmen: Okay, this would be maybe a bit too complicated for such a simple problem maybe...
Lars Hupel: I don't know. I don't really have much experience with TLA+.
Lucas Dohmen: Have you also looked at Idris?
Lars Hupel: Yes, Idris is another interesting hybrid, because in Idris you can make formal proofs embedded in the language. You have a programming language that is useful for implementing algorithms and other things, and at the same time it has an embedded type system that is powerful enough to let you actually specify properties on those programs you wrote, and then also write the proofs.
Lars Hupel: Idris is interesting because as far as these kinds of languages go, it's designed with usability in mind, so it is actually designed to write programs that you couldn't write -- like, you could write a microservice in Idris; that's the plan. I'm not sure if there are such frameworks yet... Idris Boot, maybe. [laughter] But at least that's the design. And the creator of Idris calls it PacMan-complete. It's a language that you could write PacMan in.
Lars Hupel: You can also write unit tests in Idris, but it will shine if you try to write proofs about your programs in there. Once you try that, you will realize that proving correctness is very hard. The usual rule of thumb is that you have to write an order of magnitude more lines of proof than lines of code, and I'm assuming that will be similar for Idris.
Lucas Dohmen: So in Idris would you write the proof as like the type, or is it something different?
Lars Hupel: No, in Idris you would write a specification as a type. You would for example give the specification what it means to be sorted, you would write it as a type, and then a sorting function like merge sort or bubble sort would have that type, that not only says "You give a list in and get a list back", but it would also say "Well, you take in a list, and you return a list that's also sorted, and has the same elements as the input."
Lars Hupel: You can do that with a type system that's called dependent types. Basically, what it allows you to do is you can specify return types that depend on the input. You could say the merge sort function has an output type that contains additional information. In Java you couldn't just say it returns a list. In Idris you can say it returns a sorted list that contains the same elements as the input. So you have this kind of dependency between input and output there.
Lucas Dohmen: So would it be fair to say that a type system is a way to specify the behavior of the code?
Lars Hupel: Yes, very much so. And depending on the level of sophistication in your type system, that's the amount of specification that you can do. Java can do specifications; if you have a function that returns a list, that's already a specification, because you know "Well, it returns a list." It doesn't return a float, it doesn't return a string; it returns a list. And in languages that are untyped, like JavaScript, you don't have that.
Lars Hupel: In JavaScript you have a function and you know it returns something, but you don't know what it returns, so you would need to look at the code. But in Java you can already see the types... Although you might argue that just looking at the return type it's not going to help you very much.
Lucas Dohmen: But it also says something about maybe "Can this function raise an exception?" You cannot see that in JavaScript. You cannot see if it could raise an exception.
Lars Hupel: Yes. But also in Java very often you can't see that, because there are runtime exceptions. But for a language like Haskell, where -- I mean, there are still exceptions in Haskell, but they are very rarely used, and only in particular circumstances... But a regular function, for example a sorting function, couldn't throw an exception just like that. I mean, yes it can, but it's a cultural style that people wouldn't raise exceptions if the type doesn't say so. And you could still get runtime exceptions like division by zero; you can't see that in a type in Haskell, but in Idris for example you can do that. You could define a division operation where the compiler would reject the invocation of that operation if you can't prove that it doesn't divide by zero.
Lucas Dohmen: Yes. But probably a type system cannot prove that something doesn't raise an exception, because it would be equivalent to the halting problem, probably.
Lars Hupel: That's a common misconception. What you can do with a type system is you can say "If it compiles, then it won't raise an exception. But if it does not compile, it may not be able to prove that, and it may still not raise an exception, but it may still fail to compile." For example, in Java you can write type correct programs that wouldn't crash at runtime, which don't compile because the types don't line up.
Lars Hupel: Maybe you have something like "If false, return 5. Else return string". This will always return a string, because you have an 'if false' in front, but the compiler wouldn't accept the program, because statically it can't determine this. You would violate the halting problem if you could say "Always, with absolutely certainty, can it raise an exception or not?" In a good type system you can say "If it compiles, it works. But if it doesn't compile, I have no idea." So there's not always 100% certainty. It might still work, but fails to compile.
Lucas Dohmen: Okay, so it's conservative and it just says "If I'm not sure, I will assume it doesn't work."
Lars Hupel: Yes, exactly. You're erring on the conservative side there.
Lucas Dohmen: Yes, okay. So is there a way for me to then say "Believe me, computer, I know this works"?
Lars Hupel: Yes, in all of the languages. But this is why I was a little unclear about Haskell. Culturally speaking, you wouldn't throw an exception in Haskell, but you can always do that and silence the compiler warning. And also in Idris -- I'm not sure what it's called in Idris. The system I've worked with at the university - you could just say sorry. Literally, you could type in "sorry" and it would accept what you said. Other languages have different ways. In Java you can use a cast.
Lars Hupel: Almost all of these practical languages have escape hatches, because the real world is messy, and you have this nice corner of specifications and algebras and stuff, but as soon as you have to talk to a web service, all bets are off. It can do arbitrary things, and you would be very annoyed if you couldn't have any kind of escape patch.
Lucas Dohmen: What was the language that you used?
Lars Hupel: The system that I've used was called Isabelle, and it's also a specification and proving language.
Lucas Dohmen: Interesting. To wrap this conversation up, let's talk a bit about practicality. You already mentioned that a few times - would you say that if I write a typical business web application that algebraic design is helpful to design it? Or would you say that it doesn't fit that space very well?
Lars Hupel: I like this credo "functional core, imperative shell" very much, where you would try to isolate your beautiful algebraic domain logic from the messy real world. For example, you're writing a web application that some REST endpoints, then you'd use whatever your dirty framework has to offer - annotations, whatever; just slap it on there. Just take in the request and parse them in some way, and then you create some domain objects and then you pass it onto the core, that will then deal with it in a predictable fashion. Then you can test those things separately and you can also devise different front-ends for that.
Lars Hupel: I am very much in favor of trying to separate the messy real world from the internal functionings, and I have yet to see a domain where it's completely impossible to have a functional core. In almost all of the domains this is possible, to some extent.
Lucas Dohmen: But in this view of the world, talking to the database would also be the messy part. It would be outside of the functional core, right?
Lars Hupel: It depends on what database you're talking to. Very often you can also align your data models, whatever that database has. If you have something that maps very naturally to a relational database, then you can actually leverage the properties that the relational database has... Because SQL databases are based on relational algebra, so there's algebra again. If you don't have that - maybe you're talking to a MongoDB, where you just have unstructured JSON documents... Then it's part of the shell, right?
Lucas Dohmen: Yes.
Lars Hupel: But all depends on how your data model aligns with your data source. If you're lucky, this is the same thing. Otherwise, you just have to put some more conversions on there. I think this is also called sometimes Onion Architecture, and it's just good design; your inner details are not encumbered by opening a network connection, for example.
Lucas Dohmen: So talking to the database would not be part of it, but the database model would be part of it.
Lars Hupel: I think so, yes. And if whatever database driver you have doesn't allow you to do that, then you just have to write your own library on top of that. It would probably not be a very good idea to just write raw SQL code in there, but maybe use some higher abstractions. There are a lot of different libraries that do that. Maybe not Hibernate, but something that's maybe a little bit more functional.
Lucas Dohmen: Okay. Thank you, Lars, so much for this conversation.
Lars Hupel: Yes, thanks for having me.
Lucas Dohmen: To our listeners, until next time. Bye-bye!
Lars Hupel: Bye!