Home

The Syntax and Semantics of Quantitative Type Theory

The Syntax and Semantics of Quantitative Type Theory by Robert Atkey:

Type Theory offers a tantalising promise: that we can program and reason within a single unified system. However, this promise slips away when we try to produce efficient programs. Type Theory offers little control over the intensional aspect of programs: how are computational resources used, and when can they be reused. Tracking resource usage via types has a long history, starting with Girard's Linear Logic and culminating with recent work in contextual effects, coeffects, and quantitative type theories. However, there is conflict with full dependent Type Theory when accounting for the difference between usages in types and terms. Recently, McBride has proposed a system that resolves this conflict by treating usage in types as a zero usage, so that it doesn't affect the usage in terms. This leads to a simple expressive system, which we have named Quantitative Type Theory (QTT).

McBride presented a syntax and typing rules for the system, as well as an erasure property that exploits the difference between “not used” and “used”, but does not do anything with the finer usage information. In this paper, we present present a semantic interpretation of a variant of McBride's system, where we fully exploit the usage information. We interpret terms simultaneously as having extensional (compile-time) content and intensional (runtime) content. In our example models, extensional content is set-theoretic functions, representing the compile-time or type-level content of a type-theoretic construction. Intensional content is given by realisers for the extensional content. We use Abramsky et al.'s Linear Combinatory Algebras as realisers, yield a large range of potential models from Geometry of Interaction, graph models, and syntactic models. Read constructively, our models provide a resource sensitive compilation method for QTT.

To rigorously define the structure required for models of QTT, we introduce the concept of a Quantitative Category with Families, a generalisation of the standard Category with Families class of models of Type Theory, and show that this class of models soundly interprets Quantitative Type Theory.

Resource-aware programming is a hot topic these days, with Rust exploiting affine and ownership types to scope and track resource usage, and with Ethereum requiring programs to spend "gas" to execute. Combining linear and dependent types has proven difficult though, so making it easier to track and reason about resource usage in dependent type theories would then be a huge benefit to making verification more practical in domains where resources are limited.

By naasking at 2017-07-25 17:28 | Semantics | Theory | Type Theory | other blogs | 32978 reads

Comment viewing options

Select your preferred way to display the comments and click "Save settings" to activate your changes.

Expressivity

This looks very interesting.

I am stuck a bit digesting the article: a desiderata for success is that it is possible to embed the simply typed lambda calculus in it, say in the 0/1/omega-annotated structure, but I don't see how the required structural rules, i.e., weakening and contraction are available over any annotation. Do these need to be added as additional inference rules? If so, what coherence proposition will the rules have to satisfy for the system to be well-behaved?

By Charles Stewart at Wed, 2017-07-26 10:28 | login or register to post comments

Embedding simple types

You've got two options for embedding simply typed terms:

  1. Any simply typed term G |- M : A can be embedded in the 0 usage fragment of QTT, embedding the simple function type A → B as (a :0 A) → B. When the result usage is 0, and (necessarily) all the context usages are 0, then the addition and scaling of contexts essentially does nothing because 0 + 0 = 0 and 0 * 0 = 0. The usual weakening and contraction rules are admissible (Lemma 3.4 for weakening, and a special case of Lemma 3.5 for contraction). Indeed, the system is designed so that the 0-usage fragment is a copy of normal MLTT.
  2. In QTT with the {0,1,omega} semiring, it is possible to embed Barber's Dual Intuitionistic Linear Logic (DILL). A DILL judgement G | D |- M : A becomes a QTT judgement where every binding in G is annotated with omega, every binding in D is annotated with 1, and the result binding is annotated 1. One could then link up the embedding of STLC into DILL to get another (resource annotated) embedding into {0,1,omega}-QTT.

Does that help? I'm not sure what you mean by "I don't see how the required structural rules, i.e., weakening and contraction are available over any annotation"? Surely you don't want weakening and contraction to be available at all usages?

By Bob Atkey at Wed, 2017-07-26 11:20 | login or register to post comments

Helps a bit

I certainly don't want weakening and contraction over 1, but I think I do want them over omega. It sounds like your second option, embedding DILL, is the right option, but it is precisely the possibility of embedding that I don't understand. How does this work?

By Charles Stewart at Wed, 2017-07-26 11:48 | login or register to post comments

Contraction and a Correction

Sorry, I made a mistake: the {0,1,omega} variant doesn't allow the direct embedding of DILL because it strictly distinguishes between non use, single use, and many uses, which DILL doesn't. So DILL can't be directly embedded because {0,1,omega}-QTT will distinguish between the type of functions that don't use their argument, and those that use it multiple times. DILL collapses these two possibilities. I think perhaps an extension of QTT with ordered semirings with 0 < 1 < omega would work, but this needs a bit of work. Thanks for making me aware of this extra requirement!

In general, the following contraction rule is admissible from the substitution lemma:

        G, x :r A, y :s A, G' |- M : B
  ---------------------------------------------
    G, x :(r+s) A, G'[x/y] |- M[x/y] : B[x/y]

By the rules of the {0,1,omega} semiring, we have r+omega=omega+r=omega, so contraction is admissible for multiply used things. It is perhaps useful to think of the annotations on variables as a analysis of the term: measuring how variables are used, rather than enforcing patterns of usage.

(QTT as in the paper also doesn't have an exponential modality as a type -- this is easy to add, but I ran out of space).

By Bob Atkey at Wed, 2017-07-26 17:16 | login or register to post comments

Thanks

This makes sense. I'll try to figure out the details of the embedding myself.

By Charles Stewart at Wed, 2017-07-26 18:34 | login or register to post comments