Meeting on Graded Types
17th June 2022  School of Computing, University of Kent (+ online)
Graded type systems can be understood broadly as imbuing type systems with additional information that follows the underlying structure of a program or proof. This idea has grown considerably in recent years with various forms of graded type system being developed, for example, from generalisations of effect systems (modelled by graded monads), coeffect systems (modelled by graded comonads), quantitative type theories that generalise ideas from bounded linear logic, graded modal systems, contextual modal type theory, capability tracking systems, graded session types, adjoint logic and multi modal systems. In practical settings, graded type systems are becoming more prevalent, e.g., Granule, Idris 2, Haskell (via the LinearTypes extension).
The aim of this meeting is to bring together a wide variety of researchers working on such concepts across programming language theory and practice to report on latest work and share ideas. The hope is that this can be a precursor to future such meetings, e.g., a Dagstuhl seminar.
Schedule
This is a hybrid event. You can attend in person or online. All times listed refer to the local time in Canterbury, or in other words the UTC+1 timezone. On Thursday afternoon, there is a separate but related event running, hosted by David Corfield, that all are welcome to attend as part of this:

Thursday 16th afternoon  15pm  Grading in Philosophy, Linguistics and Computer Science
Further details of this workshop

Linguistic targets for graded modalities
Daniel Lassiter (University of Edinburgh)

Graded Modal Types for Finegrained Program Reasoning
Dominic Orchard (University of Kent and University of Cambridge)

Graded modalities and dependent type theory
David Corfield (University of Kent)


Friday 17th  Meeting on Graded Types

09:30  Opening remarks, Dominic Orchard
 09:40  Giving Semantics to ProgramCounter Labels via Secure Effects
Graded monads have been particularly successful in enforcing informationflow security and giving semantics to typeandeffect systems. However, works on informationflow security reason about effects no using a graded monad, but using special labels known as "programcounter labels." This work explores how programcounter labels interact with graded monads for effects, by showing that programcounter labels indeed have semantics as effects. Thus, we see that the adhoc reasoning about effects in informationflow circles is not so adhoc after all. Moreover, by using this semantics we are able to develop a proof technique we call "noninterference halfoff." This technique uses the monadic semantics of effects to ensure that programcounterlabel manipulations in an informationflow type system correctly ensure noninterference.
Andrew Hirsch (Max Planck Institute)
 10:10  Canonical gradings of monads
Many of the graded monads that have been used as models of effect systems "look like" graded versions of existing ordinary monads, in that, on each grade, they are given by restricting the monad. This raises the question of whether we can somehow canonically grade a given monad. It turns out that we can. Given a notion of subfunctor, we obtain a notion of grading of a monad, consisting of a collection of grades, and a subfunctor for each grade, forming a graded monad. Under reasonable conditions, every monad has a grading that is canonical (satisfies a particular universal property). I will talk about how this construction works, and demonstrate it with some examples. This is based on joint work with Flavien Breuvart and Tarmo Uustalu.
Dylan McDermott (University of Reykjavik)

10:40  Coffee break
 11:10  Beyond semirings
Semirings have served as the basic algebraic structure for abstracting over usage restriction schemes in most of our work. Addition captures accumulation, while muliplication captures modality. However, in certain settings we feel either that we can't find the right semiring (for example, to yield multiplicativeadditive linear logic) or that the semiring operations are not quite the ones we want (for example, when doing typechecking in the presence of additive units). In this talk, I will present both positive and negative results about semiringlike structures we may want to explore.
James Wood, (University of Strathclyde)
 11:40  Effects, capabilities, and boxes: from scopebased reasoning to typebased reasoning and back
Reasoning about the use of external resources is an important aspect of many practical applications. Effect systems enable tracking such information in types, but at the cost of complicating signatures of common functions. Capabilities coupled with escape analysis offer safety and natural signatures, but are often overly coarse grained and restrictive. We present SystemC, which builds on and generalizes ideas from typebased escape analysis and demonstrates that capabilities and effects can be reconciled harmoniously. By assuming that all functions are _second class_, we can admit natural signatures for many common programs. By introducing a notion of _boxed values_, we can lift the restrictions of secondclass values at the cost of needing to track degreeofimpurity information in types. The system we present is expressive enough to support effect handlers in full capacity. We practically evaluate SystemC in an implementation and prove its soundness.
Jonathan Brachthäuser (University of Tübingen)

12:10  Lunch
 13:30  Graded Types For Extensible Dynamic Natural Language Semantics
Research in dynamic semantics has made strides by studying various aspects of discourse in terms of computational effect systems, for example, monads (Shan, 2002; Unger, 2011; Charlow, 2014), continuations (de Groote, 2001; Barker and Shan, 2014), and general effect handlers (Maršik, 2016). We provide a system, based on graded monads, that synthesizes insights from these programs by formalizing individual discourse phenomena in terms of separate effects, or grades. Included are effects for introducing and retrieving discourse referents, nondeterminism for indefiniteness, and generalized quantifier meanings. We formalize the behavior of individual effects, as well as the interactions between effects, in terms of algebraic laws tailored to the relevant discourse phenomena. The system we propose is thus modular and suggests a novel approach to integrating formal accounts of distinct semantic phenomena. Finally, we give an interpretation of the system into pure λcalculus that respects the laws. Future work will aim to integrate more discourse phenomena using the same methodology, for example, presupposition and conventional implicature.
JeanPhilippe Bernardy (University of Gothenburg)
 14:00  Idris 2: Quantitative Type Theory in Practice
Dependent types allow us to express precisely what a function is intended to do. Recent work on Quantitative Type Theory (QTT) extends dependent type systems with linearity, also allowing precision in expressing when a function can run. This is promising, because it suggests the ability to design and reason about resource usage protocols, such as we might find in distributed and concurrent programming, where the state of a communication channel changes throughout program execution. Idris 2 is a new version of the dependently typed language Idris, with a new core language based on QTT, supporting linear and dependent types, which allows us to experiment with these ideas. I will describe Idris 2, and how QTT has influenced its design, giving examples of QTT in practice. Further, I will describe some limitations of QTT as implemented in Idris 2, which we would like to address in future work.
Edwin Brady (University of St. Andrews)
 14:30  From Ungraded to Graded: A Historical Perspective on Linear Type Systems
In this talk, I shall trace the evolution of linear type systems. The early linear type systems that followed the introduction of linear logic by Girard faced several syntactic problems, particularly with regard to substitution. The main reason behind these problems was their ungraded nature. Such systems implicitly assumed that every contextual assumption is linear in nature, thereby modelling nonlinear assumptions as linear !assumptions. This modelling came with a price  in these systems, the promotion rule does not commute with substitution. To address this problem, later systems baked substitution directly into the promotion rule. But that made their promotion rule quite complicated. Soon it was realized that a graded presentation of a linear type system can be simpler and more elegant. Two such graded linear type systems were introduced in quick succession  Linear/Nonlinear Lambdacalculus by Benton and Dual Intuitionistic Linear Logic by Barber. These systems split contexts into two zones, one containing linear assumptions and the other containing nonlinear ones. With this grading of contexts, these systems did away with the syntactic problems their earlier counterparts faced.
Benton's and Barber's systems are graded; however, the grades are tightly coupled with the contextual zones in these systems. While this coupling does not present any problem in simple linear type systems, it becomes a limiting factor in the design of dependent linear type systems. So for a long time linear types and dependent types didn't see eye to eye.
Meanwhile, progress was being made in the design of general graded type systems for tracking coeffects. Coeffects, of which linearity is but an example, model how computations depend upon their contexts. A distinguishing feature of these coeffecttracking systems is that they represent coeffects using elements of an abstract semiring and use those elements to grade the contextual assumptions. Instead of dividing the context into graded zones, these systems grade individual assumptions and manipulate those grades via the semiring operations. Such a grading mechanism allows an assumption to appear at different grades in typing rules with two or more premise judgments; something that would be quite difficult to allow with zoned contexts. This flexibility provided by general graded type systems set the stage required for the design of a dependent linear type system.
However, a final breakthrough was necessary: the realization that 0 can be used as a placeholder to mark assumptions that cannot be `consumed'. McBride provided this final breakthrough and integrated linear types and dependent types in an elegant manner. In fact, he went further by treating 0 as a number in its own right, thereby enabling a simultaneous analysis of irrelevance in his linear dependent type system. McBride's system inspired the design of several linear dependent systems, notably QTT, GraD, Grtty, etc. and is a topic of ongoing research. His system also forms the basis of runtime irrelevance analysis in Agda and linearity analysis in Idris 2.
This evolution of linear type systems parallels the evolution of numbers in human history. First, there was just a numbersense. Then came the numbers, but they were tightly connected to physical objects like notches on bones, knots on strings, beads on abacus, etc. Finally, people learned to see numbers abstractly. This final breakthrough was made possible, in part, by the positional numeral system and the discovery of 0, first as a placeholder and then as a number in its own right.
Pritam Choudhury (University of Pennsylvania)

15:00  Coffee break
 15:30  A Mixed Linear and Graded Logic
Benton showed in his seminal paper on Linear/NonLinear logic and models that the ofcourse modality of linear logic can be split into two modalities connecting intuitionistic logic with linear logic forming a symmetric monoidal adjunction. In this paper, we give a similar result showing that graded modalities can be split into two modalities connecting graded logic with linear logic. We propose a sequent calculus, its proof theory and categorical model, and a natural deduction system in the form of a term assignment system which is shown to be isomorphic to the sequent calculus. One interesting aspect of our system is it can be seen as Linear/NonLinear logic composed with an action that adds the grading.
Harley Eades III, (Augusta University)

16:00  Short talk session
 16:0016:15  Unifying models of linear/graded dependent types Bob Atkey
 16:1516:30  Gradual Typing for Effects & Handlers Max New
 16:3016:45  Program synthesis with linear and graded types Jack Hughes
 16:4517:00  Graded session types Daniel Marshall
 17:0017:15  Modal Subtyping for Grade Inference Michael Arntzenius
 17:1517:30  Weighted Sets and Modalities Vikraman Choudhury
 17:30  Close

Signing up and attending in person
 Sign up here
 Please tick ‘In person’ if you would like to attend in person on the form.
 The School of Computing at the University of Kent is about 30 minute walk from Canterbury West station in the Cornwallis South building. Canterbury West is a bit less than an hour on the train from St. Pancras

There is a lot of accommodation nearby if you want to stay overnight. One recommendation is Acacia Lodge (which is near to the train station and again about 30 minutes walk from campus) or the Beverly Farmhouse (which is on campus).

Any questions please contact Dominic Orchard.