This is a powerful technique for building programming languages that can then build on the Curry-Howard isomorphism and reap all of its benefits for program reasoning and building theorem provers. Now we take this core theory and we add the notion of grading, which is another well-established idea in which we take a type theory and augment it with some structured information which captures something about the underlying program structure or semantics.

In this case, we're going to be looking at data flow in the program and capturing it via grading, which can be thought of as an annotation system providing some kind of static analysis. Alongside this, we have a notion of graded modality, which captures the information of this grading and internalizes it into the type theory.

Now, the paper combines both the theory and the practice. We have an implementation called GURTT, which you can download, and I'm going to be using that today to demonstrate some of the key ideas. So let's start with the following typing judgment of a dependent type theory like Martin-Löfse.

The subject of this judgment is a term X, which is a variable, and we can see it has type A, and this A is itself determined by another variable. So in a dependent type theory, our variables can be used both in terms and at the type level.

We can see that A was used both here to form the type of X and over here to form the type of the subject. Now, in existing graded type systems, the idea is that we take a type theory like this and we add information that tells us about how variables are used.

So one particular approach would assign to X the grade one, which means that X is used once in the subject and A is given the grade zero, meaning it's not used in the subject. So this captures how variables are used computationally. And then this pushes onto the binders.

If we lambda abstract over A and X, then our type over here captures the grading that tells us how the parameters of this function are used computationally. And if we have more interesting data flow, for example, we're trying to build the term X pair X, then we see that X is used twice.

And that's represented by this grade here that says that X is used once in this sub-term plus the usage of one in this sub-term. And in type theories that are based on this idea, they have a semi-ring parameterizing them, which captures the data flow inherent to the structural rules of the type theory. So when we use a variable, it's a linear use that's counted by one of a semi-ring.

If we don't use a variable, then it's accounted for by zero of the semi-ring. If a variable is used in two sub-terms, then its grades are added using the additive part of the semi-ring. And if we sequentially compose parts of our program via a cut, via a substitution, then the multiplicative part of the semi-ring is used to multiply the grades.

And so these systems are parameterized by a semi-ring that captures the data flow. Now, this has been explored quite a lot. Various languages have been built out of this, and it's been used in various settings in context of the simply typed and polymorphically typed. And a lot of this work goes back to the notion of bounded linear logic, and a lot of these ideas can be seen as a generalization of this.

But in a dependently typed setting, that hasn't been explored quite as much. Although the notion of grading has been used to reconcile dependent types and linear types in the work of Connor McBride, which was then augmented by Bob Atkey and is known as quantitative type theory.

Now, these systems are graded. They have this semi-ring grading structure which accounts for how variables are used computationally. And if variables are used at the type level, then this is just counted as zero use. But it's a useful way of reconciling linear types and dependent types.

And there's been some other recent work following a similar idea. What we're doing here, though, is that we're going to treat types and computations uniformly when it comes to grading. So the grading is going to be able to speak about both type level use and computational use. And that's our system. This idea was also proposed by Andreas Abell, who had a related idea, which our system extends in various directions.

So now our notion of grading is going to contain two bits of information, which explains how a value or a parameter is used computationally, how it's used at the type level.

So going back to the polymorphic identity in our system, the typing looks like this, where this bit of information here grades at pairs. The left part explains the computational usage, which is zero for A, and the type level usage, which is two for A, because it appears twice in the rest of the type.

So what is this useful for? The systems that have used grading in the past at the computation level. So in combination with specifications, this gives us another way of reasoning about the behaviour of programs. So we're getting that same power for our type level computations as well. It also provides us a way to tame the power of dependent types. So

in a dependently typed setting, we lose parameteristic results when we go to higher types. This is a well-known problem with dependent types, which others have seeked to solve. For example, Neutz et al had a modal system which could bring back parameteristic into a dependent type theory.

And this is something that falls out of our work for free as just one particular application of grading. Another use is that we can use the grades to actually optimise the type checking procedure itself, using the kind of optimisations that we can use linear types and other kinds of grading for, but actually in the type level computations.

And our paper shows some experiments with this idea and shows that we can speed up type checking by 30 percent, even with just some simple optimisations based on grades. And furthermore, this provides us a way to reconcile previously difficult to reconcile type system features

like parameteristic and having type case, which lets us specialise our programs based on the types. And this is something that can be distinguished by grading. So we're going to see some more examples of this using the Gerty implementation. OK, so here's the polymorphic identity function written in Gerty, but it doesn't have any grades at the moment.

We can make this look like existing graded systems by adding the following annotations which explain how each of these parameters is used computationally. And Gerty accepts this. These underscores here are going to be filled in in a moment with type grades, which explain how the variable is used in the types.

But for now, we can leave those as underscores. And what Gerty does is calculates a constraint for them and is happy as long as this constraint is shown to be satisfiable. But we can fill this in as follows, saying that A is used twice in the type level and X is used not at all at the type level.

So the type theory is parametric in the semiring. In these examples, we're using a specific semiring of natural numbers to count exactly how many times we use our variables. So let's see another example where we use a variable more than once computationally, which is the copy function.

Here I take an X of type A and I use it twice to make a pair. So its computational use is twice, but its type level use is zero. And the use of A is zero times computationally, but we see it's used three times at the type level.

Now I'm going to use the copy function to make this function quad, which takes its parameter and it uses copy twice. So via composition, which is uses the multiplicative part of the semiring, we're going to see that X is used four times computationally and still zero times at the type level.

And A is used zero times computationally still and five times at the type level. And that's accepted by the type checker. Now, if we specified five uses here, the type check is going to complain because this is counting exact number of uses.

So we have to get that exactly right. So that uses the basic semiring, so the basic structure of our type theory. Another thing that we add is graded modalities, and those are useful when we want the grading of different parts of a compound piece of data structure to be different. So let's consider an example of this via the first projection function for pairs.

We want to take a pair of type AB and return an A. So the implementation which we might expect is we case on our input, pass and match on the pair and return the first component. This is going to be a type error, though, because there's a conflict here between the usage of U and the usage of V.

The type system is trying to assign this pair here, a single grade, but the usage of the component is different. So instead, we can insert a graded modal operator here, graded by zero, which tells us that we can use this part zero times once we eliminate the box.

So I'm going to do that via another layer of pattern matching like this where I use V once, I unbox it, I unbox it and use V prime zero times. And that's now well typed. So these are all examples using the natural number semiring, but the theory is parametric.

And just as a final example, using a different semiring, we can use the idea of a lattice of security levels here in the implementation and use that to track the security and confidentiality of data in the program.

So I'm going to go back to the polymorphic identity function again, but this time I'm going to grade it using a different semiring. And I'm going to say that I'm expecting the input here to be high security. Now this is going to be a type error because we don't want to leak the high security values out like this.

But if I change it to be low security, then that's allowed. So we can use this as a way of tracking other kinds of properties through our type system as well, both at the computation and type level. So let's see a little bit about how we define this type theory. Thanks, Dom. I'm Harley and I'm going to go through the theory of graded modal dependent types and summarize some of our results.

First, we start with a traditional definition of dependent type theory with dependent function types and dependent sum types in the style of a positive type whose eliminator is a pattern matching let expression. Then judgments consist of a typing context gamma, a term t called the subject, and the subject's type, a.

In dependent type theory, the variables in the typing context can depend on each other. The term t, the subject, can depend on variables from the context and the subject's type, a, can depend on elements of the context as well. With this in mind, we move to graded modal dependent type theory.

But the theory will now be parameterized by a semiring whose elements we call grades. Then to annotate judgments with grade information, we use grade vectors, which are used to describe the usage of free variables in the subject and the subject's type, and vectors of grade vectors, which are used to describe how free variables are used within the context.

We now use this data to define the syntax in the type judgment form. As we can see, we have a similar syntax to dependent type theory, but now binders have grade information attached to them. Function types are annotated with grades for the usage of x in the subject, here denoted by s, and the usage of x in the type b, denoted by r.

Functions and applications remain the same. Similarly, dependent sums have a grade on x called r that describes the usage of x and b, and since this variable is only used in the type b, we do not need a subject grade because it's always zero.

We then add to the syntax graded modalities, which allow for the grades to be internalized as a modality in the theory. Here the usage of a term with a graded modal type is described by a single grade, but this grade will account for how that term is used in both subjects and the subject's type.

Grade vectors are used to add grade information to the judgment. The grade vector context describes how the variables in gamma are used within gamma itself. The subject grade vector is used to describe the usage of the variables in gamma in the subject of the judgment.

And the subject's type grade vector, sigma 2, describes how the variables in gamma are used in the subject's type a. Let's consider a typing rule to help us in understanding how these are used during type checking. In this rule, we can see that the subject grade s is added to the subject grade vector and the grade r is added to the subject type grade vector when typing t.

But r is also added to the subject vector when typing b. An additional insight is that sigma 1 and sigma 3 are copied across both judgments. We retain the same grading because these copies are used for well-formedness checks rather than true usage. However, when we move down the rule, we combine these using addition to accumulate the type grade usage.

And this really stems from the fact that we have gamma copied across both premises. And this is true across the entire system, but the grade vectors will describe the usage of gamma in each premise. And so if something isn't used, then its grade will be zero.

Let's consider an example use of this rule. Consider the example we saw at the beginning of this talk, the polymorphic identity function. To type this function in GRTT, we begin with the lambda rule and move a into the context and its grade information into the subject and subject type grade vectors.

Since a is not used in the subject, it is graded with a zero. But we can see that a is used twice in the subject's type. And so we see two in the subject type grade vector. Moving forward, we add x to the context. But doing so adds a type dependency in the context between a and x.

And so the grade for a, here it was two, is split between the usage in the context and the subject's type. And so we add one grade vector to the grade vector context describing how each variable is used in the context. a is used once, but x is used zero times. Then the subject grade vector states that a is used zero times in the subject, but x is used once.

And finally, the situation is similar for the subject's type grade vector. We can finally discharge this using the variable rule. So that's GRTT in a nutshell. Please check out the paper for the rest of the details. To ensure we have a well-defined system, we proved a few meta-theoretic properties, namely graded substitution for typing,

which is perhaps the most important property for graded type systems. In addition, we proved type preservation and strong normalization. The latter is proved using reducibility candidates. Again, for the details, please check out the paper. There's still lots of work to be done.

For example, we would like to add approximation to the system by adding a pre-order to the semi-ring. This allows for more kinds of usage analysis, like non-exact usage and usage intervals. We are working on a categorical model for the system as well. Some interesting features for GRTT would be allowing the subject and the subject's type grades to be from different semi-rings

and to be able to internalize both of these using the graded modality. Also, we would like to make grades first-class citizens and then allow for the definition of semi-rings within the system itself, which would make for an extremely expressive system. Finally, we plan to make a number of improvements and conduct a number of experiments to and in GRTT.

Check out our website, download GRTT, and get in touch if you find this interesting. Also, a shout-out to Ben, who was unfortunately not able to give the presentation today. He's a PhD student working with Dominic. So if you have any interest in this, you can also contact him as well. Thank you.