TY - JOUR
T1 - Quantitative program reasoning with graded modal types
AU - Orchard, Dominic
AU - Liepelt, Vilem Benjamin
AU - Eades, Harley
N1 - Publisher Copyright:
© 2019 Copyright held by the owner/author(s).
PY - 2019/8
Y1 - 2019/8
N2 - In programming, some data acts as a resource (e.g., file handles, channels) subject to usage constraints. This poses a challenge to software correctness as most languages are agnostic to constraints on data. The approach of linear types provides a partial remedy, delineating data into resources to be used but never copied or discarded, and unconstrained values. Bounded Linear Logic provides a more fine-grained approach, quantifying non-linear use via an indexed-family of modalities. Recent work on coeffect types generalises this idea to graded comonads, providing type systems which can capture various program properties. Here, we propose the umbrella notion of graded modal types, encompassing coeffect types and dual notions of type-based effect reasoning via graded monads. In combination with linear and indexed types, we show that graded modal types provide an expressive type theory for quantitative program reasoning, advancing the reach of type systems to capture and verify a broader set of program properties. We demonstrate this approach via a type system embodied in a fully-fledged functional language called Granule, exploring various examples.
AB - In programming, some data acts as a resource (e.g., file handles, channels) subject to usage constraints. This poses a challenge to software correctness as most languages are agnostic to constraints on data. The approach of linear types provides a partial remedy, delineating data into resources to be used but never copied or discarded, and unconstrained values. Bounded Linear Logic provides a more fine-grained approach, quantifying non-linear use via an indexed-family of modalities. Recent work on coeffect types generalises this idea to graded comonads, providing type systems which can capture various program properties. Here, we propose the umbrella notion of graded modal types, encompassing coeffect types and dual notions of type-based effect reasoning via graded monads. In combination with linear and indexed types, we show that graded modal types provide an expressive type theory for quantitative program reasoning, advancing the reach of type systems to capture and verify a broader set of program properties. We demonstrate this approach via a type system embodied in a fully-fledged functional language called Granule, exploring various examples.
KW - Coeffects
KW - Graded modal types
KW - Implementation
KW - Linear types
UR - http://www.scopus.com/inward/record.url?scp=85120129336&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=85120129336&partnerID=8YFLogxK
U2 - 10.1145/3341714
DO - 10.1145/3341714
M3 - Article
AN - SCOPUS:85120129336
VL - 3
JO - Proceedings of the ACM on Programming Languages
JF - Proceedings of the ACM on Programming Languages
SN - 2475-1421
IS - ICFP
M1 - 110
ER -