BLURB

Richard Eisenberg is one of the core maintainers of Haskell. He recently joined Jane Street’s Tools and Compilers team, where he hacks on the OCaml compiler. He and Ron discuss the powerful language feature that got him into PL design in the first place—dependent types—and its role in a world where AIs can (somewhat) competently write your code for you. They also discuss the differences between Haskell and OCaml; the perils of trying to make a language that works for everybody; and how best a company like Jane Street can collaborate with the open source community.

SUMMARY

Richard Eisenberg is one of the core maintainers of Haskell. He recently joined Jane Street’s Tools and Compilers team, where he hacks on the OCaml compiler. He and Ron discuss the powerful language feature that got him into PL design in the first place—dependent types—and its role in a world where AIs can (somewhat) competently write your code for you. They also discuss the differences between Haskell and OCaml; the perils of trying to make a language that works for everybody; and how best a company like Jane Street can collaborate with the open source community.

Some links to topics that came up in the discussion:

• Dependent types
• GHC
• Unboxed types in OCaml
• Language extensions in Haskell

TRANSCRIPT

00:00

Ron

Welcome to Signals and Threads, in-depth conversations about every layer of the tech stack, from Jane Street. I’m Ron Minsky. It is my great pleasure to introduce Richard Eisenberg. Richard’s a senior contributor to the Haskell ecosystem. He’s worked on Haskell’s type system in a lot of different ways over the last eight years. He’s on the GHC Steering Committee. He’s the Chair of the Haskell Foundation. One might wonder, what’s he doing here? Well, it turns out Richard has joined Jane Street. He’s working on our Tools and Compilers team, and in particular, working on the team that works on the front end of the OCaml compiler. So, thanks for joining me, Richard.

00:39

Richard

A real pleasure to be here.

00:41

Ron

So, maybe a good place to start out with is to talk about your background. You’ve done all this exciting work in the Haskell ecosystem. Maybe tell us a little bit more about how you got involved in Haskell and what kind of work you’ve done there.

00:51

Richard

Yeah, sure. I first really encountered Haskell when I went back to graduate school. I’d been a high school teacher for a little while and then I thought, ‘oh, you know, it’s time to get a Ph.D. in programming languages,’ kind of, as you do.

01:02

Ron

Mm. (laughs)

01:02

Richard

In the process toward that, I discovered dependent types. I didn’t wanna just show up in grad school and not know anything. So I did some background reading and I discovered that, you know, these fancy type systems have so much expressiveness, and so much of a way of being able to sort of define what it is that you’re programming before you even write a line of code, that you can just express your ideas so much more clearly and then get the compiler to check that you actually did it correctly. This was just sort of, you know, my brain exploded when I learned about this.

01:32

Ron

I feel like, you know, I kind of pretend to know something about programming languages on TV, but like, actually my academic background is distributed systems, not programming languages, and there’s lots of gaps in my knowledge. And so, I kinda don’t really know what dependent types are. Can you give a suitably beginner-friendly explanation of what dependent types are?

01:48

Richard

Sure. And I’m gonna start by avoiding the trap of trying to define the term, ‘dependent type.’

01:53

Ron

(laughs)

01:54

Richard

And instead, just sort of describe ‘a language with dependent types allows you to do this thing.’ And that thing is to essentially encode a proof of correctness into your program such that every time you compile your program, that proof is checked. And so you know—if you’ve set things up the right way—that your program does what you think it does. And so, I’ll give a concrete example.

And that is, to imagine a sorting function. So normally we think of a sorting function, let’s just say, it’s a function from a list of ‘ints’ to a list of ints, right? It takes this list of ints’ input, and then does some transformation, and then produces a list. But actually, that’s a very loose description of a sorting function. We can do better than that.

I wanna say that a sorting function takes in a list of ints, and it produces a list of ints in, I’m gonna say, non-descending order (because maybe there’s duplicates, so I don’t want to say ‘ascending order’ because someone out there might say that’s wrong). So we get this list out that’s in non-descending order. Okay, that’s closer, but that’s still not quite right because maybe my function just always returned to the empty list. That’s a list in non-descending order.

So instead, I really want to say that it’s a function that takes in a list of ints, and returns a result that is in non-descending order, and is a permutation of the input list. And that’s a rather glorious type that I can assign to a sorting function. But it accurately describes what that sorting function does.

And then I can implement that in any number of ways, using any of the common sorting algorithms that you learn in computer science, and any of those different algorithms will meet that specification, and then, if I’ve encoded this, my compiler will check that my algorithm actually does sorting and doesn’t do some other thing. And so now, having sort of explained that, I can return back and actually say what I mean by ‘dependent type.’

A dependent type is a type that can depend on some input that you give into a function, essentially. So, in this case, the output of the function, not just a list of ints, but the output depends on the input. The output must be a permutation of the input. And so, that’s the dependent type.

So when I started grad school, then I saw Haskell, and here was a language that had this fancy type system and had all this expressiveness. Didn’t quite have dependent types, but it had a lot of that stuff. That just got me excited. And then, through that I started working with Stephanie Weirich at University of Pennsylvania. She was doing a lot of Haskell work. She collaborated a bunch with Simon Peyton Jones, who then I started collaborating with, and things just sort of took off from there. It was a pretty fast introduction into that world.

04:18

Ron

I wanna go a little deeper on that. I feel like we’ve started with the, like, ‘Well, of course I got a Ph.D. in PL and was interested in dependent types.’ Like, how do you even get there? Where does your interest and background in programming languages come [from] in the first place?

04:30

Richard

So, once upon a time, I wanted to program. I don’t know why I wanted to program. I was too little to have that level of introspection.

04:37

Ron

(laughs)

04:37

Richard

So I guess, uh, I learned Basic when I was, I think, five somehow. There was a friend of my parents that decided I should learn Basic and so that happened.

04:46

Ron

(laughs)

04:46

Richard

But I then got more into it, I guess, when I was in 7th grade, so this was, probably I was 12 years old. And someone told me that Pascal was a good language to learn. So, you know, I pleaded with my parents and eventually they bought me the Pascal compiler ‘cause back in those days, you actually had to pay for compilers. At least on, sort of—we had a Macintosh. If I had some kind of Unix system, maybe it would’ve been different.

05:07

Ron

Well, which Pascal compiler did you use?

05:09

Richard

Um, THINK Pascal? Was that a thing?

05:12

Ron

THINK Pascal, so not Borland. I guess Borland was more in the, like, DOS side of the world.

05:17

Richard

Yeah, yeah. Borland, yes, Borland was for like, ‘real programmers.’

05:19

Ron

(laughs)

05:20

Richard

So I got this, and somewhere along the way, I had decided that every piece of software should be, like, if you read the instruction manual, that should tell you everything you need to know about that piece of software. I don’t know why I assumed that, but that was my starting point. And so, it came with these two big books and most of the books were just like on compiler flags and setting up projects and none of this stuff about programming. At the end of one of the books was a syntax reference with no glosses, no further information, just a syntax reference using those, sort of, block and line diagrams to represent recursive loops in the syntax. And I was like, ‘Okay, well, if my assumption is that this book defines how to program, and this is the only thing it has, then all the information must be here.’

So I just stared at these syntax diagrams probably for hours and hours. Like, ‘Okay, what does all of this mean?’ And then eventually sort of bootstrapped my way into learning how to program Pascal. And so, that being my first ‘real programming experience,’ somehow that built the structures in my brain just around syntax and languages, and it kind of went from there.

And then fast-forward 10 years or so, and I took a PL course as an undergrad from Norman Ramsey and it just lit me up. It was just like, this is really cool stuff. I really enjoy this kind of thinking. And it turned out, I took that at the end of my senior year of undergrad, and so it was sort of too late to immediately go into grad school at that point and I had this whole machine going toward high school teaching. So I did that for a while, but then I ended up returning.

06:45

Ron

I love that your entrée into programming was, roughly speaking, a traumatic experience with syntax. That seems… (laughs)

06:51

Richard

But it wasn’t traumatic. It was fantastic. Somehow, this was just what I needed. This was what my 12-year-old-self needed: big syntax blocks.

07:00

Ron

(laughs) Okay. So, you went off, you got your Ph.D., you started working on Haskell. Where did it go from there?

07:07

Richard

Well, I was working on my Ph.D. It was basically, Stephanie and I had this idea about how to encode dependent types, but it required some more support from the Haskell compiler. And so, I was pleading [with] the Haskell people to create this for me. And then, eventually Simon just wrote and said, ‘Why don’t you just do it?’ And that was a new concept for me. I was like, ‘I could influence this language? Well, you know, I’m just this random person.’

But between Stephanie and Simon mentoring me, I got to a point where I could contribute and then it just grew from there. So, [I] did a bunch of that as a Ph.D. student. Then after leaving my Ph.D., I was a professor for a few years at Bryn Mawr College. What was great about that experience was, they were open to the idea that open source contributions were a form of publication, right? A lot of professors have a lot of pressure to keep producing papers. That was definitely there for me, too. But alongside papers, I couldn’t just do software. But I could do, sort of, traditional scholarly publications and software. So that gave me a chance to continue my implementation work, remain a part of this open source community, while still doing the high-level scholarly research that I had been doing. So that was a really nice part of it.

It turned out that, to my great surprise, that—well, this wasn’t to my great surprise—it turned out that this was a lot of work. That maintaining a research program with a bunch of papers every year, and doing these open source contributions, and teaching, there was just more than could comfortably fit into one job, especially during term time. And to my own surprise, I realized that the teaching part was the part that maybe I could pause on. I had done that full-time as a high school teacher for eight years, now I was back doing it. It was fun, but I thought it was time to sort of push in a slightly different direction.

So after a couple years at Bryn Mawr, I left to join Tweed which is a software consultancy based in Paris. They do a ton of Haskell work. And they hired me, basically just to continue my contributions in the Haskell space. So, I continued doing research there, continued contributing to the compiler there. And, you know, after a few years of that, that was fun, and I got to a point where I was looking to be part of a cohesive team all working together, and realizing that after so many years just working in one language, I was really ready to see what things were like in a different space. And so the timing worked out really well when you, Ron, reached out to me and started the discussions that led to me joining Jane Street.

09:26

Ron

Right. And often in these interviews, I’ll ask someone, like, ‘so how did you get here?’ But actually, I was part of the dramatis personae of how you actually arrived.

09:33

Richard

You were the—the dramatis personae, yeah. (laughs)

09:37

Ron

(laughs) Right, which is, at some point, I was like, ‘oh, it would be really good if Richard worked here,’ and I started reaching out and trying to convince you to come. Which took, it’s important, I calculated, 11 months from (laughs) when I started.

09:48

Richard

Yeah, yeah. That’s right. I mean, you know, of course the story [of] me coming to Jane Street starts with you asking me, and me saying ‘No.’

09:54

Ron

(laughs)

09:55

Richard

And again, it was a matter of timing. I’ve been aware of Jane Street for a long time, been sort of wondering what was happening over there, and somehow when you first reached out, it just wasn’t the right time for me yet. And then the second time, it was sort of a better time. I couldn’t even tell you why. It’s just, this is the way that life flows.

But, you know, one of the barriers which we’ve joked about is that I grew up in the New York area and actually ended up going to high school in New York and commuting from New Jersey. So every day I was going back and forth across the George Washington Bridge, and swore to myself then that I would never commute to and from New York City. And also just sort of had this negative vibe from the financial industry, and I was just like, ‘I don’t know. Like, I want to be creating something that other people use,’ right?

But actually, this is fantastic. I’m having great fun. Part of it is that I’m working as part of this larger ecosystem. It’s not just a closed thing where I’m only doing stuff that’s internal to Jane Street. But instead, contributing to this open source ecosystem, working on an open language, OCaml, and really continuing some of these research trends that I started 10 years ago. Now that I’m here, it just all fits very naturally together.

11:01

Ron

I feel like, in general, one of my takeaways is that there’s lots of interesting work in lots of different places and the preconceptions you have when you are young often (laughs) don’t work out over time. So a thing you talked about earlier is a topic that I feel like I should know something about, but don’t. I like your first high-level description ‘cause it actually lines up with the very little bit I know about dependent types.

And there’s also something that’s always made me a little nervous about them because a basic fact about proofs is—proofs seem pretty hard to construct. People go to great trouble to build automated proving systems where you have tactic libraries, like, little tiny programs that you can run to, like, ‘try this way or try that way’ of coming up with a proof of a thing. And it all sounds really hard and when you talk to people who do kind of theorem proving on large scale software systems, it sounds like a pretty challenging operation where this is kind of a lot of engineering work that just goes into just constructing the proof. So I’m curious how you think of the practicalities of that? Like, how convenient can you make it? And if you make it a deeply embedded part of the programming process, does that work well with the other things you might wanna do? Does it interfere with the ordinary process of programming? How do you see the pragmatics of that working out?

12:08

Richard

Yeah, that’s a great question. And this is a question that doesn’t have an answer yet. This is, I think, still something that the programming languages community is grappling with. I have my own takes, but this is still sort of an open question out there.

I think, first of all, that for a programming language to be effective, everything needs to be opt-in, right? If you have a language that supports dependent types—and there’s a bunch out there. So actually, OCaml’s module system is a dependent type system. It’s missing one or two key features that makes it really sort of go. But that definitely has aspects of dependent types in it. Haskell has aspects of dependent types.

There are other languages, Coq, Agda, Idris, Lean, these are the ones that really have embraced dependent types. But in any of these languages, you don’t have to use these dependent types. You can just write a sorting function that is described as ‘a list of ints to a list of ints.’ That’s fine. And I think that’s a key aspect of any kind of system that’s gonna be using this dependent types feature, because not everyone wants to prove everything all the time. As you say, proofs are expensive. And so, what you need is, you need the ability to only prove the parts that you think are worthwhile proving.

So let’s say we have an important part of the system that might be easy to get wrong that we want to prove something about. How do we do that? Is that still worth it? And one thing to think about is, what’s your cost-benefit analysis, right? If you do this proving, can you spend less time on testing? Can you spend less time on debugging? Can you spend less time on catastrophic failure because you missed something when debugging?

It is a lot harder to do these programs with proofs. But sometimes, that’s really worth it. It’s a matter of applying good taste, like it is everywhere in programming, right? Any programming language gives you a ton of tools to work with, and it takes time and experience and taste to figure out when it’s time to use which tools.

13:53

Ron

Right. And I do really like that, kind of, pay-as-you-go kind of attitude of, like, you want some kind of base language that’s relatively simple to work with, and then the ability to add on more features that give you more power of various kinds, and not be forced to pay for that complexity constantly in everything you do. Which is, I think, actually a really hard thing to get right in the design—of like, not having these more powerful features leak in and corrupt the rest of your experience within the language.

14:17

Richard

That’s right. It’s a very careful thing. And my push in Haskell has been to try to increase or add new features to help support dependent types, and there’s been a large community of people really excited for this. And in my measurement, my biased measurement, a smaller community of people who have been saying, ‘No, no, no. Don’t do this because it’s gonna make it impossible to write simple programs.’ And many, many, many times, I’ve had to reassure people, ‘No, no. All those simple programs will continue to exist, they’ll continue to work. You can do what you want.’ But I also wanna give power to people who want to use the fancy dependent types.

14:49

Ron

Great. Okay. So let’s leave Haskell and dependent types behind for the moment because that’s not primarily what you’re working on here. Maybe you can tell us, what are you working on here? Like, what is the mission that you are on here, working on OCaml?

15:01

Richard

So, I’ll start more broadly and then I’ll get narrower. My broad mission is my belief that type systems are a fantastic way to structure thought and structure programs. So by being able to write down what you intend to do before doing it, then you can check what you’ve done, and you can also help formulate your thoughts. And when I say, ‘write down what you intend to do before doing it,’ I mean, write down a specification in types.

The flip side of that, is that it must be the case that you can do that without paying a one-time cost. It’s gonna be problematic if you want to write an efficient program, and yet, by defining your program carefully ahead of time, now it’s no longer as efficient at runtime. This checking and this writing of a specification should all happen at compile time. This should be happening in front of the programmer and not in front of any users. If any of those details leak into user land by slowing your program down or somehow interfering with the operation of your program, then there’s a misdesign in the language.

So coming down to what I’m actually working on here at Jane Street, so the feature I’m working on is something called unboxed types. There’s various different ways of characterizing it, but one way to do so is, it allows inlining of type definitions. So what we might want to have in our design is to have a structure that has four fields that describe some aspects of a trade. And then maybe we store that structure in some larger structure, and maybe that’s stored in some larger structure.

Well, if you do that the naïve way in OCaml, every time you store one structure inside of another, it’s stored by a pointer. And it means now when I wanna access the price of this trade that’s all the way down (it’s a nested structure) I have to follow this pointer, then that pointer, then that pointer, then that pointer, each time I have a cache miss, each time I have to load into memory. This is really bad.

16:46

Ron

Right. And this highlights a kind of basic fact about OCaml, that it has a very fancy, at least on the scale of modern language that people might use, a very fancy type system and a brutally simple memory representation. OCaml’s internal implementation might have been like a Scheme or Lisp written in the mid-‘60s or something, which is to say, everything looks like either some immediate value, it’s no bigger than a word that fits in a register, or a heap-allocated value, which is like one header word and then one full word for every slot inside of it, and we have all the fancy, like, type goo on top of it that you want, but all of the physical representation looks just like that.

17:23

Richard

Exactly. Exactly. It means that we’re building this beautiful type discipline in our software to try to avoid errors, and try to express ourselves, and try to communicate more clearly among developers—and we’re paying for that at runtime! This is ridiculous. To me, every time a type system feature slows down your program or otherwise interferes is just a misdesign. And so, the fact that this is our current state of play is problematic. The task I’m working on is coming up with a new design for OCaml’s type system, or this aspect of OCaml’s type system, that allows us to have this rich type structure without paying for it at runtime.

17:56

Ron

That’s right. Although it’s not that you can pick a type structure that’s kind of oblivious to the performance details, right? In some sense it’s the opposite. The idea of the unboxed type work and a lot of the work that we’re doing now is really about taking design decisions that have to do with performance and making them explicit at the level of types.

18:13

Richard

Yes, that’s right. Because you can’t, I mean, in the end, we need to execute this somehow. There needs to be an execution model. And so, if we try to ignore all of these execution details in the type system, then there’s not gonna be a way of making it fast. And so, the work is, in some sense, taking some of these execution-oriented details, making them manifest in the type system, getting programmers the ability to write types that take these into account, so that we can then execute fast.

18:39

Ron

Right. In some sense, I think of this as really being about enabling performance engineering, right? There’s kind of two different lines of people thinking about how to optimize programs via compilers. One is, you make your compiler smarter so it can do more and optimize things for you. So the user can write kind of an ordinary program that just reflects, ‘what do they want to achieve and what’s the logical structure,’ and then the compiler will, like, do something good. And then, the other direction is trying to give a lot of precise understanding to the programmer so they can know exactly what they’re doing and they can optimize their program. And these are both important.

But, like, in some sense the scale of optimizations are very different. Like, if you come up with a way of making your compiler faster that, like, takes most user programs and makes them 20% faster, that’s an enormous win. Like, that’s a shockingly good outcome. Whereas, if you give people good performance engineering tools, the idea that they can think hard about a particular program and make it five, or 10, or 100 times faster is like, in some sense, totally normal. And so, there’s a kind of extra power of giving individuals the ability to optimize. It obviously misses out on scope and there’s something great about being able to go and in one swell foop (laughs) make 20 different, or 100 different, or all the different programs faster. But you can’t get the same kind of order of magnitude of improvements that you can get from giving one programmer the ability to really carefully engineer their system.

19:57

Richard

Well, there’s a real tension because what in the end we’re doing in programming languages is, we’re trying to find a way for humans to communicate precisely to computers. And we have at our disposal our tool, one of our tools is the fact that this is happening on a computer. So we can write computer programs to try to sort of help cover this distance, right?

In the early days, humans were just completely at a disadvantage and the humans wrote in assembly code. And this was kind of terrible. And we’ve come some way since then, and so now instead of writing sort of instruction-by-instruction that’s gonna be executed by the processor, we can write in a high-level language and have a compiler translate that high-level language to something that the computer can execute. Hopefully along the way, it can actually make that faster. But sometimes, we’ve gotten ourselves sort of too high-level. If we abstract away too many of the details of execution, it’s exactly as you were saying. It means that the programmer can no longer do the performance engineering. And so, we need to expose just enough to the programmer so that now there’s some more details that they can think about. Now they can do that performance engineering.

But still, I think the burden sits on the compiler to take those few hints that the programmer gives to make blazingly fast code come out the other end. And it’s just really about this interplay between how many details do we wanna expose? Certainly not all the details because that’s too hard for the programmer. But we need to expose some. And so, it’s about, over time, programming languages developing more and more features that sort of figure out the right line and the right balance between this desire for high-level languages, closer to human thought, and low-level details, easier to execute.

21:33

Ron

So, before when we were talking about dependent types, we were talking about how it’s important to have this kind of pay-as-you-go phenomenon, like, it gets harder as you try and get more power. It feels like the same kind of thing shows up here.

21:44

Richard

Absolutely.

21:45

Ron

So, when you try and get more control over the shape of data in the way that you described, what are the trade-offs? And how do you think about designing the language in such a way that you don’t have whatever extra complexity is there infect everything that you do?

21:59

Richard

Well, we have to be really careful. So, with unboxed types, one of the challenges is gonna be that unboxed types interfere with polymorphism. So, in a language like OCaml, you can write a function, say, that computes the length of a list. And that’s gonna work over a list, no matter what the list contains. And so the way that we say that, is that in the type of the length function, there’s a type variable. We say that it’s an ‘alpha list’ where alpha can stand for any type that you might wanna put in there. Once we introduce unboxed types, that no longer works out. Some of these types won’t be suitable replacements for alpha. And so it means that, by having these unboxed types in the system, now this really powerful feature of polymorphism becomes constrained. And so, algorithms that people are used to being able to use everywhere, no longer work so well.

So one of the challenges that we have is, how can we recover that? How can we still keep this nice feature of polymorphism and without having unboxed types interfere? And so, one of the things that we’re thinking about doing is some amount of essentially what could become runtime code generation. It comes down to building experience with the feature. As we start understanding this language feature better, we’re going to create programs using these unboxed types, recognize areas in which the current programming paradigms that we engage in no longer work, and then figure out ways around them. It’s this give and take as we’re doing the language design.

23:20

Ron

And just to focus in on this code generation thing for a second, the basic issue here is that the way you make in OCaml today, separate compilation of work, and make the ability to write a function in one place and use it polymorphically on lots of different types is, again, you’re just kind of taking advantage of this rock stupid memory representation. Like, what’s a list? A list is a collection of heap-allocated values, every one has, like, two slots. One is a place to put the data and the other is a place to have a pointer to the next thing on the list. And when you iterate over it, that thing always has the same shape, it always has the same number of bytes, and so you could just write one piece of code that kind of uniformly walks over it. And what happens in the unboxed types world is, suddenly you want the system to contemplate multiple different possible shapes of the data. And so, kind of at a mechanical level, you need different machine instructions in order to do the walking of the data structure, depending on what that structure is.

And so, that’s how you might end up with wanting code generations. The way to kind of claw back the polymorphism is to generate the code. Maybe you can generate the extra code at compile time, maybe you have to generate the extra code at runtime. But you somehow now have to generate code for multiple different scenarios that essentially represent different physical shapes of the data.

24:33

Richard

Exactly. And right now, our best thought is that this will happen at compile time, that we’ll be able to figure out what code we need to generate at compile time. That will prevent a few programming idioms that someone might potentially want. I don’t think anyone will ever want those (laughs) idioms in practice so I think we’ll be able to get away with it. But it does mean we’re thinking carefully about this design and it’s a hard thing. I’m not aware of another language that’s really tackled the problem in the way that we expect to tackle it over the next few months.

25:01

Ron

So another language I think is interesting to compare to, in all of this, is Rust.

25:04

Richard

Sure.

25:04

Ron

So Rust is a language which tries really hard to do two things at the same time which are not trivial to do at the same time. One is to give stronger sense of type safety so that you can write programs that you’re confident aren’t going to crash, so you get lots of protection from bugs from the type system. And also give the user a lot of control over low-level details over how memory is managed. And we’re essentially trying to push OCaml in some sense at that high level of description in the same direction.

25:29

Richard

Sure.

25:29

Ron

How do you think the Rust approach differs from the approach you see us trying to take with OCaml?

25:34

Richard

This is a good comparison. This takes us a little bit away from unboxed types and polymorphism because I think the way that that appears in Rust is quite different. But the notion of this sort of finer level of control is definitely accurate. But Rust gives up something really big to do what they do. They give up garbage collection. Within Jane Street and generally in programming, I think a lot of the time garbage collection is fantastic, right? It allows us to program without worrying about these low-level details that for most programs, we don’t need to.

So, for instance, when I’m writing the OCaml compiler—which is written in OCaml, of course—I do want it to be performant, but I don’t really care about microsecond latency. And so, I’m happy to write my compiler in a way that allocates a bunch of memory and then when it’s done with that memory, the garbage collector comes and gets rid of it. This is really, really convenient. In Rust, we don’t have that. In Rust, we are forced to think about memory, allocation, and deallocation at every point in time. And this gives us this fine level of control, but it comes at a real cost, and it means now we’re sort of fighting against this ‘pay-as-you-go principle’ that we were talking about earlier. In Rust, for memory, you don’t pay as you go. Everyone has to pay all the time for Rust fine memory control. So we wanna keep the high-level, garbage-collected OCaml for most applications, and then when we really want to have this fine level of control, we wanna have that, too.

And so, some of the work that we’re doing is around adding that finer level of control, but just where we need it.

26:57

Ron

So, one thing I wonder is whether this pay-as-you-go principle really applies in general or whether it’s like itself a kind of trade-off? I think, if you’d asked the question of like, ‘well we should think of types in general as pay-as-you-go.’ Maybe your baseline should be by default untyped, and then when you want some extra control, you should add types to it and lock it down more.

27:14

Richard

Mm.

27:14

Ron

That seems in principle reasonable. But all the languages that I’ve dealt with that have pay-as-you-go types or what you might call gradual type systems, actually inherit quite a lot of complexity and problems from that choice. It’s often simpler and better, at least for some kinds of problems, to have a uniform approach where you sort of figure out what trade-offs you wanna do and you kind of apply those trade-offs uniformly. And I think, at least from my perspective, the base choice you make in a language like Haskell or OCaml of like, ‘actually, even though it has some ups and downs, we’re just going to have types everywhere and that’s just how it’s gonna be,’ I think is at least a reasonable place in the trade off space of designs.

And I wonder if the same is true about this kind of thing about pay-as-you-go control? Whereas, I can imagine for some kinds of applications, you would want the property that, ‘yeah, I am explicit about memory everywhere. I kind of have a hard guarantee that anywhere I look I have all of this extra information.’ I don’t know. How do you think about this question of where pay-as-you-go is the right way or the wrong way to think about designing something?

28:09

Richard

I think that’s a great question and I agree. I mean, pay-as-you-go types, people have wanted that for some time. It hasn’t ever really happened. And, I mean, you could almost say that C++ and C have pay-as-you-go types and that they have type systems, but the type systems are sort of completely broken.

28:25

Ron

(laughs) Pay-as-you-go but then what do you get? I like that.

28:28

Richard

Well, right, but, I mean, just to clarify for our listeners. What I mean by ‘completely broken’ is that at any point in time in C and C++ you can just say, ‘Oh, ignore the type system. And I’m gonna just take this thing and change its type to be something else.’ And the languages, you know, they take this stance of, trust the programmer, that when the programmer decides to do this, that this is a good idea. But we lose the guarantees that one would want from a type system like that when you dereference a pointer that there’s actually something there when you dereference it.

28:52

Richard

So, getting back to memory control, I like the idea of pay-as-you-go there, or maybe it’s not even pay-as-you-go as much as a language that can have multiple different modes of use with very easy interop. In that we can have a system where there’s not fine memory management, that you just sort of use the current OCaml’s system of uniform memory representation, and then another part where maybe this particular team or this particular file says, ‘No, no. Here I really want careful memory management.’ This is a different kind of pay-as-you-go. It’s sort of at the file level or something like that, or the package level, I suppose. And then as long as one piece of code can easily call the other, that also works well.

We also see this kind of idea coming out in polyglot systems where we actually have multiple languages all calling one another because maybe this part of the system is easier to write in some language, that part of the system is easier to write in some other language. It’s all a way of, these sort of different approaches to attack the same problem that we don’t wanna have all of this complexity. We want to sort of narrow down what complexity we have, where.

29:50

Ron

Right. So there’s almost a notion of different dialects within the same language?

29:52

Richard

Sure.

29:53

Ron

With a really high quality FFI that really captures all of the important details so you can kind of interoperate, right? In fact, the work of polyglot stories are actually really challenging to engineers. There’s like, a ton—

30:03

Richard

Yes.

30:04

Ron

… of hard work. I mean, we’ve done a bunch of work trying to get the Python-OCaml interop story working just right. We’ve made good progress there but it’s actually quite challenging. And I feel like the work is quadratic in the number of different (laughs) languages that you need to hook together ‘cause it’s often unique, weird issues that come with every pairing of things that you wanna make all one to the other.

30:21

Richard

I think that’s right. And that’s one of the appeals of having one language that maybe is flexible enough to operate in multiple different modes. So, in particular, in our design for unboxed types, we are planning to make a box operation explicit. And the box operation is going to be ‘the spot’ that allocates memory. And so, normally, you’ll be able to get uses of this box operation for free. Programmers won’t ever notice it, they won’t write it. It just, all the existing code will have all the boxes inserted. But it would be really easy to imagine some kind of compiler setting that turns that feature off. Meaning that every time you wanna allocate memory, you have to explicitly ask for it.

So this doesn’t bring you all the way to Rust, in that there’s still a garbage collector operating, you still don’t have to manually deallocate memory. But if I wanna write a program that absolutely, where every allocation is known, we haven’t designed this out. Maybe we’re gonna go there, maybe we’re not gonna go there. Nothing is for certain. But it turned out that in our design, it just naturally fell out that we could just add this compiler flag that just turns off boxing and it would be super easy to implement and we could experiment to see how easy it is to work with.

31:23

Ron

So, here we’re talking about a lot of very ambitious changes to OCaml. One uncomfortable fact about all of this is, like, we don’t own OCaml, we are not the (laughs) primary upstream developers. Every time we wanna make a change to OCaml, there’s a bunch of people who we have to convince that it’s a good change. So one of the things that you’re thinking about in particular is, the kind of relationship of the work that we’re doing here and our connection to the larger OCaml community. Say a little bit more about how you think about this whole process.

31:51

Richard

So, I wanna start by pushing back against ‘unfortunate fact.’ I don’t see that as an unfortunate fact at all. So OCaml was born as a research project out of Inria in France and still is there. That’s sort of its beating heart. And we are really significant benefactors of that work that others have done, that others continue to do. And so, Jane Street has chosen to work in part of this open source language community where we’re taking others’ ideas and we’re contributing our ideas back.

So in this podcast and in our work, we have these grand ideas. ‘Oh, we’re gonna add this to OCaml. We’re gonna do this, we’re gonna do that. Of course, what I really mean is, we’re going to experiment with this idea internally. And then as that experiment unfolds, as we gain experience and become more sure that it’s a right—I shouldn’t say a right idea. There’s many right ideas. But as we gain more confidence in a particular design, we can then work with the rest of the OCaml community to try to make this part of everyone’s OCaml and not just Jane Street’s.

And in that way, we’re giving back to that community. At the same time, we’re continuing to reap rewards from other work happening in that community. So the biggest example of which is the multicore support that’s coming in OCaml 5. Still gonna be some time before Jane Street’s ready to upgrade to OCaml 5. But that was a huge pile of work done mostly outside, or maybe entirely outside of Jane Street’s walls, and we benefit by being part of this open source ecosystem. And so, I think that this is a really great place to be where we’re participating, we’re getting new input of technical content, like multicore OCaml, as well as design ideas. And I’m even thinking of something just a few weeks ago where I found an infelicity in the compiler, made an improvement, pushed that upstream, and then we got fresh ideas from folks outside of Jane Street’s walls about, ‘Here’s actually an even better way to do it,’ and that was great. And then we could incorporate that here. Without being part of this open source ecosystem, we wouldn’t have gotten that insight and we would be poorer for it.

33:47

Ron

So, in the Haskell world, you spent a lot of time working on exciting new type system features for Haskell and now you’re doing, in substance, similar kinds of work here. But I think that work flow is pretty different, right? I think then, in the Haskell world, it was like the primary work and ideation and evaluation was all deeply integrated from the beginning in the open source world. And here, we’re doing this work where we’re still open source, still, you know, you can go look at the results on GitHub. But we are mostly iterating internally, and then, over time, as we gain experience, as we gain more confidence that the things we’ve built are good ideas, working to see what subsets of these we can get upstreamed. I’m curious how that has changed your feeling about the work, how it changes the texture of the work that you do?

34:27

Richard

So working within the context of Jane Street gives us a lot more opportunity for experimentation. So a real big challenge of doing language design is that, by necessity, you come up with an idea and maybe you think it’s a good idea and you experiment with it on a few small programs on your own machine or you get your friend to sort of experiment. You bounce the idea. Maybe, you know, you’re even proactive and you convene a committee of experts on this idea and now you have, you know, five people thinking really hard about this one idea and trying to come up with the absolute best design.

But then, once you come up with the design, if you’re just in an open source environment—without the context of a place like Jane Street—you develop the idea, implement it, and release it, and then now you have thousands or hundreds of thousands of programmers using it, and maybe it was a bad idea. But by the time you discover that it was a bad idea, it’s a little bit too late because maybe you have 90,000 programmers who think it’s a bad idea, but you have a thousand who think it’s a fantastic idea and will be very, very, very upset if you break their programs by changing it. And now you’re in a bad way.

35:27

Ron

And even the people who think it’s a bad idea, who would like to get rid of it, don’t necessarily want you to break their programs in the interim before they’ve (laughs) stopped relying on the feature.

35:35

Richard

That’s right. And so, it’s really, really hard to make changes to a proper open source programming language. In the context of Jane Street on the other hand, it’s—I don’t wanna say dead easy. There’s work involved, but it is tractable and somewhat easy in that we can develop an idea, push it out there, get other programmers in the firm to start using it, and then as that happens, we can say, ‘Mm. This isn’t quite working out the way that we thought it would.’ That, you know, theory meets reality, and theory loses.

And so, then we can make a change to the feature and we have sort of an operation that we use internally called a ‘tree smash,’ where some Jane Street engineers work together to come up with a big diff that happens to all of Jane Street’s code, all at once, and we can change the spelling of a keyword if we want to. And in fact, we’re imagining this now. So Jane Street has been working on a feature called ‘local types’ or ‘stack allocation.’ These two things are kind of the same thing. And we’re realizing that one aspect of the design was just a bit wrong. And there’s already a ton of code written using the old design, but we’ve invented a new keyword and a new place for the keyword to appear, and all this stuff.

And so, it’s gonna be some work to fix it, but there’s no part of us that’s saying, ‘Oh no. Now we need to think about a migration plan and we need to make sure that no one is too unhappy with this.’ We’re just gonna go do it. And so, it means by the time we get to upstreaming, everything is battle-tested. And so, it just increases the level of confidence in the design when we go through that process.

37:03

Ron

One of the concerns I could see people having about this kind of process is, it’s going to do a lot of training on, ‘What are the requirements within Jane Street?’ But there are all sorts of ways in which you could imagine the requirements in Jane Street and outside of Jane Street being different. I’m curious how you think about the design process in a way where you end up with language features that are likely to be of quite general utility, ‘cause I think, in the end, the only ones you’re gonna get accepted upstream are the ones that people think are more broadly useful than just being useful for us.

37:30

Richard

So that’s indeed a challenge, right? It’s a challenge of overfitting, right? We have a very particular style of code within Jane Street and a very particular use case that we’re working on. I think that is sort of a harder question to answer in some sense. I think one way that we address that is by seeking outside feedback from the very beginning. So, the plan that we have for unboxed types, another Jane Street engineer, Stephen Dolan, he made a presentation about this design for unboxed types, I think in 2019. We’ve been thinking about this for a long time. The local types and stack allocation feature, this has also been featured in a number of presentations that we’ve made to the OCaml community, out in public.

And so, by incorporating that process early, we can get broad feedback. That’s not the kind of feedback that tells us, ‘Oh, should the keyword go here, or should it go there?’ Right? That’s the kind of thing that we develop internally. But I think that, by giving these presentations, by involving the broader community, even from the very beginning, that helps to prevent some of this overfitting problem.

38:27

Ron

So, another interesting aspect of your background is, you’ve spent a lot of time, years really, working in the Haskell community and working on Haskell. And now, you’re working on a totally new programming language using it both as the surface language in which you write your programs, and also helping to design that language. I’m curious, what struck you about difference? I’m curious, what are the differences that have struck you about Haskell and OCaml at multiple different levels?

38:48

Richard

It’s been really fun over the past, I guess, six months now being part of these two language communities. So, I should say, I’m still quite active in the Haskell world. I have not left the Haskell world. I’m living both Haskell and OCaml on a daily basis. So let me think of a couple of interesting points of comparison.

So, one is, it seems kind of simple, but actually I think it affects the way that we program. The approach toward interfaces. In Haskell, you tend to write your type signatures sort of right next to the function and Haskell uses a lot of type signatures. OCaml doesn’t so much. And so, OCaml there’s these separate interface files where you define the interface to your whole module, but it’s kind of apart and it means, in my experience, looking at a bunch of OCaml code. OCaml code tends to be rather less documented than similar Haskell code, and I think that’s in part because in Haskell, you put your types right there and that’s a form of documentation. And once you put your types in, then you can also put more documentation there and it becomes part of the habit of the Haskell programmer to put those comments right in there.

A flip side of this, is that Haskell has this feature called typeclasses. And typeclasses allow you to use essentially one functioning to mean a variety of different things. OCaml doesn’t have that feature. And so, what that can mean sometimes is that Haskell code can become quite a bit harder to understand because if you have a bunch of these function names, any of which can mean a variety of different things, all strung together, then it takes a lot of work on the part of the reader to try to understand what on earth is going on there. And that problem just doesn’t arise in OCaml. OCaml is much more explicit about what operations it’s taking.

So maybe I can even, taking these two examples, generalize that a little bit and say, I find Haskell to be somewhat more explicit about what’s happening at compile time. Whereas, OCaml is somewhat more explicit about what’s happening at runtime. So another place where that comes into play is that, the Haskell compiler—and this connects with a topic we were talking about earlier—the Haskell compiler optimizes much more aggressively than the OCaml one does. And that’s because in Haskell, Haskell’s a lazy language which means that if you say, ‘Let X equal some big computation,’ we’re not gonna compute the big computation until we need the value of X. In OCaml, if you say, ‘Let X equal a big computation,’ we just compute that thing right away.

And so, that means, on the one hand you might say, ‘Oh, well maybe Haskell is more efficient,’ because maybe some code path never uses the value of X and so it means that we can discard that whole big thing. But it also means that it’s much harder to predict in Haskell how fast your program is going to run or what its performance characteristics are gonna be. In OCaml, it’s much easier to predict that. You can just sort of read your file top to bottom and, within a function, it just performs the operations that you see roughly in the order that you see them. And that means, OCaml again is more explicit about what happens at runtime, but without some of the type annotations that we see in Haskell, a little less explicit about what’s happening at compile time.

41:36

Ron

You mentioned a couple of things that are different that I wonder if they’re really language differences, or just cultural differences. If you look at the tendency to do fewer type annotations on the definition of functions, you could put more type annotations. And I think there are some people who write OCaml who do, but there’s certainly a tendency not to and I think the Jane Street house style certainly is one that does not have lots of type annotations, outside of interface files where those are essentially required everywhere.

And the documentation thing, too, like, the interface files are a very natural place to put documentation and I am constantly dissatisfied that I think we put way too little documentation in the (laughs) places that we could. And I don’t know that there’s anything exactly about the language that forces that. Like, I’m not sure that I buy ‘the need to put type annotations right on functions’ is the thing that really makes that difference.

42:19

Richard

That may be true. It’s hard to say. I do think that form follows function, function follows form a little bit, in that, when you’re used to describing the specification of a thing right next to that thing, that, to me, is going to encourage you to write documentation. Whereas, in OCaml, you write the specification over there, in that other file, nowhere near where you write your implementation. And sometimes I think that means that you’re less likely to put those comments on the implementation when you need them.

42:45

Ron

It’s funny. My intuition is the opposite of, like, ‘Oh, I’ve written this very bare interface file that just has types,’ and I think empathetically about the person who’s reading it. It’s like, ‘How will they have any idea what this means? I had better put a comment here.’ (laughs)

42:58

Richard

Right. So the comment and the interface files are good, but I think it’s not just that. I mean, and this could also be, I have a bias in that, most of the OCaml that I’m reading and writing is in the OCaml compiler itself. Maybe this is different than everything else at Jane Street. In fact, I’m sure it is. And it has been striking for me after spending so many years working in Haskell’s compiler, that Haskell’s compiler has many, many, many more comments than OCaml’s compiler does. Maybe I’m overfitting on this particular piece of software instead of just the language in general.

43:26

Ron

I do think looking at the innards of a compiler is always a weird place to think about how one should write code for the language. Because, like, one of the facts about OCaml—as it is often the case for many languages—is that OCaml was written by people who didn’t yet really know how to program in OCaml kind of by definition. And lots of the code that’s there now has been there for a long time and you can sorta see that. I think if you went to those same people today and been like, ‘How would you write this now?’ They’d all be like, ‘Oh, really very differently.’ But, you know, parts of it just kind of haven’t been rewritten and have the shape that they did years ago and are harder to understand than kind of anyone would exactly like it to be today.

44:00

Richard

And to be fair, that exact same thing is true in the Haskell compiler. There are stretches of that that no one would write it that way today. But it was written that way before anyone really knew how to program in Haskell.

44:09

Ron

So another difference that’s always struck me about Haskell is the different approach to language extensions. And I think about this in two different ways. One is, OCaml is just massively more conservative. There was a period in time early in OCaml’s development where you could almost see the process of Ph.D. students graduating. It’s like someone graduates, they write some language feature, and it gets added to the language. And that stopped pretty early in OCaml. OCaml got pretty conservative about making changes. It was like, ‘No, no, no, we’re gonna add things that are like, really good, and it was pretty restrictive about what would go in. And throughout that time, it kind of had one language, pretty much. OCaml worked in one particular way and that was kinda that.

Haskell on the other hand, has had a lot of glorious experimentation around language features and those experimental language features were often hidden behind pragmas, right? There’s lots of different things you could turn on and off. And so there kind of isn’t one Haskell or two Haskells, but there’s like 10,000 different Haskells, depending on which collection of flags you wanna turn on or turn off. You have 10 different pragmas and now you have two of the 10 different possible arrangements of the language features. I’m curious how you think about those different sets of choices?

45:15

Richard

Yeah. I mean, that’s a great question. So I do have to push back against your sense of scale. So Haskell has, when I last counted, and this was a few years ago, 150 or so extensions. So Haskell has actually 2150 languages.

45:27

Ron

(laughs) Ouch.

45:28

Richard

Ouch, indeed. So I think that this comes from the origin of Haskell versus the origin of OCaml so actually you probably know more about the origin of OCaml than I do. But I know Haskell was started by committee. There was a committee that met starting in, I think, 1989 into 1990, coalescing these ideas around a lazy functional programming language. And then this eventually became a Haskell standard and there were multiple different compilers for Haskell that all implemented the same standard Haskell. And then maybe one compiler would think, ‘Ooh, wouldn’t it be fun if we had X?’ And so, then they would add that feature, but everyone still wanted to make sure that it was a Haskell compiler and not this other special language based on Haskell compilers. So there was an idea of language extension. So you could have base Haskell plus these various extensions.

46:16

Ron

So, in other words, OCaml is like Python and Haskell is like Scheme?

46:21

Richard

Sure. Yes. In that OCaml has a manual for the language, but there is not a standard. There are not multiple different software artifacts that all compile some OCaml language that exists beyond a single compiler. But, in any case, going back to Haskell, that was the early days of Haskell and there were multiple Haskell compilers. As time has gone on, all of the other ones have either died off or there are still a few other Haskell compilers out there, but there’s not really an attempt to stay current with the newest features. And there’s really now just one: the Glasgow Haskell Compiler, or GHC. And that’s the one that, when I say that there’s 150 language extensions, the GHC is supporting that.

46:59

Richard

And so, when you have multiple different things, if you wanted to find a common core that all of these different compilers can interop with, it makes a lot of sense to have individual extensions when you say you’re deviating from this common core. Now there’s really just one compiler.

I think that the current system, the current plan at Haskell, is not very well motivated. And instead, the feedback that I hear from users is that they find the whole language extension system very heavy and it means that, to get much done in Haskell, you need to now start your file with the list of 20 extensions that you’re using. And newcomers can’t tell the difference between brand new experimental extensions that might change from one compiler to another, or extensions that have been around for 20 years, or there are some extensions that have been around for 20 years but actually we know are dangerous and you really shouldn’t use.

And when I say, ‘We know,’ I mean, like, I know this and a couple of other Haskellers know this, but someone just picking up the language won’t know that. And I personally find that quite problematic. And so, there’s a debate going on right now within the GHC Steering Committee who is a body chosen to sort of help evaluate the evolution of the language to reimagine all of this. And I’m hoping that we end up with a structure that looks quite different from what we have today, while still retaining backward compatibility.

So if you have your 20 language extensions at the top of your file, that will continue to work in this new vision. But I am hoping that we can reorganize it in a way that’s a little bit more user-friendly.

48:23

Ron

Do you think in the end it would make sense to move toward something where there’s closer to one standard language that includes most of the extensions, and so that most users end up not thinking about that ‘two to the whatever’ configuration space?

48:36

Richard

I do think settling on one standard language would be good. I think we can get 80% of the way there and go from 150 extensions to maybe seven or something like that. I don’t think we’ll be able to get all the way there because there’s just too many different use cases for Haskell, there’s too many different people who have slightly different ideas of what that core should be. So if we just sort of got rid of the extensions mechanism, I think that that would cause too much of a rift in the community and probably not be tenable. But we can get close.

49:04

Ron

So, throughout this conversation, I feel like there’s been a particular kind of vision and idea of what programming is that’s motivated a lot of your thinking. And that has something to do with having a language that’s simultaneously expressive, it lets you say what you wanna say, but also has real tools for reasoning, in both type systems and, you know, more sophisticated mode-dependent types, or essentially automated tools for reasoning about your program. So in the last, I don’t know, few months, couple of years, there’s been an enormous amount of motion in a totally different direction for making programming better, which is various AI-assisted ways of making programming easier. With all of this kind of recent work on large language models, things like ChatGPT, Codex, all of that, making an enormous difference to how people are programming on a regular basis. I’m curious how you think about this and how it fits into your broader way of thinking about programming?

49:55

Richard

I see this evolution of sort of AI-assisted programming as not quite the sea change that maybe others have seen it to be. I see it as a big step. It’s not a small step change. But it doesn’t remove the need to communicate precisely. In that, to me, the interesting thing about a programming language is that it’s a mode of communication that is precise. In a sense, that’s almost the definition of what makes a programming language a programming language, as opposed to some other kind of language. There’s a precise semantics to everything that is said in that language. And that language is used as a medium of communication, both from human to computer. That’s how we often think of it. But also from human to human.

With the advent of AI-assisted programming, now we have sort of a new method of communication in that it’s a communication from computer back to human. In that, you might have something like ChatGPT producing the code, but a human still has to read that code and make sure that it does what you think it does. And as a medium of precise communication, it’s still very important to have a programming language that allows that communication to happen.

And so, this new mode of communication is going to put different pressures on language design than what we’ve had in the past. But I don’t think it removes the need for programming language design. But like I said, it does create different pressures and these have been evident for some time in that one little maxim I’ve had in my head for years now about language design is that you wanna optimize for reading, not for writing. Code gets read much more often than it gets written.

And so, when designing a new language feature, maybe you’re thinking, ‘Okay, I could do this very cleverly with, like, a nicely placed twiddle in this spot in the code. And I could use that twiddle to mean something very important about my program. And maybe that’s very concise, but it’s hard to read, it’s hard to search for, it’s hard to train new people to understand. Instead, it tends to be better to write out words in your design and programming language, that’s easier to search for, and easier to learn, and just easier to organize in your brain. If we end up getting to a mode where humans are doing even less and less writing, and computers are doing more and more of it, then those pressures just increase. And we wanna make the language easier to read and maybe even harder to write. Maybe we even get to a point where if computers are doing all of the code generation, it’s just kind of, you know, symbolic and structured. It’s not just text.

So we get these richer programming languages but I just don’t see it as, there was yesterday and then there’s tomorrow and it’s gonna be totally different and let’s just start from scratch. I see this as just one phase in evolution of this precise communication medium.

52:35

Ron

One of the things that’s really striking about these AI assistants, at least in their current form, is they’re really surprisingly powerful, right? They can really do a kind of stunningly good job of taking a query and understanding it and providing a piece of code that tries to do what it is that you asked for it to do.

But they’re also strikingly fallible. They make lots of mistakes. And, yeah, the reading thing is pretty important because you ask ChatGPT or, you know, whatever your favorite large language model is, to write a piece of code and look at the result. And it’s super easy for the result to just be wrong in all sorts of different ways. And I can sort of see the rising requirement of making things more readable. I’m curious how you think things like dependent types fit into this story?

53:16

Richard

So, dependent types in their essence are a way of writing precise specifications. So the sorting example that I gave earlier, I described that, you know, you could have a function instead of going from ‘a list of ints to a list of ints’ to something more glorious. Well, before dependent types, or you know, language without dependent types, you could just do that in comments. But probably in your comments, you’re not going to be as precise as you could be if you really wrote it in types, right? You say, you know, return to the input list in ascending order, or something like that. But what does that really mean?

We need a language where we can precisely specify what this function is doing. So as I said earlier, ascending isn’t quite right. I mean, if you write in a comment, ‘This returns the input list in ascending order,’ well, what if the input list has duplicates? Now you can’t even meet that specification. Where actually, that specification doesn’t make any sense at all because the input list isn’t in ascending order. What does that mean to say to put the input list in ascending order? That’s a contradiction in terms, because the input list isn’t in ascending order.

And so, there’s some amount of interpretation that humans can provide, interpretation that a large language model can provide, but in the end, it’s gonna come down to precise communication and specification. And so, where do dependent types fit in? Well, they can become the input to the large language model. Maybe now we have programmers who are well-versed in precise communication of specifications, not implementations, and we can say, ‘ChatGPT, give me a function of this type.’ And then you have your nice type that takes an input list, and it returns an output list that is a permutation of the input list in non-decreasing order and we specify that.

And then now, that gives a nice specification for ChatGPT to go off and say, ‘Okay, here’s an implementation that meets that. Oh, and by the way, it has this asymptotic running time because I’m a nice large language model and I’m gonna tell you that.’ And then, now we actually have a model by which we can check that the result meets its specification if it is in this precise language of dependent types.

55:07

Ron

Although I have to say, I think I am more pessimistic about the idea of people actually going off and writing down the specifications even. ‘Cause those are actually pretty hard to write.

55:15

Richard

Sure.

55:15

Ron

I wonder if a more plausible model is, you go to your large language model and say, ‘Please write me a specification for a function that sorts a list.’ And then it, like, spits something out. And then you look at it and think, yeah, that seems about right. And then you go from there to next stages. But the role that this kind of concise specification has, it’s like a smaller and maybe more readable thing that you can use as part of verifying whether the later pieces in fact do what you think they’re supposed to do.

55:40

Richard

Yes, but I think there’s a real danger here. I agree with what you say in that, writing a precise specification is hard. And humans are lazy. So if it’s hard, we’re gonna ask the computer to do it. If we’re asking the computer to write the specification of the function that it’s going to write, now we’re getting into thin ice. Because if we’re working in a system where the human is not expert enough to be able to read the specification and know that it’s the right specification, now we’ve lost. Now the computer can just sort of go off and do whatever it wants and we have no way of knowing whether it’s right or wrong because we’ve lost that ability to sort of have that precise communication.

56:14

Ron

I think one of the tricky things here is, people are often pretty bad at the reading part of this, right? The idea if something gets written and now you have to read it, especially if it wasn’t written in a really clear way, reading some piece of code that is not really well-structured is actually really challenging. Like, one of the actually most important parts of the process of code review I find, is not so much that, like, one person writes the code and someone else reads it to validate that it’s done the right thing. It’s more like, somebody writes the code and the other person says, ‘Oh, man. This is, like, too messy for me to even read.’ And then there’s some kind of back and forth process where you try and get something that’s actually simple enough to be understood. And I think it’s an interesting open question of, like, as we start using more of these AI assistants, how good they will be at generating things that are actually simple.

56:55

Richard

Although, if we have precise specifications, the simplicity of the implementation becomes less important.

57:01

Ron

That’s fair. I mean, in some sense there’s a kind of open technological question of, like, how good will large language models be, acting as tactics for theorem provers?

57:10

Richard

Right. Yeah. I mean, but if we’re in an environment where there is a tight correspondence between the specification and the implementation, and what I mean by ‘tight correspondence’ is this dependent type’s model where you can—and there’s other models, it’s not just dependent types, there’s refinement types, there’s other ways of checking an implementation against a specification. But if we’re in an environment where we can check an implementation against a specification, the specification is simple enough and communicated precisely whether that’s in very careful natural language or probably not just natural language ‘cause natural language is very, very squishy. But probably in some specification language, you could call that specification language ‘dependent types’ if you want or you could call it something else. But if we can communicate that specification, check the implementation against the specification, now suddenly there’s not all that much incentive to ever read the implementation.

57:59

Ron

Right. It becomes a little bit like, you know, reading the output of the compiler.

58:03

Richard

Yeah, that’s right.

58:03

Ron

You don’t normally bother.

58:04

Richard

That’s right.

58:04

Ron

Yeah. It’s interesting. I do wonder whether a whole potential kind of direction for innovation here, which you more or less have pointed in the direction of, is designing languages that work usefully in this kind of intermediate things to generate in the process of working with some kind of AI assistant. The thing that’s generated as an intermedium really affects the overall process of working on the system and generating confidence it’s doing the right thing. It’s not a totally new problem, I guess, in the context of language design. But it does put new kinds of pressure and maybe changes the trade-offs that show up.

58:34

Richard

Yeah, that’s right. I mean, you know, it’s too early, I think, to start to design a programming language around this kind of interaction. We’ve only been having these interactions with these assistants for a few months. And they’re changing fast. So I think now would be the wrong time. In two years, maybe one could start thinking about designing a language from scratch to do this. That sounds plausible to me. But I think a good starting point would be languages that we have now because they’re designed for precise communication. That’s, in the end, what we need. And, again, maybe there’s less pressure on the writing piece and more pressure on the reading piece. But I don’t think that they’re so divorced from each other that it means that we throw out everything we have and start from scratch. That seems, to me, pretty unlikely.

59:15

Ron

That makes sense. Well, thanks so much for joining me. This has been a lot of fun.

You’ll find a complete transcript of the episode, along with links to some of the things that we discussed at signalsandthreads.com. Thanks for joining us and see you next time.