TY - JOUR
T1 - A graded dependent type system with a usage-aware semantics
AU - Choudhury, Pritam
AU - Eades, Harley
AU - Eisenberg, Richard A.
AU - Weirich, Stephanie
N1 - Funding Information:
This material is based upon work supported by the National Science Foundation under Grant No. 1521539, and Grant No. 1704041. Any opinions, findings, and conclusions or recommendations expressed in this material are those of the author and do not necessarily reflect the views of the National Science Foundation.
Publisher Copyright:
© 2021 Owner/Author.
PY - 2021/1
Y1 - 2021/1
N2 - Graded Type Theory provides a mechanism to track and reason about resource usage in type systems. In this paper, we develop GraD, a novel version of such a graded dependent type system that includes functions, tensor products, additive sums, and a unit type. Since standard operational semantics is resource-agnostic, we develop a heap-based operational semantics and prove a soundness theorem that shows correct accounting of resource usage. Several useful properties, including the standard type soundness theorem, non-interference of irrelevant resources in computation and single pointer property for linear resources, can be derived from this theorem. We hope that our work will provide a base for integrating linearity, irrelevance and dependent types in practical programming languages like Haskell.
AB - Graded Type Theory provides a mechanism to track and reason about resource usage in type systems. In this paper, we develop GraD, a novel version of such a graded dependent type system that includes functions, tensor products, additive sums, and a unit type. Since standard operational semantics is resource-agnostic, we develop a heap-based operational semantics and prove a soundness theorem that shows correct accounting of resource usage. Several useful properties, including the standard type soundness theorem, non-interference of irrelevant resources in computation and single pointer property for linear resources, can be derived from this theorem. We hope that our work will provide a base for integrating linearity, irrelevance and dependent types in practical programming languages like Haskell.
KW - Irrelevance
KW - heap semantics
KW - linearity
KW - quantitative reasoning
UR - http://www.scopus.com/inward/record.url?scp=85098824564&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=85098824564&partnerID=8YFLogxK
U2 - 10.1145/3434331
DO - 10.1145/3434331
M3 - Article
AN - SCOPUS:85098824564
SN - 2475-1421
VL - 5
JO - Proceedings of the ACM on Programming Languages
JF - Proceedings of the ACM on Programming Languages
IS - POPL
M1 - 50
ER -