research-article

Open access

A graded dependent type system with a usage-aware semantics

Authors:

Pritam Choudhury,

Harley Eades III,

Richard A. Eisenberg,

Stephanie WeirichAuthors Info & Claims

Proceedings of the ACM on Programming Languages, Volume 5, Issue POPL

Article No.: 50, Pages 1 - 32

https://doi.org/10.1145/3434331

Published: 04 January 2021 Publication History

Abstract

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.

References

[1]

Martín Abadi, Anindya Banerjee, Nevin Heintze, and Jon G. Riecke. 1999. A Core Calculus of Dependency. In Proceedings of the 26th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (San Antonio, Texas, USA) ( POPL '99). Association for Computing Machinery, New York, NY, USA, 147-160. https://doi.org/10.1145/292540.292555 Andreas Abel. 2018. Resourceful Dependent Types. Presentation at 4th International Conference on Types for Proofs and Programs (TYPES 2018 ), Braga, Portugal.

[2]

Andreas Abel and Jean-Philippe Bernardy. 2020. A Unified View of Modalities in Type Systems. Proceedings of the ACM on Programming Languages 4, ICFP ( 2020 ). To appear.

Digital Library

[3]

Andreas Abel and Gabriel Scherer. 2012. On Irrelevance and Algorithmic Equality in Predicative Type Theory. Logical Methods in Computer Science 8, 1 ( 2012 ). https://doi.org/10.2168/LMCS-8( 1 :29) 2012

[4]

The Agda-Team. 2020. Run-time Irrelevance. https://agda.readthedocs. io/en/v2.6.1.1/language/runtime-irrelevance. html Robert Atkey. 2018. The Syntax and Semantics of Quantitative Type Theory. In LICS '18: 33rd Annual ACM/IEEE Symposium on Logic in Computer Science, July 9-12, 2018, Oxford, United Kingdom. https://doi.org/10.1145/3209108.3209189 H. P. Barendregt. 1993. Lambda Calculi with Types. Oxford University Press, Inc., USA, 117-309.

[5]

Bruno Barras and Bruno Bernardo. 2008. The Implicit Calculus of Constructions as a Programming Language with Dependent Types. In Foundations of Software Science and Computational Structures (FOSSACS 2008 ), Roberto Amadio (Ed.). Springer Berlin Heidelberg, Budapest, Hungary, 365-379.

[6]

P. N. Benton. 1995. A Mixed Linear and Non-Linear Logic: Proofs, Terms and Models (Extended Abstract). In Selected Papers from the 8th International Workshop on Computer Science Logic (CSL '94). Springer-Verlag, London, UK, UK, 121-135.

[7]

Jean-Philippe Bernardy, Mathieu Boespflug, Ryan R. Newton, Simon Peyton Jones, and Arnaud Spiwack. 2018. Linear Haskell: practical linearity in a higher-order polymorphic language. Proc. ACM Program. Lang. 2, POPL ( 2018 ), 5 : 1-5 : 29. https://doi.org/10.1145/3158093

Digital Library

[8]

Guillaume Bonfante, François Lamarche, and Thomas Streicher. 2001. A model of a dependent linear calculus. Intern report A01-R-262 || bonfante01c.

[9]

Edwin Brady. 2020. Idris 2: Quantitative Type Theory in Action. (Feb. 2020 ). Draft available from https://www.typedriven.org.uk/edwinb/idris-2-quantitative-type-theory-in-action.html.

[10]

Aloïs Brunel, Marco Gaboardi, Damiano Mazza, and Steve Zdancewic. 2014. A Core Quantitative Coefect Calculus. In Programming Languages and Systems, Zhong Shao (Ed.). Springer Berlin Heidelberg, Berlin, Heidelberg, 351-370.

[11]

Iliano Cervesato and Frank Pfenning. 2002. A Linear Logical Framework. Information and Computation 179, 1 ( 2002 ), 19-75.

[12]

Jawahar Chirimar, Carl A. Gunter, and Jon G. Riecke. 1996. Reference counting as a computational interpretation of linear logic. Journal of Functional Programming 6, 2 (March 1996 ), 195-244. https://doi.org/10.1017/S0956796800001660 U. Dal Lago and M. Gaboardi. 2011. Linear Dependent Types and Relative Completeness. In 2011 IEEE 26th Annual Symposium on Logic in Computer Science. 133-142.

[13]

Ugo Dal Lago and Martin Hofmann. 2009. Bounded Linear Logic, Revisited. In Typed Lambda Calculi and Applications, Pierre-Louis Curien (Ed.). Springer Berlin Heidelberg, Berlin, Heidelberg, 80-94.

[14]

Ugo Dal lago and Barbara Petit. 2012. Linear Dependent Types in a Call-by-Value Scenario. In Proceedings of the 14th Symposium on Principles and Practice of Declarative Programming (PPDP '12). Association for Computing Machinery, New York, NY, USA, 115-126.

[15]

Richard A. Eisenberg. 2016. Dependent Types in Haskell: Theory and Practice. Ph.D. Dissertation. University of Pennsylvania.

[16]

Richard A. Eisenberg. 2018. Quantifiers for Dependent Haskell. GHC Proposal # 102. https://github.com/goldfirere/ghcproposals/blob/pi/proposals/0000-pi.rst

[17]

Marco Gaboardi, Andreas Haeberlen, Justin Hsu, Arjun Narayan, and Benjamin C. Pierce. 2013. Linear Dependent Types for Diferential Privacy. In Proceedings of the 40th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL '13). Association for Computing Machinery, New York, NY, USA, 357-370.

[18]

Marco Gaboardi, Shin-ya Katsumata, Dominic A Orchard, Flavien Breuvart, and Tarmo Uustalu. 2016. Combining efects and coefects via grading. In ICFP. 476-489.

[19]

Dan R Ghica and Alex I Smith. 2014. Bounded linear types in a resource semiring. In European Symposium on Programming Languages and Systems. Springer, 331-350.

Digital Library

[20]

Jean-Yves Girard, Andre Scedrov, and Philip J. Scott. 1992. Bounded linear logic: a modular approach to polynomial-time computability. Theoretical Computer Science 97, 1 ( 1992 ), 1-66.

[21]

Jonathan S. Golan. 1999. Semirings and their Applications. Springer Netherlands. https://doi.org/10.1007/ 978-94-015-9333-5 Adam Gundry. 2013. Type Inference, Haskell and Dependent Types. Ph.D. Dissertation. University of Strathclyde.

[22]

Neelakantan R. Krishnaswami, Pierre Pradic, and Nick Benton. 2015. Integrating Linear and Dependent Types. In Proceedings of the 42Nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL '15). ACM, New York, NY, USA, 17-30.

Digital Library

[23]

John Launchbury. 1993. A natural semantics for lazy evaluation. POPL '93: Proceedings of the 20th ACM SIGPLAN-SIGACT symposium on Principles of programming languagesl (3 1993 ), 144-154. https://doi.org/10.1145/158511.158618 Conor McBride. 2016. I Got Plenty o' Nuttin'. Springer International Publishing, Cham, 207-233.

Digital Library

[24]

Alexandre Miquel. 2001. The Implicit Calculus of Constructions Extending Pure Type Systems with an Intersection Type Binder and Subtyping. Springer Berlin Heidelberg, Berlin, Heidelberg, 344-359. https://doi.org/10.1007/3-540-45413-6_27 Nathan Mishra-Linger and Tim Sheard. 2008. Erasure and Polymorphism in Pure Type Systems. In Foundations of Software Science and Computational Structures (FoSSaCS). Springer.

Digital Library

[25]

Benjamin Moon, Harley Eades III, and Dominic Orchard. 2020. Graded Modal Dependent Type Theory (Extended Abstract). TyDe (May 2020 ).

[26]

Jason Reed and Benjamin C. Pierce. 2010. Distance Makes the Types Grow Stronger: A Calculus for Diferential Privacy. In Proceedings of the 15th ACM SIGPLAN International Conference on Functional Programming (Baltimore, Maryland, USA) ( ICFP '10). Association for Computing Machinery, New York, NY, USA, 157-168. https://doi.org/10.1145/1863543.1863568 David N. Turner and Philip Wadler. 1999. Operational interpretations of linear logic. Theoretical Computer Science 227, 1 ( 1999 ), 231-248. https://doi.org/10.1016/S0304-3975 ( 99 ) 00054-7

Digital Library

[27]

Dennis Volpano, Cynthia Irvine, and Geofrey Smith. 1996. A Sound Type System for Secure Flow Analysis. J. Comput. Secur. 4, 2-3 ( Jan. 1996 ), 167-187.

Digital Library

[28]

Philip Wadler. 1990. Linear types can change the world. In IFIP TC, Vol. 2. 347-359.

[29]

Stephanie Weirich, Pritam Choudhury, Antoine Voizard, and Richard A. Eisenberg. 2019. A Role for Dependent Types in Haskell. Proc. ACM Program. Lang. 3, ICFP, Article 101 ( July 2019 ), 29 pages. https://doi.org/10.1145/3341705 Stephanie Weirich, Antoine Voizard, Pedro Henrique Avezedo de Amorim, and Richard A. Eisenberg. 2017. A Specification for Dependent Types in Haskell. Proc. ACM Program. Lang. 1, ICFP, Article 31 ( Aug. 2017 ), 29 pages. https://doi.org/10. 1145/3110275

Digital Library

[30]

James Wood and Robert Atkey. 2020. A Linear Algebra Approach to Linear Metatheory. arXiv: 2005. 02247 [cs.PL]

Cited By

Torczon CSuárez Acevedo EAgrawal SVelez-Ginorio JWeirich S(2024)Effects and Coeffects in Call-by-Push-ValueProceedings of the ACM on Programming Languages10.1145/36897508:OOPSLA2(1108-1134)Online publication date: 8-Oct-2024
https://dl.acm.org/doi/10.1145/3689750
Giannini PDuso GDi Stefano L(2024)Coeffects for MiniJava: Cf-MjProceedings of the 26th ACM International Workshop on Formal Techniques for Java-like Programs10.1145/3678721.3686232(30-36)Online publication date: 20-Sep-2024
https://dl.acm.org/doi/10.1145/3678721.3686232
Lorenzen AWhite LDolan SEisenberg RLindley S(2024)Oxidizing OCaml with Modal Memory ManagementProceedings of the ACM on Programming Languages10.1145/36746428:ICFP(485-514)Online publication date: 15-Aug-2024
https://dl.acm.org/doi/10.1145/3674642
Show More Cited By

Index Terms

A graded dependent type system with a usage-aware semantics
1. Theory of computation
  1. Logic
    1. Linear logic
    2. Type theory

Recommendations

A Graded Modal Dependent Type Theory with a Universe and Erasure, Formalized

We present a graded modal type theory, a dependent type theory with grades that can be used to enforce various properties of the code. The theory has Π-types, weak and strong Σ-types, natural numbers, an empty type, and a universe, and we also extend the ...
Partial Gradual Dependent Type Theory
SPLASH 2023: Companion Proceedings of the 2023 ACM SIGPLAN International Conference on Systems, Programming, Languages, and Applications: Software for Humanity

Gradual typing supports imprecise types in the type system, allowing incremental migration from untyped code to typed in the same language. Through the gradual typing approach, our ongoing work proposes a new theory based on the Martin-Löf type theory ...
Parametric quantifiers for dependent type theory

Polymorphic type systems such as System F enjoy the parametricity property: polymorphic functions cannot inspect their type argument and will therefore apply the same algorithm to any type they are instantiated on. This idea is formalized mathematically ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image Proceedings of the ACM on Programming Languages

Proceedings of the ACM on Programming Languages Volume 5, Issue POPL

January 2021

1789 pages

EISSN:2475-1421

DOI:10.1145/3445980

Issue’s Table of Contents

Copyright © 2021 Owner/Author.

This work is licensed under a Creative Commons Attribution International 4.0 License.

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 04 January 2021

Published in PACMPL Volume 5, Issue POPL

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Badges

Author Tags

Qualifiers

Research-article

Funding Sources

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

22
Total Citations
View Citations
1,429
Total Downloads

Downloads (Last 12 months)302
Downloads (Last 6 weeks)43

Reflects downloads up to 10 Dec 2024

Other Metrics

View Author Metrics

Citations

Cited By

Torczon CSuárez Acevedo EAgrawal SVelez-Ginorio JWeirich S(2024)Effects and Coeffects in Call-by-Push-ValueProceedings of the ACM on Programming Languages10.1145/36897508:OOPSLA2(1108-1134)Online publication date: 8-Oct-2024
https://dl.acm.org/doi/10.1145/3689750
Giannini PDuso GDi Stefano L(2024)Coeffects for MiniJava: Cf-MjProceedings of the 26th ACM International Workshop on Formal Techniques for Java-like Programs10.1145/3678721.3686232(30-36)Online publication date: 20-Sep-2024
https://dl.acm.org/doi/10.1145/3678721.3686232
Lorenzen AWhite LDolan SEisenberg RLindley S(2024)Oxidizing OCaml with Modal Memory ManagementProceedings of the ACM on Programming Languages10.1145/36746428:ICFP(485-514)Online publication date: 15-Aug-2024
https://dl.acm.org/doi/10.1145/3674642
Marshall DOrchard D(2024)Functional Ownership through Fractional UniquenessProceedings of the ACM on Programming Languages10.1145/36498488:OOPSLA1(1040-1070)Online publication date: 29-Apr-2024
https://dl.acm.org/doi/10.1145/3649848
Atkey R(2024)Polynomial Time and Dependent TypesProceedings of the ACM on Programming Languages10.1145/36329188:POPL(2288-2317)Online publication date: 5-Jan-2024
https://dl.acm.org/doi/10.1145/3632918
Liu YChan JShi JWeirich S(2024)Internalizing Indistinguishability with Dependent TypesProceedings of the ACM on Programming Languages10.1145/36328868:POPL(1298-1325)Online publication date: 5-Jan-2024
https://dl.acm.org/doi/10.1145/3632886
Marshall DOrchard D(2024)Non-linear communication via graded modal session typesInformation and Computation10.1016/j.ic.2024.105234301(105234)Online publication date: Dec-2024
https://doi.org/10.1016/j.ic.2024.105234
Hughes JOrchard D(2024)Program Synthesis from Graded TypesProgramming Languages and Systems10.1007/978-3-031-57262-3_4(83-112)Online publication date: 6-Apr-2024
https://dl.acm.org/doi/10.1007/978-3-031-57262-3_4
Bianchini RDagnino FGiannini PZucca E(2023)Resource-Aware Soundness for Big-Step SemanticsProceedings of the ACM on Programming Languages10.1145/36228437:OOPSLA2(1281-1309)Online publication date: 16-Oct-2023
https://dl.acm.org/doi/10.1145/3622843
Hanukaev PEades III HCong YDagand P(2023)Combining Dependency, Grades, and Adjoint LogicProceedings of the 8th ACM SIGPLAN International Workshop on Type-Driven Development10.1145/3609027.3609408(58-70)Online publication date: 30-Aug-2023
https://dl.acm.org/doi/10.1145/3609027.3609408
Show More Cited By

View Options

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Article

Media

Figures

Other

Tables

View Issue’s Table of Contents