CoRecursive: Coding Stories - Tech Talk: Dependent Types in Haskell with Stephanie Weirich

Episode Date: June 13, 2018

Tech Talks are in-depth technical discussions. At Strange loop 2017, a wandered into a talk where I saw some code that deeply surprised me. The code could have been python if you squinted, passing dictionaries around, no type annotations anywhere. Yet key look up in the dictionary was validated at compile time. It was a compile time error to access elements that didn't exist. Also the dictionary was heterogeneous, the elements had different types, and it was all inferred and validated at compile time. What I was seeing was Dependent types in Haskell. In today's interview Stephanie Weirich explains her efforts to add dependent types to haskell and how that example worked.   Shows Notes: Dependent Types in Haskell Talk https://www.cis.upenn.edu/~sweirich/ https://github.com/sweirich @fancytypes Dependent Types Regex

Welcome to Code Recursive, where we bring you discussions with thought leaders in the world of software development. I am Adam, your host. Now, you called it magic, and I call it programming. At Strangeloop 2017, I wandered into a talk where I saw some code that deeply surprised me. The code could have been Python if you squinted. It was passing dictionaries around, no type annotations anywhere. Yet the key lookup in the dictionary was validated at compile time. It was a compile time error to access elements that didn't exist. Also, the dictionary was validated at compile time. It was a compile time error to access elements that didn't exist. Also, the dictionary was heterogeneous. The elements had different types,

and it was all inferred at compile time. What I was seeing was dependent types in Haskell. In today's interview, I try to understand what was happening in that talk. Stephanie Wyrick is a professor at the University of Pennsylvania and works on extending the type system of GHC, among many other things, I assume. Stephanie, welcome. Thank you for talking to me. Thank you. Thank you for inviting me. I'm happy to be here. I saw a talk that you did at Strange Loop, I think last year. It kind of blew my mind. And it was about kind of extending the type system of Haskell to support dependent types. So what are dependent types?

That's a tricky question. And it's a tricky question because there's lots of answers of what dependent types are, and those definitions can be technical, where they classify some things as definitely being dependent types and some things as definitely not being dependent types based on mechanism. But I prefer to think more about applications. Can you get your language and your type system in your language to do particular applications and using that kind of definition? So in that talk, I walked through how Haskell, even though under some of the technical definitions doesn't have dependent types yet, I walked through how it could already do quite a number of the activities that we want

from dependent types. And at the end, kind of pointed out what still needs to go into Haskell to make it a full spectrum dependently typed language. Now, I guess that's not really answering your question about what dependent types are. But just to briefly summarize, dependent types are a way of having some kind of computation in your type system. So, you can use your types to express domain-specific invariance about your program that the type checker uses to check your code. There's a lot of the inspiration that I get for extensions for Haskell's type system comes from Martin-Loff type theory. So, this is a specific mathematical formalism that is used in the foundations of logic to create formal systems to describe what is provable and what is true. So, I did an interview with Edwin Brady, who created Idris, and he said he likes this term, maybe just, I'm not sure if just applied to Idris or in general, but he likes the term first-class types.

He said you can think of dependent types as just like a programming language where you can manipulate types just like their values. How do you feel about that? That captures quite a bit of what you get from dependently typed languages. And this is one of my goals in Haskell is very similar to what Idris provides, giving you. And this is what I mean a bit in having your type system be as programmable as the rest of the language. This lets you, again, lets you express why you think your program has particular properties using the same language that you do to implement your system. So your logic and your programming languages

have a really nice uniformity to them. So what makes dependent types useful? So there's many levels to answer that question right of course type checking is useful because we want to use it to both identify bugs in our programs but also to capture some structure while we are programming to be able to think about our programs both in terms of what they do at runtime, but also at a more abstract level. What do we know is always true about our code versus what is true at this particular moment? Or what is true about this entire class of values versus what is true about this particular value?

So type systems naturally give us this form of abstraction. And without dependent types, this kind of abstraction is limited in what I get from dependent types is the ability to be able to say, based on this runtime test, I know this about my compile time value. So it gives you much more flexibility about the interaction between sort of your context-sensitive tests and what your type checker knows at compile time. So I find it is a tricky subject to grasp, the advantages. But you had this example that I really liked. So it was regular expressions, right? Could you describe the example you had of using dependent types? Sure. Yeah, so I use this example in the Strange Loop talk because I really kind of captured what dependent types can give you in lots of different ways. So in the example, the nice thing about a regular expression is that most of the time you use very concrete regular

expressions, right? We're trying to, and I was using the example not just for matching regular expressions, but for doing something that's called capture groups, where you could take a regular expression and name specific parts of it and pull out parts of the text, like a very primitive form of parsing. And if you have a concrete regular expression, you should be able to look at that regular expression and know exactly what parts of the regular expression are going to get captured, how many groups are going to get captured. Regular expressions allow you to name those groups. So, what are the names of the subparts of the regular expression that can form a capture group? And also, because regular expressions allow you to alternate or have optional components,

sometimes the capture groups will definitely give you an answer, and sometimes they might give you an optional answer, and sometimes they might give you several different answers, like, for example, if you're under a cleany star. And so the type of the capture group might depend on where it appears inside that regular expression. So in the Strange Loop talk, I go over designing a library for regular expression capture groups where the type checker can look at the regular expression and figure out what kind of result you're going to get

from that particular regular expression. So that when you get, it's essentially a dictionary, but that dictionary, sometimes it's going to match a name of a capture group to a string. Sometimes it's going to match it to an optional value. Sometimes it's going to match it to an optional value. Sometimes it's going to match it to a list. But we know this at compile time. And so the type checker should help you use this correctly

because all the information is there when you type check your program. I think it makes a lot of sense, but it's not something I've thought about before. So if you have a regular expression string and it has, like if it has something that ends in a question mark, then that means that you may or may not get a value. So if the type system could get hold of that information,

it could be a maybe or an option. Or if you have a star, then you might be matching, actually, maybe a star. If you have a capture group with a star, then you could get multiple matches, I guess, right? So, this information is embedded in this string, but without dependent types, you're not getting it in the type system, right? Exactly. And the connection between how you interpret that string to what the type system should think about, that's not something any language should have built in. This is something that a regular expression library should be able to express via some kind of programming. This should be part of the design of the library that supports these regular expressions.

And so the thing that really blew my mind, I guess, is so I take this regular expression. So your example was matching like Unix paths. So you're getting like you give it a path and there could be multiple like subdirectories and then a file name and an extension um and you're you were giving these names so you have you can get back you know a match for the directories a match for the base name and a match for the extension you you run your regex and you get back this dictionary um and then you show, I think part of the magic is you, so you call into the dictionary, you say, get me the base name, and it comes back.

But then you try to get back some other element from the dictionary that wasn't part of your capture group, and it's a compile time exception. And I think that's kind of when the light bulb went off for me. I was like, oh, there's something magic here um well because i know that um well i mean that's not how i expect dictionaries to work i guess and i know there's a whole class of languages where they spend a whole bunch of time throwing dictionaries around and it's hard to validate say like in javascript if you you know if you access some element in in this dictionary and then it's like a runtime error if you if you access some element in this dictionary,

and then it's like a runtime error if you make a spelling mistake. And here we're pushing all that system to the compiler, I guess. So how does this work? And I think that's kind of what I like about the example is that it very much does relate to dictionaries. And kind of shows you that even in JavaScript and a lot of these dynamic languages, right, parts of our dictionary when we create it are very dynamic, right? We don't know at compile time. When I say compile time, I mean we don't know so much at development time what we're going to get, but maybe we do. And if we do, we should be able to tell that to our compiler so that the compiler

can help us out. Because once we have created this dictionary, if we know what its structure looks like at compile time, we should be able to have the compiler help us out, help us use it correctly. Now, you called it magic. And I call it programming. Right? So, the talk kind of walks through how it works step by step, but some of the key ideas are constructing the regular expressions with types that are rich enough to calculate and express what the capture groups are. So that when you construct the regular expression, you know just from its type how those capture groups interact with each other.

But the types themselves, they're a little more expressive than we usually see in programming languages because the types of the regular expression operators, like, for example, concatenation, where you do one regular expression and then another one right after it, right? You're combining two together. Well, the capture group from this entire regular expression is going to be some merging of the capture groups that we get from the first regular expression and the capture groups that we get from the second regular expression. And then we can write that merging as a functional program that takes this compile time data, the capture group data, and combines it together. The part that's a little confusing about that, I guess, is that we're providing a string. Yes. So I think in this case, the magic is, but I should stop saying the word magic. So we have a regular expression string and you're saying we're going to turn

this into a more, um, complex type. Now I'm not really familiar in my programming experience with taking a string and turning it into a type. Ah, ah. Um, so, so part of the magic was I was using a feature of Haskell. And one of the great things about working in Haskell is it's a rich language. So it has a lot to draw on. So I can put many features together.

So one of the features I was using was a feature that's called Template Haskell, which is a way of doing... It's another way of doing compile time programming in Haskell. So it allows you to take things like a string and just run Haskell code on that string to produce Haskell abstract syntax, which then is type checked and inserted into your program at that point. And so the very first step of that example was taking the regular expression string and creating a parser for that regular expression string that would replace the string with some regular expression constructors that I had developed for my library. So the parsing part is not so much dependent types as being able to use this

template Haskell feature. So you're writing a parser as you would have to do to write your normal regular expression library. Yes. The trick is it's being called sort of like in a macro, like at compile time. Yeah, very much like a macro at compile time. And then somehow when this dictionary is returned, when I apply a match, that dictionary needs to know all this type information. So that when I ask for, I didn't even describe this, when I ask for the directories,

actually you're coming back as a list because your regex knows that there could be multiple directories just based on its parsing and is returning the type of the match. So how does it know, how is the dictionary type constrained in that way? Yeah, so an important feature of dependent type system is this idea of an index type. So this is a data structure that is indexed by some compile time data, and that compile time data enforces constraints on that data structure. So you can imagine just a simple dictionary data structure as an association list where I can say I can map any string to any value. But the constraints we might want to say is not any association list. Association lists where the first association is between this string and this type of value,

and the second association is between this string and this type of value, and the second association is between this string and this type of value, and there isn't anything else. So we can go from a very, very general type, arbitrary association list, to a very, very specific dictionary types, association lists that have exactly this form. And the mechanism that we're doing there is the index type. The index on the dictionary constrains what the association list has to look like. Why is it called an index type? Um, this is terminology that it's adopting from dependent type theory. So, if you think about, you can think about it as the dictionary type is actually a function from its type argument

to many, many different types. And the type argument is serving as an index to which particular type you actually mean. So there is a function that takes a type, like the type of base directory and then returns a dictionary that has a base directory? Am I on the right track? I'm thinking of it at a slightly different level, right? So, here's a very, very simple example of an index type. It's very,

very simple. It's indexed by a Boolean value. And if the Boolean is true, then our type is integer. And if our Boolean is false, then our type is character. And so we can have a general type that if we don't know what the Boolean is, we know it's either an integer or a character. But if we do know what the Boolean is, we know precisely which one it is. I follow. So that is an index type. Actually, I thought that was type computation, where you're taking an argument and computing a type. Are these related concepts? They are related. What makes it an index type is that we actually are making a decision based on this static information.

Okay. Right. Does this – go ahead. This is just to distinguish things like type parameters, where we might take one type and give another type, but treat that type argument parametrically. Like, for example, a list data type has a parameter for the elements in the list. And so the list type constructor takes types and gives us new types from it. So that is still a type function, but it's a parametric type function. And so the type theory for working with a parametric type function works out fairly differently than if the system allows you to make distinctions on what those arguments are.

And so there might be a theme of this interview of me asking you stupid questions. However, a type function, that's just a function that returns a type as it's output? Yes. Yeah. Okay. Got one. There we go. So it's a way to, so in Haskell, you could express standard Haskell, you have param to list parametrically, right? You know, nil is going to give you a list of that type, and cons is also going to give you a list of whatever the type argument is. And there's not that much interaction between your data constructors and that type argument because of this restriction to parametricity. With GADTs, you can have interaction between your type arguments and your data constructors. So, in a GADT, so a very simple example of a GADT might be you have some type that takes in a Boolean, right? And then this is going back, making that earlier example I gave you a little

more precise, right? So our type, let's call it T, it takes in a Boolean as its index, and it has two constructors, one that takes in a char and another that takes in an int. And we know that based on, and we can reflect that in our Boolean to say that if we are using the constructor that takes in a char, we'll say we don't create just T with an arbitrary Boolean. We'll take a T where the Boolean has to be true. And if we're going to do one with the constructor that takes in an int, then that's going to force the Boolean to be false. And so what that means is elsewhere in our program, if we have t where we know that index is true, we know exactly what constructor made that value. Because one of the constructors gives us a type where the Boolean is true, and the other constructor gives us a type where the

Boolean is false. And so it wouldn't even type check if we had used the other constructor gives us a type where the Boolean is false. And so, it wouldn't even type check if we had used the other constructor. We know exactly which constructor we have, so we know exactly what the type of the argument should be. And we know we don't really have to, if we do a case analysis, we know we only even need to do one branch. We don't have to do that other branch. And this is the, seems like the baby step into crossing over these data and types are now depending upon each other. Exactly, right? So this is capturing a connection between what's going on at compile time and what's going on at runtime. So back to this dictionary, we get this dictionary back after I run my regular expression match.

And in it, I can look up by, I can say, give me the directory. So I pass this dictionary, the string directories. What's happening at compile time and what at runtime? Are we storing those strings strings the lookup keys yeah so one neat thing about this example is because the type system keeps track of all the keys we don't need to store them at runtime right so the way the example the way we had implemented that example, for a given regular expression, you knew what all the lookup keys are going to be. And so the type system would sort those keys into alphabetical order. So it would know exactly where in the result dictionary a particular lookup key had to be, right? So from this particular regular expression,

like we were getting the directories and the extensions and the file names, so we knew the directories would be the first part of that dictionary because D comes before E and comes before F, right? So we don't need to actually go and look at any keys because we know we know where where in the data structure we're going to store the values already. So we're looking up via with this compile time string and that's taking us to to it's accessing the part of actually using a dictionary is gone because that like the dictionary doesn't actually exist at runtime. It's just an array. Um, it's, it is a linked list and, um, we do know where it is, which index in the linked list we want to access at compile time. I'm not quite sure how much inlining goes on when the compiler, when GHC compiles it to know whether it will specialize it

to actually go right to that spot or whether you will have to actually go down to that point in the dictionary. Okay. In a theoretical sense, I mean, dependent types could, in theory, make things faster at runtime because, or is there overhead to having this extra information? So in a theoretical sense, we have more information at compile time.

So very much the compiler could take advantage of this information to make things faster. And there are examples of people using dependent types to speed up their code, to eliminate runtime pattern matching that they would have to do because they don't need it. Like if you know a check will always succeed, you can eliminate, the compiler can eliminate that check safely. So, I'm thinking of, I don't know if you read Yaron Mensky's blog. He is a CTO of Jane Street. So, the OCaml language also has GADETs. And about a year or two ago, he wrote a blog article about how they were able to use GADETs to, not just for the safety, but also to speed up part of their code

by eliminating these redundant checks. Oh, wow. We're just giving more information that can be used to optimize in some sense. Exactly. So what happens if I'm throwing away these keys? What happens if I want to print out this dictionary? Like I want a nice, you know, key equals value, key equals value, key equals value. Yeah, so we're not throwing them away because the compiler still knows about them when it compiles the program, right?

The type checker, the key that we have is in the type. And so for printing, right, in that part of the Strange Loop talk, I demonstrated how we could print out these dictionaries. And there I was taking advantage of Haskell's type classes, which are ways that this is a mechanism Haskell allows you to use compile time information to insert runtime values. The equivalent in Scala, I think, are implicit arguments, where you're using type information to control what argument you supply at runtime. In this case, our implicit information

is the name of the key, right? That's part of the type. And so in the runtime information that we're going to insert with the type class is the actual string that we're going to print out. So, again, part of a high-level theme is having a lot of flexibility between storing your information in the type at compile time and having it available to you at runtime. And when you're working in an expressive language like Haskell, you can go back and forth very easily where you can use the indices to kind of capture the connection between the runtime and the compile time data. And you can use type classes to have your compile time data control what runtime data is inserted by the compiler. And this works together very neatly. So the programmer doesn't need to add a lot of annotations or a lot of duplications, even though some parts of the program are at one level and other parts of the program are at a different level.

And I think you called this double-duty data. That's a little bit hard to say. Yeah, it was kind of a tongue twister. Yeah, so that's exactly what I mean in terms of having a compile-time view of your program and a runtime view of your program. Being able to use the same data to capture invariants about your code as indices on your types, right? So we know that we have to have this key in our dictionary. So we're going to use that key as part of our index. That's one way we're using that data.

And another way we're using that data is we need to have it at runtime. So, we need to use it to control what gets printed when we print out that dictionary. And having the flexibility to be able to use that data in both ways is what I meant by the double duty nature of it. One thing I think that is probably obvious to Haskell programmers, but maybe not others, like there's no reflection. Because I think it seems to me this, the different runtime versus compile time might break down if you were able to somehow inspect things like you can do in the JVM with reflection. Is that true or is it unrelated? It's very related, but in perhaps non-obvious ways. Okay.

Right. So, one, and the reason I'm pausing is that one thing that dependent types allow you to do is to encode a very principled form of reflection into your language. So Haskell actually does have some kinds of reflection using a library called data.typeable. So this library allows you to have runtime witnesses to types that usually are erased when you run your Haskell program. So how could this be? Well, in terms of the type system, it's using several different mechanisms. So it's using type classes to keep track of which types have runtime evidence and which types do not. And then it's using some of the same mechanisms that we use to implement GADETs to connect that runtime type information to the compile time types so that as

you use it, as you look at that runtime type information, you can do it safely. So Haskell does have a form of reflection, and that form of reflection is actually implemented using the same mechanism. So instead of reflection getting in the way of dependent types, we have dependent types allowing us to have a very safe form of reflection. And is data typable? Is that related to like generic deriving and scrap your boilerplate type stuff? So no, that's a different feature. So generic deriving.

So that's also... So typable is mainly concerned with runtime information about types based on their names, right? So whenever you create a data type in Haskell, you have a new name for a type. And the runtime information that it's storing, it doesn't remember what the structure of that data type definition is. It just remembers, I have a type that's called this name, and maybe it's applied to these arguments. For generic programming, you need that extra structure information. So generic programming in Haskell, especially generic deriving, It allows you to take the structure of a type and express how you might get kind of far by just saying, well, I know it has these constructors and these constructors take these arguments and I know how to show all the

arguments. So, to show it, we could have a generic version of show that just sort of looks at that structure information and figures out how to crawl over that tree and construct a string out of that data type, right? But in order to do that, you need to know what that structure looks like. You need to know how many constructors there are for each of those constructors, what the arguments to the constructors are. So I guess the question that we haven't really touched on is

how are we adding features to Haskell? Haskell exists, but how are you making it dependent or pushing it in that direction? So Haskell is a research language, and so it has been very open to experimentation with new features. So I have in the past and continuing been collaborating with the Haskell developers with new ideas for type system features. So, Haskell, the Glasgow Haskell compiler has this ability to introduce new features protected by language pragmas. So these language pragmas, they mark which source files adopt new features

so that it gives a little bit more flexibility so that we can look at features that aren't quite completely backwards compatible. So to enable a new feature on your Haskell program, you have to specifically ask for it. But in turn, that means that the new feature doesn't have to behave exactly the same on the old source code. And so, as we're extending the compiler, we don't have to worry so much about breaking old programs as much as we're providing access to new programs. Now, of course, as a research project, Haskell has been going for many, many years. So, there's quite a number of language features now. And it can get a little bit ridiculous about the number of language features that you might want to enable, especially since they are, a nice thing about it is they are defined at a very small level of granularity.

This is good for research into programming languages because if we have small language features, we can think about how they interact in lots of different combinations, as opposed to just throwing in every new feature that we want into one sort of monolithic, you know, enable dependent types that does everything. We can kind of look and see that, okay, this feature is good for dependent types, but we also see people using scope type variables just for lots of other applications that perhaps we had not even thought about. And we can tease that apart from sort of our initial ideas about how new language features might be used. Yeah, in your talk, I'll put a link in the show notes.

I recall like one of the first slides is basically just entirely full of extensions that you're enabling. And I mean, I guess that begs the question, how do these things not interact negatively? How do we have all these language extensions? It seems like there's an exponential amount of combinations of them. How do we have them cleanly sitting together? Or is there combinations that are verboten?

Usually they don't interact too much. I mean, that's a hard problem in general in language design, right? Generally, when we're looking at languages and we're thinking about new features, we may think about that new feature extended on a small core, but it's very, very difficult to think about how it interacts with every possible other combination. Now, the compiler does have to answer that question. How do all these language features interact? Because it has to implement every single one of them at the same time. So there is that. But in terms of will this feature interact with that feature, it has been the case in some compilers that two different features enabled at the same time

could expose a hole in the type system. And this kind of gets me to a recent research project that I'm looking at is being able to use proof assistance to do some of the type safety proofs for our programming languages, right? If you look at, so I'm specifically talking about type system extensions, right? Type system extensions, we develop them by making a mathematical model of the type system, extending that model and improving that whatever theorems we want to hold about our language still hold. Usually it's a theorem that's called type soundness that says that if your program type checks,

we have captured all the behaviors. Your program is not going to crash. And we do that feature by feature, but we don't typically define a model that has all of the features in it at once and prove our type system sound for that really, really big model. And the reason is it's really big. That's a lot of, that's a very detailed, detail heavy proof do, and it's very easy to kind of miss all the cases. And so, what I've been, one line of research that I have is, let's do all those proofs in a proof assistant. So, there are tools, so I use one that's called the Coq proof assistant,

that allows you to explain these mathematical models as programs in a type theory in a logical system, and then write down a theorem in that system, and then use programming to help develop those proofs. And so what that does, the benefit of that is that you have the proof assistant checking your proofs. And then you also, since your proofs are kind of developed programmatically, you can automate a lot of the sort of boilerplate aspects of your proof. And I think that's going to allow us to look at our features in combination at a scale that we haven't been able to do in the past. Interesting. An interesting thing I just thought of is, so Coq is also a, Coq is a type language, right? Yes. And so I'm assuming that you're kind of admitting that maybe Haskell's not, it's not up to the burden of doing this proof within Haskell. The dependent type system isn't as feature rich as a proof assistant because you're going out to another language to prove these.

Is that true? Yeah, so I'm using, so Coq, there is definite similarity here, right? Because they're both, Coq is an implementation of the dependent type theory that is an inspiration for Haskell's type system, or at least some of the extensions that I've made for it. But there's one very big difference between Coq's type theory and Haskell's type theory. And the big difference is that in Koch, there's this, there's, in addition to having this type soundness property to know that because things type check, they don't crash. We also have a much stronger property, which says that this type theory is consistent when we're looking at it as a logic. And this is kind of looking at your programs in a different way, where you're looking at programs as if they were proofs, and then the types are the propositions that they're proving.

So a proof and caulk is really saying, here is this type. I'm using the type to talk about something that I think should be true. And I know it's true because I'm giving you this proof, but that proof is just a functional program that has that type. And to know things are consistent, well, you have to be able to know that false propositions don't have proofs. So, in Coq, there's a particular proposition that's just called false. And there's no program that can have that type. So, we have types that are empty.

In Haskell, every single one of the types that we have in Haskell, there are functional programs that have that type. And the reason is we have things like we have in Haskell, there are functional programs that have that type. And the reason is we have things like infinite loops in Haskell. You can write an infinite loop, and you can give it whatever type that you want. And so that reason, we can't use Haskell as this logical foundation in the same way that we can use Cox type theory

because we don't have the termination analysis in Haskell that Koch does. And the type system hasn't made the decisions that Koch does to ensure this consistency of the language when we view it as a logic. This relates, I think, right, to totality checking. Like I know in Idris, you can turn on or off totality checking. Yeah. Yeah, this is exactly what I'm talking about. So in Idris, when you turn on the totality checking, you can use that part of the program to represent proofs.

But if you don't have the totality checker turned on, then the programs that you write in that part of the system can only be interpreted as programs. You can't treat them as proofs. In Haskell, we can't really use it in the same way to encode proofs as we do in Cox dependently typed functional programming language. Now, in your talk, you did talk about writing, I think, equality proofs in Haskell. So, in Haskell, there's actually another language embedded inside of Haskell that is the witness language for equality proofs. And users don't use that explicitly, but that language is manipulated by the Haskell type checker. And that language actually, it turns out, is consistent. It's not as expressive as Cox dependently type language, to encode specific equality proofs that you need to be able to provide the evidence that two types are equal, which is a lot of what you need to do when you're type checking, right?

So when you're type checking code, like the main question that you're asking when you're type checking is, is this, you know, is the type of this function of this argument appropriate to the type that this function expects? It's a lot of equality checking questions. And so, being able to justify to the type checker why two types are equal, that does require work sometime. And some of the work that you can do is controlling how these equality proofs are generated. And to me, like, I didn't really understand this, why this would be an important or hard thing until I started working through the Idris book. And as you start exposing this kind of, I guess, data at the type system, things get a little tricky.

So the easiest example that I hit was just like you have a vector and it has the length encoded in the type, right? But then you have a function that adds two vectors, right? And it's like vector n plus m, but you want to pass it where it's like vector n plus n. Like, just the arguments are reversed. It's very simple to see, like, for me that these are the same, but I have to somehow tell the type system that n plus m and n plus, you know, that this equivalence holds. Exactly.

And that's what I mean that where I say, like, equality proofs are a very essential part of type checking, right? Because you end up with a lot of questions like this. Is this expression that I'm using as a type index equal to this other expression that I'm using as a type index? And the type system itself is going to have a definition of when two things are equal, but that's not going to cover all of the cases when two types are equal. Just like, for example, the type system doesn't define this associativity of addition. This is something it doesn't know intrinsically. It's something that you have to justify to it via some kind of proof. Hmm. So, you have worked on a whole lot of extensions to the type system of Haskell.

The one that I've actually used is the generalized algebraic data types. So how is it? What's the process of working on that? Was it a challenge? Fun? Certainly fun. Yeah. So my role has been mostly on the theory side.

So looking at the mathematical models and making sure that things work well with how Haskell does type inference. And also Haskell has this statically typed core language that after type inference, it elaborates to the statically typed core language. And that's where we want to make sure that it has this type soundness property. So, my role has been to work with Haskell developers like Simon Payton-Jones, is one of the main developers of the Haskell language, collaborating with him about nailing down precisely what these extensions look like and doing proofs to make sure that they have the properties that they have. And also working with some of my PhD students who also assist him in extending the Glasgow Haskell compiler, GHC, with these new capabilities.

And as an academic, how does it work? Like, do you, so you're writing a paper about some extension. Is the extension written along with that, after that, before that? The paper discusses it in retrospect or? Usually we work on the implementation at the same time as we work on the theory, right? Because we want to have a complete view of what's going on with this extension. So the theory kind of tells us what guarantees we can get from this extension, but it doesn't tell us that the extension is actually useful. So for that, it's good to have an implementation where you can try out examples and make sure that the things that you want to use the extension for actually work. In terms of usefulness, do you collaborate with industry at all or how do you determine usefulness? Is it purely theoretical or is it looking at code?

So we look at a lot of code. So there's a lot of open source Haskell code out there. And in particular, so there was a package that I developed with my former PhD student, Richard Eisenberg, who's now an assistant professor at Bryn Mawr College. And we developed one package that's called the Singleton's Package. And it was a way of encoding dependent types in Haskell using GADTs without having actual dependent types. It was a way for us to kind of judge the usefulness of dependent types before actually doing the full

extension. And the nice thing is that we can go to the Haskell package repositories and look for other packages that depend on this particular library. So we can see what are people using dependent type like features for in practice? What kinds of code? How are they taking advantage of it? So that might be people in industry, that might be other research projects that are not about dependent types, but they want to take advantage of these Haskell features to do their particular application. Or it might be people who just want to code up interesting problems. Do you see dependent types filtering out outside of Haskell, outside of, you know, this very researchy type industry into mainstream programming languages?

I hope so. I mean, so already things like GADETS, right, so OCaml also supports GADETS, right? So, OCaml also supports GADETS. If you look at Scala, actually Scala has its own mechanisms for encoding dependent types that take advantage of some of the features of Scala that are different from Haskell. So, Scala's type system itself has already had to adopt a little bit of dependent type theory just to describe the interactions between the subtyping and objects and functional programming that happens in Scala. And I've seen some really great libraries that take advantage of that to push that to have more dependent type-like features in Scala itself. So I would love to see more of that in Scala. I would love to see more of that in all sorts of languages with static type systems.

Yeah, I think your example, I mean, shows how it could be quite useful in an interesting way, which is your, your regex library, um, as a user of it, um, you don't really need to know much about dependent types. The implementation uses them, right? But the actual user, they, they just use it and get this, get this extra features added. Yeah. And I think that's part of that is careful library design, right? Certainly dependent types are a power tool that if you're not careful, you can put heavy requirements on your users where they could end up with error messages that are not very obvious about how to fix it or how to use your library correctly. So, just like anything else, thinking about what your interface is and how people will interact with the functionality that you provide is an important part of

programming. And I think it's doubly so when you're working with the rich type systems of dependent type theory. I know, yeah, in Scala, like there is the shapeless library, which does a lot of dependently type looking things if you look at it correctly. And it's quite complex to use. However, it's used all over the place in a number of libraries. And I think that what ends up happening is it seems like every large-scale project has Shapeless included as some transitive dependency, right? So these features are being used just more by library creators than day-to-day users. So I think that could be a vision for how this could work. Yeah, I think that's completely appropriate, right? I mean, we kind of view programming as this monolithic thing, but it's not.

We have many different types of users coming into our languages at many different levels. And coming up with simple interfaces that newcomers can jump into to be able to do certain things quickly and easily is an important job that we have. But at the same time, we need to make sure that we have the powerful features that library designers need to be able to develop expressive and efficient libraries. So we're running a little, we're running out of time. I wanted to ask you, what's new and exciting in the world of programming language theory or type systems? Oh, that's always a hard question. What are you working on? What are you excited about? MIT on a project that we call the science of deep specifications. And the goal of this project is to bring verification that is provided by a system like the Cockproof Assistant to software systems at a very large scale, right? Not just proving individual little programs correct, but actually verifying a large part of your system,

from the hardware to your operating system to the compilers to the high-level languages that you use. So in my part of it, I am looking at how can I apply the Cockproof Assistant to verify and reason about the implementation of Haskell itself, of GHC. Can I use Coq to show that some of the optimizations and some of the transformations in the type system that GHC uses is correct? And we're just starting this out.

So we're just starting to be able to model Haskell code inside of Cox so that we can not just test the Haskell compiler to know that compilation is correct, but also have some much more formal guarantees. And as you were saying before, this might make it easier for future extensions because you'll have this proof to lean on? Yeah. So, hopefully this... So, I'll have a proof to lean on and hopefully this can also be a platform for being able to reason about the combination of the extensions. So, not just knowing that an individual extension is sound with respect to a small core language, but if we have a large proof of the entire system, we can think about how does that extension interact with everything else. Well, thank you so much for

your time, Stephanie. It's been great to talk to you. Thank you. I've enjoyed it.