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.
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 would be of the form
In this rule the context of the conclusion must be arbitrarily split into two parts, and . must consist of the variables that will use, and must consist of the variables that will use.
A completely naive solution to this problem would try all possible splittings of the context of length . A somewhat better solution that works for this particular typing rule is to check which variables occur in which subterm ( or ) 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
This is read as follows: if in the context we try to type , we will find that it may have type . Morevoer, the variables/resources of that were not used in giving the type can be found in .
[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.
Mackie, Ian. 1994. ‘Lilac: A Functional Programming Language Based on Linear Logic’. Journal of Functional Programming 4 (04): 395. https://doi.org/10.1017/S0956796800001131.
@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}
}
Hodas, J.S., and D. Miller. 1994. ‘Logic Programming in a Fragment of Intuitionistic Linear Logic’. Information and Computation 110 (2): 327–65. https://doi.org/10.1006/inco.1994.1036. [pdf]
@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}
}
Allais, Guillaume. 2018. ‘Typing with Leftovers - A Mechanization of Intuitionistic Multiplicative-Additive Linear Logic’. In 23rd International Conference on Types for Proofs and Programs (TYPES 2017), edited by Andreas Abel, Fredrik Nordvall Forsberg, and Ambrus Kaposi, 104:1:1-1:22. Leibniz International Proceedings in Informatics (LIPIcs). Dagstuhl, Germany: Schloss Dagstuhl–Leibniz-Zentrum fuer Informatik. https://doi.org/10.4230/LIPIcs.TYPES.2017.1.
@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},
}