Leftover Typing

Leftover typing refers to a technique used when implementing substructural type systems, i.e. type systems that ensure the careful use of a resource.

The technique amounts to presenting a typing relation as inputting a context of resources, using some of these to type the term in question, and outputting those that were not needing, aka the leftovers.

The technique appears to be independently due to Mackie 1994, and also due to Hodas and Miller 1994.

Allais 2018 also credits a technical report by Winiko and Harland 1994.

Please confirm this.

Example

Many such type systems have typing rules which make proof search and type inference difficult. For example, take a type system in which variables can only be used linearly. In that systems variables function as resources, and cannot be shared between different variables. A standard introduction rule for a product type \otimes would be of the form

\frac{
  \Gamma \vdash M : A
  \qquad
  \Delta \vdash N : B
}{
  \Gamma, \Delta \vdash (M, N) : A \otimes B
}

In this rule the context of the conclusion must be arbitrarily split into two parts, \Gamma and \Delta. \Gamma must consist of the variables that M will use, and \Delta must consist of the variables that N will use.

A completely naive solution to this problem would try all 2^n possible splittings of the context \Gamma, \Delta of length n. A somewhat better solution that works for this particular typing rule is to check which variables occur in which subterm (M or N) and split the context thus. But neither of those are good or general solutions to the problem.

Thus, the 'leftover' technique consists of writing the typing relation as

	\Gamma \vdash M : A\ |\ \Gamma'

This is read as follows: if in the context \Gamma we try to type M, we will find that it may have type A. Morevoer, the variables/resources of \Gamma that were not used in giving M the type A can be found in \Gamma'.

Mackie 1994 describes this solution as follows:

To reflect the linearity constraint that all assumptions must be used exactly once, we treat the assumption set as a set of resources-once used, we remove it. To this end our type reconstruction algorithm will return a triple ... which will consist of a substitution, a type and the assumptions not yet used.

References

• This technique appeared in Mackie's work on the linear functional programming language Lilac:

@article{mackie_1994,
	title = {Lilac: a functional programming language based on linear logic},
	volume = {4},
	issn = {0956-7968},
	doi = {10.1017/S0956796800001131},
	number = {04},
	journal = {Journal of Functional Programming},
	author = {Mackie, Ian},
	year = {1994},
	pages = {395}
}

• A very similar technique also appeared in the work of Hodas and Miller on linear logic programming:

@article{hodas_1994,
	title = {Logic {Programming} in a {Fragment} of {Intuitionistic} {Linear} {Logic}},
	volume = {110},
	doi = {10.1006/inco.1994.1036},
	number = {2},
	journal = {Information and Computation},
	author = {Hodas, J.S. and Miller, D.},
	year = {1994},
	pages = {327--365}
}

• A description of the technique in the context of mechanization can be found in

@InProceedings{allais_2018,
  author =	{Guillaume Allais},
  title =	{{Typing with Leftovers - A mechanization of Intuitionistic Multiplicative-Additive Linear Logic}},
  booktitle =	{23rd International Conference on Types for Proofs and  Programs (TYPES 2017)},
  pages =	{1:1--1:22},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  year =	{2018},
  volume =	{104},
  editor =	{Andreas Abel and Fredrik Nordvall Forsberg and Ambrus Kaposi},
  publisher =	{Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
  address =	{Dagstuhl, Germany},
}