Recorded 2024-07-04. Published 2024-08-04.
In this episode, Wouter and Sam interview Dominic Orchard. Dominic has many roles, including: senior lecturer at the University of Kent, co-director of the Institute of Computing for Climate Science, and bye-fellow of Queen’s College in Cambridge. We will not only discuss his work on Granule - graded monads, coeffects, and linear types - but also his collaboration with actual scientists to improve the languages with which they work.
Wouter Swierstra (0:00:15): Welcome to the next episode of the Haskell interlude. I’m Wouter Swierstra, and I’m joined today by my co-host, Samantha Frohlich.
Samantha Frohlich (0:00:22): Hi.
WS (0:00:23): Our guest today is Dominic Orchard, who will tell us a bit about impact by infection, the accidental complexity of climate models in Fortran, and climate modeling in Haskell using linear types.
SF (0:00:38): Welcome, Dominic. So, how did you get into Haskell?
Dominic Orchard (0:00:41): Well, when I was a teenager, I was really obsessed with low-level programming. I loved processor design and assembly language, and I wrote lots of C code. I was a very nerdy teenager. I was just really interested in working at the lowest level and really making the computer do these very specific things. And that was really what I thought programming was about. I thought, ‘Oh, it’s C or it’s nothing, right?’ C, you can make things really fast. And that was my view of programming.
When I then went to university, I was a student in England at the University of Warwick, where I studied Computer Science, and I was extremely excited to basically get to immerse myself in a thing that I already loved. And perhaps I went in thinking, ‘Yeah, I know what this programming thing is.’ But in our first year, we had a core module that was functional programming. And I thought, ‘Well, all programming is functional. It has to do something.’ And I sat down in this lecture theater taught by David Lacey, who had been involved in various functional programming research compilers, and it was just like the world flipped upside down. It was like a scene in a movie where it’s like you enter into a different world. And I sat there and listened to these lectures and thought, ‘This is amazing.’ This is programming, but it’s like my favorite bit of maths. I had studied maths a lot at high school, and my degree was very mathematical, and I loved doing proof by induction. That was one of the favorite things I did at high school. And I was sitting there thinking, ‘This is like the proof by induction, but it’s programming, and I’m making the computer do the thing.’
So, by the end of that course, it was a complete turnaround in my understanding of what programming is, what computer science is. I thought, ‘This is fantastic.’ I really loved it. That was actually using standard ML. That was what was taught. But then my housemate, my roommate the next year, he kept saying me, “Oh yeah, that was good. But you should get into this Haskell thing. That’s where it’s really at. And they’ve got this monad thing going on. It’s really, really cool.” And I was resisted for a little bit, but then he showed me how to do a few things. And I said, “Oh yeah, this is really cool. This is really great.” So, he was the gateway into Haskell for me. I then used Haskell in my final year dissertation in my third year. So, that’s when I really got to grips with it and started using it to write larger projects.
So, from that point, I was getting deeper into it. I was starting to read the papers of people at that time. This was about 2005, 2006. So, there was a lot of activity at the time thinking about the expressivity of the type system for Haskell. The idea of type families was just on the horizon, associated type families. So, I was reading those papers and getting more and more interested in the research ideas around programming language design. So, I was thinking about doing a PhD, and that informed the direction I wanted to go in then in my PhD. I was quite interested in parallelization as well and parallel programming, and functional view of parallelism. So, that was really the journey for me. Standard ML opened my eyes, and then Haskell was the thing that kept me going from that point onwards.
WS (0:03:47): So, you did your PhD in England as well?
DO (0:03:48): Hmm.
WS (0:03:49): And that was in Cambridge?
DO (0:03:51): That’s right, yeah.
WS (0:03:52): And who was your supervisor?
DO (0:03:53): Alan Mycroft.
WS (0:03:55): Yep.
DO (0:03:55): Alan has a long career working in static analysis, compilers, functional programming, semantics. And I looked at the work he was doing, and it seemed to hit lots of my interests, so I approached Alan. I had looked at a few different places, and Cambridge is where I ended up.
WS (0:04:14): And what was the topic of your PhD?
DO (0:04:17): Well, like many PhDs, you start off in one place and you end up in another. I went in – perhaps like my undergrad as well, I started in one place and ended up in another. I went in very interested in parallel programming and building programming languages for expressing parallel computation. That was the starting point. But during that time, I got very into the idea of contextual effects or the role of context in programming. So, that led to me spending a lot of time thinking about comonads as a structure that could be used in programming and as a way of organizing semantics. That then led into the concept of coeffects, the jewel to effects. If an effect changes the context, the coeffect is how the program depends upon the context. And Tomas Petricek and Alan and I spent a lot of time, perhaps towards the end of my PhD, thinking about this idea. So, I think my dissertation was titled Programming Contextual Computations, and it was really looking at how we can express programs in terms of their context dependence, and use that as a way to structure programs, and also analyzing programs for how they use the context.
WS (0:05:26): So, I think a lot of people will be familiar with monads and IO and this idea of effectful programming. So, what is a coeffect and how is it different from an effect?
DO (0:05:37): Well, they do overlap in the middle as well, but broadly speaking, a coeffect is the program’s dependence upon the context. And that could be a few different things. That could just be the normal free-variable context. We always have this environment of variables that we have bound. And a coeffect analysis will look at how you actually use those variables. So, do you use them at all? Are you actually demanding the value from that variable? Or how many times do you do it? Where does that value then flow once you use it? Does it flow to some other part of the program? So, using coeffect analysis, which was a general framework that we built, you can track data flow properties of your inputs to your outputs. So, that’s context when it comes to the free variables, but you might have a wider notion of context, like some hardware devices that are available on your computer or some ambient resources like a database or access to a private store or something like that, which you want to access from other parts of your program or control the access in your program.
There are also very more data structure-oriented ideas that you can think about. So, you can see traversals over data structures. There are various different interfaces of various different mathematical ideas that you can use for structuring traversals. Over the data structures, a very common one is the functor idea, where you have a container-like data structure and you want to visit every single element within it. While a comonad gives a generalization to that that says not only can you look at every single element and transform one element at a time, but you also get the context of where you are within that data type within your input. So, a very classic example of this, which I looked at in my PhD, was something called stencil computations, where you want to go over an array. You want to visit every single point in an array to compute a new array, but at each point, you have access to some local neighborhood of elements around you.
So, for example, doing like a Gaussian blur, you want to look at your neighbors immediately up and below and left and right, and take some average of them or some weighted average to compute a new single pixel, or Conway’s Game of Life, where you’re looking at your neighbors and using that to determine the new value. So, in that pattern, it’s more general than the functor, which has only access to a single element. Here, you’re pulling in some context. And it turns out that that is structured by a comonad. Comonads provide an interface that captures exactly that pattern.
WS (0:08:06): There’s a lot of cowords here, so comonads being dual to monads, right, where you have not just a return and a bind, but you can always project out an A, which is the dual of the return. And a cobind, which does something else flipped, I imagine?
DO (0:08:22): Yeah. I can describe it in words, but sometimes you have to see it written down. If you think that the bind is taking something of type A to MB, where M is a monad and that’s saying, okay, I’m going to take in an input A, and I’m going to produce some computation, which has these effects wrapped by the M, MB, and I’m going to lift that into an MA to MB so that I can take in a computation on the input and work out how to combine that with the computation of the output. So, we’re lifting an A to MB into a MA to MB.
Now in the cobind, what you’re taking is a – I use the letter C for comonad, you’re taking a function that goes CA to B. So, now the structure is on the left, that’s the dualization. We flip things around. And so, what you’re taking in there is some data structure which represents the context that you’re in. Rather than an output effect, it’s the input coeffect of the surrounding context. So, you take a CA to B and the cobind lifts that into a CA to CB. So, you can see that as taking a local computation—a computation that happens in local context—and it lifts it to a global context. So, now you go CA. You’re taking a global context. You’re running this function in all of the local context, and you reassemble a global context CB as the output. So, if dualization is about flipping the direction of arrows, that’s where you can see that in the cowrite.
SF (0:09:48): And how did that work in your PhD shift that you did next?
DO (0:09:52): That’s an excellent question. So, I somewhat went in cycles, I think, with this, because in the very early days of my PhD, as I said, I was really into parallel programming, and I was reading a lot of papers about using functional programming as a means for structuring parallel programs. I was just happened to be sitting in a talk one day that was really about something quite different to what I was working on. And I don’t even remember really what the talk was about, but it had people from outside the Computer Science Department in it. And somehow there was a discussion about parallel programming in physics and in natural sciences. And people were talking about MPI, they were talking about OpenMP, which are these frameworks for taking an existing program, typically in an imperative language, and making it parallel. And I listened to this discussion, and I thought, ‘Oh, that’s quite a difficult way of programming parallel computations.’ And I had actually had experience of this. When I was an undergraduate, I had a high-performance computing course where we had to take a fluid dynamics simulation written in C, and our programming task at the end of the course was to paralyze it using MPI, which at the time I thought, ‘Oh, this is going to be fine.’ And then I discovered it was actually quite a tricky problem to solve if you try to do it in multiple dimensions. And I had found that to be a very interesting assignment and quite tricky. And I got there in the end, but it had taken a lot of thought and care.
And then I was listening to these scientists talking about having to do that as a big part of their job, and I was thinking, ‘No, we should be designing programming languages that mean that you don’t have to do this, that you can get something that automatically guarantees this kind of parallelism that is correct by construction. You don’t have to spend weeks like I did, bashing your head against the fact that it’s just wrong and you can’t work out why and have some kind of programming systems that help you do this.’ So, that particular moment quite early on in my PhD was very tied into what I was thinking about at the time and using programming languages as a way of making it easier to write parallel programs. And that is somewhat what led me to the idea of comonads. That particular experience went on the shelf. It went into a box in my memory, and it went on the shelf. And I spent lots of time doing category theory instead in the remaining parts of my PhD.
But near the end, I started thinking about this a little bit again because someone that I knew quite well in Cambridge, an academic who was there, Dr. Andy Rice, he had been talking with scientists within the university. One of the nice things about the way that Cambridge is structured is that it allows people to bounce around between disciplines and bump into each other a lot. So, we have this college system where there are 31 colleges that are technically separate to the university, but they have this symbiotic relationship, and most academics belong to a college. There are undergraduates who are there, and they live there and have a smaller academic community. And the typical thing that you do in a college is you go and you sit down at lunch or dinner. And you just sit down next to the next person at the table. You don’t sit with your friends. You just go sit down next to someone, and you say, “Hey, so what are you working on today?” And you talk across disciplines. And he had had lots of conversations with scientists and ecologists who were bashing their head against code. Programming was now a big part of their jobs, but they were struggling with getting it right. They were struggling with the correctness of it, getting it right in the context of parallel programming.
And he mentioned this to me one day over lunch or coffee or something. And I said, “Oh, yeah, this is definitely a problem. I sat in this seminar a while ago and thought about this as well. And I tried to think about this in the first year of my PhD. There’s definitely something here because computer scientists are not talking to scientists enough. And maybe there’s a little bit of crossover in the HPC domain, but what we’re really missing is some programming languages and programming tools that will actually help them do their job.” And he said, “Yeah, absolutely. That’s what I’ve been thinking as well. Why don’t we try and do a project on that? You’re coming to the end of your PhD soon. There might be some money available. Why don’t you do a postdoc with me, and we can start thinking about that more seriously together?” So, I said, “That sounds great.”
I was getting to the end of the PhD. I really enjoyed the PhD and wanted to do more. Doing a postdoc was the natural step. That’s quite the common thing within the UK to go from doing a PhD to doing a few years of being a researcher as a postdoc. And so, I was really excited to have that chance. And it was somewhat going back to the drawing board, really. I was going out of the things that I knew very well and had built up lots of expertise in to, okay, let’s go back to the drawing board and think about how do scientists even write code and what are the problems that they have. So, we had a couple of years working on that particular problem. We talked to a lot of people within the university, primarily what you would call earth scientists. People looking at modeling the atmosphere or the biosphere and the interactions between them—those are the people that we got talking to. And we looked at their code, and we had long discussions with them about the difficulties that they faced in the day-to-day programming that they were doing as a core part of their job.
WS (0:15:08): So, what kind of problems were they running into and what kind of languages were they using, and how did you sell Haskell to people who’ve never heard of functional programming, essentially?
DO (0:15:20): Well, I’m afraid we probably didn’t do that. We discovered quickly, somewhat to our surprise, initially was that Fortran was very common. I didn’t know a lot about Fortran at the time. And I think that most computer scientists take a bit of a dim view of Fortran. There’s at least, I think, unjustified skepticism in it as a language, and we sat through lots of these meetings and looked at the Fortran code that they were doing and said, “Okay, you’re using Fortran.” We started to see the perhaps sociological reasons why that’s the case. There’s a long history of using Fortran in science. It is very high performance. Modern Fortran has some quite nice features. They’ve moved away from some of the slightly unusual features in the past, which are good sources of bugs. Those have become deprecated and have gone out of the language. There’s been lots of language revisions. You can see modern Fortran as quite a clean imperative programming language that’s slightly safer than C. So, it doesn’t have pointer arithmetic and things like that. Arrays are first class, so they’re part of the language. You can do A + B onto arrays and it does the pointwise addition of the arrays. So, it has some nice overloading. It even has an effect system in modern Fortran as well. So, you can say, “Oh, this function is pure and it checks it. And if it’s pure, then it will do a vectorization.” So, Fortran was the language du jour of science.
The kind of problems that we were seeing was three things, really managing the complexity of the models. You’ve got these very large pieces of software that had really been built by many people over decades who weren’t necessarily expert programmers but knew their domain very well. And so, there were lots of artifacts of that that you could see that made it hard to then add in new features or maintain them. So, there was a kind of accidental complexity problem, which is a big part of all kinds of software engineering, but you could see it there in that scientific context through the lens of then working on also very complex problems. So, there was the accidental complexity, but it was the inherent complexity of the models that they were trying to build.
Then there was a lot of issues around being able to understand the numerical characteristics of the code, how it’s going to perform over long executions, where sometimes error might build up and the model just starts to go to a state which just seems unnatural, unphysical. People talk about a model blowing up. Suddenly, the values just go way too high in this exponential thing. There’s been some runaway of the errors. These are nonlinear systems that you’re modeling, so you can get into just completely unnatural runaway states because of various kinds of error.
WS (0:18:02): Is that an error in the model or in the floating-point arithmetic, or what kind of errors are we talking about?
DO (0:18:08): Well, that’s the question, and that’s what makes it hard to diagnose. There are lots of sources of error. There are inherent error that comes in that you know about due to the numerical analysis approximations that you’ve had to do. You’re introducing some kind of error there. There is floating-point error as well that comes from that next step of approximation. But there might be implementational errors that you’ve made unintentional implementation artifacts. Maybe the parallelization is wrong, for example. Or you might have just misunderstood the science, and you’ve got the model wrong as well. So, teasing those apart we saw was really a difficult challenge.
And then the next thing was really probably just trying to get more information into the code so that it was easier for people to understand what it was actually doing, what the meaning of the inputs and outputs actually are, what the behavior of functions, what their behavior is. And so, we saw that there were challenges around having code that was well described that humans could understand, and that had some way of checking consistency when you’re trying to plug things together and understanding, okay, this variable here, Q, in this model, and this variable Q in this other model that we want to put together, is Q really the same thing? Does it actually have the same dimensionality? Does it have the same units? Does it have the same resolution? Is it actually talking about the same value? And often there is a description problem there between models.
SF (0:19:30): Is there a particular area of natural science you think could benefit most from improved languages?
DO (0:19:37): Oh gosh, I probably can’t answer that question. So, we started down this journey over 10 years ago now, and the people that we talked to ended up perhaps slightly accidentally being earth scientists. But over those discussions, I started to feel quite strongly that this was really the right place that I wanted to be talking to people. I was already quite aware of the environmental challenges we were facing as a species and starting to learn more about the relationship between sciences, climate science, and then governmental decisions, and thinking about how we generate evidence and understand what effects we’re having on the planet. So, to me, it seemed, if I’m going to work with any particular group of scientists, these scientists would be a valuable group to put time into, especially because it’s a very, very heavily computational field and it always has been. Numerical weather prediction and climate science really only exist because we invented computers. And there was a very close symbiotic relationship between the two fields.
In the early days, one of the first things that people did with the public computer resources was to generate numerical weather forecasts. Of course, they had been used secretly during the Second World War for code-breaking. But in the immediate aftermath of that, with projects like the ENIAC in the US, one of the first things that John von Neumann and his team did was, okay, let’s predict the weather with this computer that we now have. So, there’s always been this strong relationship, speaking to earth scientists, climate scientists, physical geographers. You can see that programming is just absolutely central to their work. They spend huge amounts of time programming. And that was perhaps something I just hadn’t really thought about, that actually, I was there as a computer scientist in my office. Of course, I was doing lots of programming and I love writing code. At the end of the day, I am a programmer, a hacker. I just like making stuff. And I wasn’t really thinking about the fact that a few hundred meters away in a different building, there were scientists, and they were spending all of their time writing code as well. And so, part of those early days was realizing, ‘Oh, they’re just like us.’ They just spend all their time programming, but they don’t know about all of these other tools that could help them. And we’re not doing anything to talk about the problems and specific kinds of things that they’re trying to do. So, maybe we should do that.
WS (0:22:09): So, your research has shifted a bit, I think, also in that direction, not entirely, but it’s become an important part of your work where you have this Programming for the Planet Workshop with POPL this year. You’re also director of – I should look this up.
SF (0:22:24): The Cambridge Climate Institute, right?
WS (0:22:27): Yes, thank you. Sam came more prepared than I was.
DO (0:22:32): It’s a slightly different name to that, actually.
SF (0:22:34): Oh, it is the official name. Tell us about your role.
DO (0:22:39): Yeah. So, it’s called the Institute of Computing for Climate Science, based at the University of Cambridge. It’s a multidisciplinary research institute that looks at supporting climate scientists through the latest work in computer science, in software engineering, in mathematics, in machine learning, and programming. So, that really came about on the back of the work that I had done previously. As I said, I did a couple of years of postdoc with Andy Rice looking at this problem. That spun out into a larger project. We had some funding to work with people on this particular problem. We had a project that’s called the CamFort project, which came out of that, where we started building lightweight verification tools for scientists, static analysis tools over Fortran, and then specify and checks verification tools for Fortran. And we had some spin-out projects from that, working with the Met Office, looking at building specialized tools for them to help them analyze their code. Those initial bits of work really set my interest in this area. And a few years later then came this opportunity to set up this institute in Cambridge.
Now we have a lot of people working within ICCS. As I said, it’s multidisciplinary. We have a team of software engineers, research software engineers, they’re called, working within ICCS, who then work directly with lots of climate science groups around the world, helping them with model development, with coming up with new models, with taking existing work and making it better packaged and more sustainable as a piece of software, so it can keep having value and be used by others, working on analysis tools, data analysis tools, and things like that. So, it’s blossomed from the initial work that we were doing into a larger project and institute where we’re working with lots of people now, trying to think about how we go from immediate support, doing things on the ground, helping the scientists right now with software engineering support, then into what are the programming language tools and systems that could help in five or 10 or 20 years’ time.
WS (0:24:44): And that’s an interesting challenge, I imagine, because, like you say, they’re quite used to working in Fortran, and there’s a lot of reasons for them to do so. And then to actually convince them that, well, maybe we should migrate to other tools or systems and not just talking about Haskell, but I mean, to somehow create momentum, create interest into, look, you could do things in this way and somehow get that transition going must be quite challenging for not just technical reasons, right?
DO (0:25:13): Oh, yeah, absolutely. There’s huge sociological human barriers to this kind of thing. I think that I’m not necessarily thinking that I’m going to produce a language which suddenly everyone’s going to use. That might happen, but I’m not necessarily taking that as my goal, because there are huge amounts of engineering effort that need to go into that. And then there’s lots of other factors that go into why people use a language or why people switch languages or start using a language. So, I’m not thinking that that’s the way to do things. I’m also not saying that’s not the way, but you have to be realistic about these things. And I think that that was also a process I went through unpicking what that might look like about 10 years ago or so.
We wrote a position paper. That was called something like a Programming Languages Agenda for computational science, where we did propose a bunch of new language ideas, but we also said, “Look, this probably has to be an evolutionary approach.” You can’t just force people to use something else, but what you could do is build tools that they can use with their existing languages that could provide some of these benefits and really demonstrate why additional features might be helpful. And then I think you still have to do the research into what could those language ideas look like. If no one does that research ever, then we will just stay with the languages that we have. But I don’t really believe that from this point onwards, we’re going to stick with Fortran 2008, Python 3.12, and whatever the particular version of C++ is now. And they’re stuck, and we’re just going to stay with that for the rest of humanity. Haskell has shown this as well. When you have people thinking about new language ideas, then eventually those ideas make it out into other places. They creep into other languages. And so, you can have impact by conquest, by having a language that suddenly everyone starts using, and it does happen, or you can have impact by infection and get these ideas, and they creep in eventually. But you’ve still got to go and have those ideas and try them out and explore what they would be.
So, I think that’s where I’m at in my thinking. We should think about the evolutionary things we could do, what we could provide now that people would actually use in their existing toolchain. And then what are the ideas that we should be thinking about that will go into some language in the future, whether that’s into a version of one of these existing, well-established languages, or into something that is new, that gets enough engineering time and enough momentum behind it, and enough libraries and user base, that it becomes something that people want to use.
WS (0:27:48): A good example of that is you mentioned associated types earlier, and Swift, which is Apple’s big language. They have essentially type classes with associated types. And this would not have happened if in 2005, 2006, Haskell hadn’t messed around with this idea of what happens if we have associated types with our type classes. Now they’ve suddenly become mainstream, essentially. But the question I wanted to ask was, is there any kind of opportunity to apply what you learned during your PhD about coeffects and static analysis and data flow in this setting, or is that not a direction you’re pursuing? Is it more pragmatic looking for how do I solve this problem about fixing a class of bugs in Fortran?
DO (0:28:36): Yeah, this is a good question. I’m pausing for thought because – well, let me think for a second, then I’ll say a really good answer. So, I think when you do a PhD, you get into a particular area and you focus on it very narrowly and you develop lots of ideas there. But also at the same time, you’re learning lots of things as well and picking up other wider skills. You’re learning the general paradigms of your field and how they could be used.
So, the work with coeffects, comonads, and graded comonads, I then took that and really focused on it in a different project, which is the Granule project, where we built a language really out of these ideas and studied that as a language where that was a primary part of how you write code in that language. But in terms of the work with the climate scientists, I’m not trying to use coeffects and comonads in that space directly, but all the other wider things about how you build static analyses and how you understand when they’re correct. and what are the models of these things feed into that discussion.
Now, there are some small crossovers. One of the parts I mentioned is fluid dynamics. Part of any system model, say an atmospheric model, it has what’s called the dynamical core, which is where you solve the equations of fluids and you do a fluid dynamics simulation. And inherently, that is a comonadic computation because you can express it in terms of these local stencil computations that are then turned into global computations. So, there is often – I do look at code and I think, ‘Oh, yes, there’s the comonad sneaking in there in the Fortran.’ And I sometimes think about, ‘Okay, should we use that as a structuring mechanism for some kind of library or something in the future?’ But that’s a side piece, and I’m not specifically using everything from that PhD in what I do now.
SF (0:30:23): So, you’ve not converted climate scientists to comonads. We’re not conquering climate crisis of comonads?
DO (00:30:29): Not yet, but I do think that there are interesting things that one can learn by looking at this categorical way of seeing programming as a tool for thought. There’s something that can be learned by programmers in the numerical programming world in sciences and climate science. So actually, I’m running a Summer School next week, and we do have a session where I’m going to teach about categories, functors, and natural transformations, and looking at – I’m going to use Python as the example in all of those, and using those structures from category theory that many functional programmers in the Haskell world are familiar with and using those as a way of thinking about the properties of programs, what properties we might want to test on our programs, and also optimizations and just bringing that way of that perspective, that way of thinking to give people another tool in their arsenal of how do I understand if I’m writing correct software and how do I understand what its performance is?
So, I definitely think there’s something there that can be exploited by people in this domain. As I said, climate modeling, there’s really, really interesting code going on there. And it’s very complex code. There’s data structures. There’s a lot of numerical analysis work that’s embedded in there. And there’s definitely some of these things that familiar to functional program is going on. So, I’m trying to surface that a little bit with the climate scientists that I work with and saying, “Oh, well, here’s another way of thinking about this.” And people are receptive.
WS (0:31:57): So, you briefly mentioned Granule already. And that’s the other thing which I think many people will know you for. Can you say a little bit about that project? Because it seems to run concurrently with your interest in climate science, I guess.
DO (0:32:12): Yes. So, that project has somewhat run concurrently with these things. I’ve never really thought to myself, ‘Oh, I should only do one thing.’ Perhaps it’s a little bit of a crazy thing to do, but I had worked on the idea of coeffects, and I looked a lot at effects and their semantic models in terms of graded monads and graded comonads, and I had written a number of theoretical papers on those ideas. And in 2017, I was due to give a talk at the University of Edinburgh, and I was writing the slides. It was a relatively quiet period of time for me, and I was writing these slides about the paradigm of grading, where you add this extra information that’s within the types that reflects the structure of the semantics or the structure of the proofs. And I was suggesting that, “Oh, there could be a programming language centered around these ideas where you’d have these extra reasoning powers.” And I had said this in a few places. And I was writing the talk, and really, I was thinking, ‘I am bored of giving this talk. I’m very bored of giving these theoretical talks.’ And I keep saying that it would be interesting to explore a language with these ideas built in. I had a couple of weeks before the talk, and I thought, ‘Why don’t I just try and see what it would be like to make that language? I wonder if I could do it.’ I thought, ‘I like programming. I know Haskell and I’ve used Haskell for lots of things. And why don’t I sit down and just try and make a language implementation with these two weeks?’ And it was a little bit of a crazy idea.
But after two weeks of hacking, I actually did have this language prototype. Originally, it was called Gram, and then it got renamed to Granule not long afterwards. But I wrote this small functional language. It was a little Haskell-like in its syntax, and it had strong static typing, but it had these graded types as part of it. And I used the Z3 SMT solver to solve equations on those grades. And it was just a small, little demonstrator. It was a lambda calculus core with some built-in data types.
And in the end, the talk that I gave at Edinburgh, I basically mostly just did demos with this little language implementation and talked about where it’s come from, the theory. And it was like all of this work that I had done suddenly came alive again in my hand having that implementation. I had an undergraduate intern, and I showed it to him, and he was, “Wow, this is really cool. This is really exciting. Let me do some of that as well.” And he started working on it in the summer. And that just was really exciting to have the theory, but now to have it real. And immediately, all of these other problems and ideas started popping out at us once we could play with it and write programs.
So, that became the Granule language. It was 2017, really, that we started it at that time. That particular student, Vilem Liepelt, became my PhD student and worked on this with me. He did his final year dissertation on this and looked at how to mix this with GADTs. And we put together all of the things that you needed to have a usable functional language, but with the idea of grading for both effects and coeffects. And we had an ICFP paper about that in 2019. And that just became a really interesting research vehicle. And I took inspiration from what Haskell had done with the GHC compiler, having this place in which you can try out ideas. And this was, okay, this is my place to try out ideas. And so, that pulled in a number of other students, and I had some funding, got some government funding to work on that. I had a postdoc work on this as well. So, that snowballed a bit into a larger project. We tried out lots of things with Granule over the last few years. And that was somewhat – again, it was like one of these cycles. I was taking the things that I had done in my PhD, but now I was doing them in a new way. And that’s been really interesting and really rewarding. I think we’ve come up with lots of interesting ideas there. At some point within that process, the climate science work started heating back up again. So, it was another one of these cycles. And I thought, ‘Well, that’s fine. I’ll just do the things that I enjoy.’ And that’s the beauty of being in academia, really. No one’s telling me, “No, you shouldn’t do that.”
WS (0:36:27): I think a lot of people know what monads are, but what are graded monads, and are they the same thing, or I don’t really know?
DO (0:36:35): Again, this is something that helps to have a whiteboard for, but let me try and give you the podcast version. So, when you have a monad, you have a single type constructor, the type constructor over which you’ve got this monadic interface. And you can essentially think of this as giving you a way of classifying computations in a binary view. So, say you’re thinking about the IO monad and you have pure Haskell programs, and then you can put the IO monad in there to represent when you have impurity and some very large set of possible effects. So, you’ve got this binary view that your type system gives you now. Either you’ve got things that are pure or you’ve got things that are side effectful.
So, a graded monad, instead of having a single type constructor, has an indexed family of type constructors. So, it has lots of type constructors, and they’re all related in some way, and they have an index to denote which particular type constructor is. So, you can think of it as a constructor that has a parameter of some other set. Let’s call it I. that’s your indexing set. And given a particular I, then you get a type constructor back. So, rather than having just an IO constructor, perhaps you have a whole spectrum that says, “Oh, here’s a constructor that represents just reading from some state, and here’s a constructor that represents writing to a state, and here’s one that represents reading and writing, or here’s one that represents exceptions.” And so, rather than having a binary view, you have a much finer spectrum of possible effects that can be represented here. And you then, as a user, can distinguish those different kinds of effects rather than just having this all or nothing. You can see all the gradations in between.
So, what a graded monad then does is it has a structure that’s very similar to a monad, but it connects the different index constructors together. So, when you have the return operation, what you do is that you construct a value using some particular defined point of that space, which represents pure computations. So, one particular constructor in that index family is going to be the thing that represents computations which are trivial that don’t have any side effects. So when you do return, you’re constructing in that particular constructor. So, you can think of it as like the IO zero, like it doesn’t actually do anything.
And then the bind, it interacts the indices, and we have some structure on the indices. You have some operation on the indices that lets you combine them together and say, “What does it mean to have something with side effect X, something with side effect Y?” And then they get combined to X times Y. So, the structure of doing returns and binds then gets reflected into the indices. And you can see this then as the indices giving you an analysis about what the effects actually are that are going underneath this thing. So, it has a very strong relationship to effect systems and that part of the literature.
WS (0:39:21): So, a very concrete example might be something where you want to track the set of all files that you’re reading from. And then if you return, then the set is empty, but if you have two computations, you run them in sequence. You take the union of all the sets of files that either computation happened to access. Is that fair?
DO (0:39:39): Perfect. Yeah, that’s a good example.
WS (0:39:40): Okay. So, another thing I noticed that you published on is Program Language Evolution, or you organized a workshop on that. I mean, you’ve been using Haskell for many years, even to develop your own language, I suppose. So, how do you see Haskell evolving or the wider ecosystem of programming languages? And we touched upon this briefly when we talked about climate science, but maybe you have thoughts about how you see programming languages heading in the future.
DO (0:40:11): That’s a tough one.
WS (0:40:12): It’s a very broad question.
DO (0:40:16): There’s two questions in there, I suppose. The Haskell’s evolution and programming language evolution in general. I think in general, we’re seeing that – well, okay, it’s always difficult to predict the future. You can look at what’s happened in the past and you can try and extrapolate, right? And we’ve seen programming languages become multi-paradigm. You look at the popular languages. They have evolved themselves by bringing in ideas from other places and bringing in functional programming ideas. So, you look at Java, still a very popular language, but it didn’t start off having many functional things at all, but now it has parametric polymorphism that got added in, then they added in first-class functions. It’s grown by bringing in ideas from functional programming. And I think most major popular languages have functional programming aspects to them. They have something of the functional programming paradigm in there or function, first-class functions, function first style programming. And I think there’s an increasing then picking up of the ideas around the data model that functional programming brings. Yeah, algebraic data types are really one of the – and another really great thing about functional programming is maybe the functions are the less interesting. It’s this really strong data model of algebraic data types and then generalized algebraic data types that has started to have impact on other languages. So, you see pattern matching coming about in Java. And the ideas in Rust that are heavily based on algebraic data types. So, I think having more of that structure of the data and being able to derive your programs from that structure is something that is becoming more popular and will continue to do so.
It feels to me like object-oriented programming has diminished slightly, and it’s become less of the primary thing that people are doing in this mainstream space. It’s still there, and you can still see that it’s useful in some places, but it’s rather than that being the dominant way of doing things, actually this much more mixed landscape of, well, sometimes it’s functional, sometimes it’s imperative, sometimes it’s object-oriented. That’s the kind of space that people are ending up in.
I would love to think that more of the ideas from Haskell will bleed into other languages and having ways of enforcing guarantees about your programs or optionally and gradually being able to ratchet up the level of guarantees that you get via type checkers and via extended type checkers with other kinds of solvers. I think it would be great to see that grow, and it is growing somewhat. I think having something that’s gradual and people can slowly add to something and evolve a piece of software and increase the level of trust a piece of the time, I think that’s where I’d like to see things heading. And I think they are heading in various places. So, that’s probably language evolution.
Now, of course, we’re entering into this phase where AI assistants are becoming very popular, and one could speculate about how that’s going to influence languages and programming going forward. To be honest, I’m not really sure what that’s going to look like. I think we’re in this transitional stage where it’s a bit difficult to predict the effect on programming. Certainly, it seems that having AI assistants can be useful for speeding up programming once you’re well-versed in what you’re doing. It certainly seems like that’s the case. And it can be useful then for generating certain bits of your code. And maybe a particular use case at the moment would be using it to generate tests. I’m always encouraging people to write tests in their software, and it’s a way of perhaps speeding that up, but it’s a bit of a double-edged sword at the moment because you can put too much confidence in it. And even when you’re not using it to generate your actual code, but you’re using it to generate tests, well, are those tests right? Is the specification correct?
So, we’re in this interesting transitional phase. It’s not clear yet to me what influence that’s going to have on languages, but I think it is going to have some influence. I’m just not quite sure yet what that will be.
WS (0:44:26): And Haskell specifically, do you still use Haskell in day-to-day work at all?
DO (0:44:31): Oh yeah. Yeah. No, I use Haskell a lot. If I ever need to make something, I’m usually dusting off Haskell, sometimes other things. But I have a new language project prototype brewing at the moment, and I used Haskell to build that because Haskell is great for building language tools. I still use Haskell actively in a few other projects that are in a maintenance phase, perhaps, but they’re all developed in Haskell. So, it continues to me to seem an extremely powerful language. And the features that have been built up in the GHC Haskell space have really opened up what you can do with the language and continue to push our understanding of computation and how to structure computation.
Part of Granule’s work is related to linear typing, and so it’s been really, really exciting to see the linear types extension in GHC come on stream and gradually maturing. And I’m hoping that that will become something that can be more widely used in the future as well to write idiomatic functional programs, but then that have this safe mutation inside of them that can be leveraged for high performance.
One of the projects we did with Granule was to look at Rust-style ownership and borrowing and lifetimes and how you can do that in a functional way. And we have a graded linear functional view on that within Granule, and I’d love to see some of those ideas make it into languages like Haskell as well. So, my other mission perhaps is that conquest by infection from a really niche language like Granule into Haskell and bring across some of the ideas in Granule. Because the linear types extension in Haskell, the way it works underneath is via a graded type system. It’s like a very specialized core of what Granule has. So, Granule, you can do lots and lots of different kinds of grading for linear types in Haskell. It’s a smaller, specific example.
WS (0:46:21): And what kind of applications would you be looking for linear types and high-performance computing, or what were you thinking of?
DO (0:46:30): Well, I did think it would be interesting to see what it would be like to write a small climate model in Haskell and try to approach the kind of performance that one gets in Fortran. Almost as a thought experiment to see what’s it actually like and why isn’t functional programming used in these domains, or what are the gaps in expressivity.
With one of my PhD students, Daniel Marshell, we started trying to do this using the linear types extensions to take a well-known intermediate complexity weather model and re-implement it from Fortran into Haskell, using these extensions and seeing if that could work. It’s a work in progress, and it hasn’t been as smooth as we would have liked, which is interesting, which tells us something about the languages. And it’s trying to find the right patterns and the right idioms in Haskell, and particularly the linear Haskell way of doing things that gives us what we need. So, that’s really a bit of an experiment to see what is this expressivity gap between the two.
I think that Haskell as a programming language continues to be a really exciting project and a really exciting language that has this dual function as both a research vehicle for new language ideas, but also a really serious, high-quality compiler that can be used to do very important core, serious work. And I know lots of people use it in their day-to-day work and in industry and in context where there’s software deployed using Haskell. And I think that’s an amazing result for the Haskell language. And I hope it continues to be used in many places. I think it’s having an increasing influence on lots of other languages, and there are spinoff-style languages, things like PureScript, that have taken a lot of the core ideas and built something that is new. And I think that’s a great place to be for Haskell. And I think it will keep influencing languages in the future. So, I hope that more people do get into Haskell and are influenced by its way of doing things. It will have its own route in the future to developing in new ways, but influencing other languages in other ways as well.
WS (0:48:40): Thanks. I think that’s a great place to wrap up. So, thanks for your time, Dominic.
DO (0:48:45): Yeah, no worries. Thank you very much for having me.
Narrator (0:48:48): The Haskell Interlude Podcast is a project of the Haskell Foundation, and it is made possible by the generous support of our sponsors, especially the Monad-level sponsors: GitHub, Input Output, Juspay, and Meta.
