research-article

Lightweight linear types in system f°

Authors:

Steve ZdancewicAuthors Info & Claims

TLDI '10: Proceedings of the 5th ACM SIGPLAN workshop on Types in language design and implementation

Pages 77 - 88

https://doi.org/10.1145/1708016.1708027

Published: 23 January 2010 Publication History

Abstract

We present System F°, an extension of System F that uses kinds to distinguish between linear and unrestricted types, simplifying the use of linearity for general-purpose programming. We demonstrate through examples how System F° can elegantly express many useful protocols, and we prove that any protocol representable as a DFA can be encoded as an F° type. We supply mechanized proofs of System F°'s soundness and parametricity properties, along with a nonstandard operational semantics that formalizes common intuitions about linearity and aids in reasoning about protocols.

We compare System F° to other linear systems, noting that the simplicity of our kind-based approach leads to a more explicit account of what linearity is meant to capture, allowing otherwise-conflicting interpretations of linearity (in particular, restrictions on aliasing versus restrictions on resource usage) to coexist peacefully. We also discuss extensions to System F^o aimed at making the core language more practical, including the additive fragment of linear logic, algebraic datatypes, and recursion.

References

[1]

Amal Ahmed, Matthew Fluet, and Greg Morrisett. A step-indexed model of substructural state. In ICFP '05: Proceedings of the tenth ACM SIGPLAN international conference on Functional programming, pages 78--91, New York, NY, USA, 2005. ACM.

Digital Library

[2]

Amal Ahmed, Matthew Fluet, and Greg Morrisett. L3: A linear language with locations. Fundam. Inf., 77(4):397--449, 2007.

Digital Library

[3]

Andrew Barber. Linear Type Theories, Semantics and Action Calculi. PhD thesis, Edinburgh University, 1997.

[4]

Nick Benton, G. M. Bierman, J. Martin E. Hyland, and Valeria de Paiva. A term calculus for intuitionistic linear logic. In M. Bezem and J. F. Groote, editors, Proceedings of the International Conference on Typed Lambda Calculi and Applications, pages 75--90. Springer-Verlag LNCS 664, 1993.

Digital Library

[5]

P. N. Benton. A mixed linear and non-linear logic: proofs, terms and models. In Proceedings of Computer Science Logic (CSL '94), Kazimierz, Poland., pages 121--135. Springer-Verlag, 1995.

Digital Library

[6]

G. M. Bierman, A. M. Pitts, and C. V. Russo. Operational properties of lily, a polymorphic linear lambda calculus with recursion. In Fourth International Workshop on Higher Order Operational Techniques in Semantics, Montral, volume 41 of Electronic Notes in Theoretical Computer Science. Elsevier, 2000.

[7]

Gavin M. Bierman. Program equivalence in a linear functional language. Journal of Functional Programming, 10(2), 2000.

Digital Library

[8]

Lars Birkedal, Rasmus Ejlers Møgelberg, and Rasmus Lerchedahl Petersen. Category-theoretic models of Linear Abadi & Plotkin Logic. Theory and Applications in Categories, 20(7), 2008.

[9]

Arthur Charguéraud and Franc¸ois Pottier. Functional translation of a calculus of capabilities. In ICFP '08: Proceeding of the 13th ACM SIGPLAN international conference on Functional programming, pages 213--224, New York, NY, USA, 2008. ACM.

Digital Library

[10]

Karl Crary, David Walker, and Greg Morrisett. Typed memory management in a calculus of capabilities. In Proc. 26th ACM Symp. on Principles of Programming Languages (POPL), pages 262--275, San Antonio, Texas, January 1999.

Digital Library

[11]

Robert DeLine and Manuel Fähndrich. Enforcing high-level protocols in low-level software. In Proc. of the SIGPLAN Conference on Programming Language Design, pages 59--69, Snowbird, UT, June 2001.

Digital Library

[12]

Manuel Fähndrich, Mark Aiken, Chris Hawblitzel, Orion Hodson, Galen Hunt, James R. Larus, and Steven Levi. Language support for fast and reliable message-based communication in singularity os. SIGOPS Oper. Syst. Rev., 40(4):177--190, 2006.

Digital Library

[13]

Manuel Fähndrich and Robert DeLine. Adoption and focus: Practical linear types for imperative programming. In Proc. of the SIGPLAN Conference on Programming Language Design, pages 13--24, Berlin, Germany, June 2002.

Digital Library

[14]

Jean-Yves Girard. Interprétation fonctionnelle et élimination des coupures de l'arith mé tique d'ordre supérieur. Thèse d'état, University of Paris VII, 1972. Summary in J. E. Fenstad, editor, Scandinavian Logic Symposium, pp. 63--92, North-Holland, 1971.

[15]

Jean-Yves Girard. Linear logic. Theoretical Computer Science, 50:1--102, 1987.

Digital Library

[16]

Jean-Yves Girard, Y. Lafont, and P. Taylor. Proofs and Types. Cambridge University Press, 1989.

Digital Library

[17]

Michael Hicks, Greg Morrisett, Dan Grossman, and Trevor Jim. Experience with safe manual memory-management in Cyclone. In ISMM'04: Proceedings of the 4th international symposium on Memory management, pages 73--84, New York, NY, USA, 2004. ACM.

Digital Library

[18]

Kohei Honda, Vasco T. Vasconcelos, and Makoto Kubo. Language primitives and type discipline for structured communication-based programming. In ESOP98, volume 1381 of LNCS, pages 122--138. Springer-Verlag, 1998.

Digital Library

[19]

Atsushi Igarashi and Naoki Kobayashi. Resource usage analysis. ACM Trans. Program. Lang. Syst., 27(2):264--313, 2005.

Digital Library

[20]

Oleg Kiselyov and Chung-chieh Shan. Lightweight monadic regions. In Haskell '08: Proceedings of the first ACM SIGPLAN symposium on Haskell, pages 1--12, New York, NY, USA, 2008. ACM.

Digital Library

[21]

Yves Lafont. The linear abstract machine. Theoretical Computer Science, 59:157--180, 1988. Some corrections in volume 62 (1988), pp. 327--328.

Digital Library

[22]

Patrick Lincoln and John Mitchell. Operational aspects of linear lambda calculus. In 7th Symposium on Logic in Computer Science, IEEE, pages 235--246. IEEE Computer Society Press, 1992.

[23]

John C. Reynolds. Towards a theory of type structure. In Programming Symposium, volume 19 of Lecture Notes in Computer Science, pages 408--425. Springer-Verlag, Paris, France, April 1974.

Digital Library

[24]

John C. Reynolds. Types, abstraction, and parametric polymorphism. In R.E.A Mason, editor, Information Processing, pages 513--523. Elsevier Science Publishers B.V., 1983.

[25]

Kaku Takeuchi, Kohei Honda, and Makoto Kubo. An interactionbased language and its typing system. In Proceedings of PARLE'94, pages 398--413. Springer-Verlag, 1994. Lecture Notes in Computer Science number 817.

Digital Library

[26]

David N. Turner and Philip Wadler. Operational interpretations of linear logic. Theoretical Computer Science, 227(1-2):231--248, September 1999.

Digital Library

[27]

Vasco T. Vasconcelos, Simon J. Gay, and António Ravara. Type checking a multithreaded functional language with session types. Theoretical Computer Science, 368(1--2):64--87, 2006.

Digital Library

[28]

Edsko Vries, Rinus Plasmeijer, and David M. Abrahamson. Uniqueness typing simplified. In Implementation and Application of Functional Languages: 19th International Workshop, IFL 2007, Freiburg, Germany, September 27-29, 2007. Revised Selected Papers, pages 201--218, Berlin, Heidelberg, 2008. Springer-Verlag.

Digital Library

[29]

Philip Wadler. Linear types can change the world! In M. Broy and C. Jones, editors, Progarmming Concepts and Methods, Sea of Galilee, Israel, April 1990. North Holland. IFIP TC 2 Working Conference.

[30]

Philip Wadler. There's no substitute for linear logic. In 8th International Workshop on the Mathematical Foundations of Programming Semantics, 1992.

[31]

PhilipWadler. A taste of linear logic. In Mathematical Foundations of Computer Science, volume 711 of Lecture Notes in Computer Science, pages 185--210. Springer-Verlag, 1993.

Digital Library

[32]

David Walker. A type system for expressive security policies. In Proc. 27th ACM Symp. on Principles of Programming Languages (POPL), pages 254--267. ACM Press, Jan 2000.

Digital Library

[33]

David Walker. Advanced Topics in Types and Programming Languages, chapter Substructural Type Systems. MIT Press, 2005.

[34]

Keith Wansbrough and Simon Peyton Jones. Once upon a polymorphic type. In POPL '99: Proceedings of the 26th ACM SIGPLANSIGACT symposium on Principles of programming languages, pages 15--28, New York, NY, USA, 1999. ACM.

Digital Library

[35]

Andrew K. Wright and Matthias Felleisen. A syntactic approach to type soundness. Information and Computation, 115(1):38--94, 1994. Preliminary version in Rice TR 91-160.

Digital Library

[36]

Dengping Zhu and Hongwei Xi. Safe Programming with Pointers through Stateful Views. In Proceedings of the 7th International Symposium on Practical Aspects of Declarative Languages, pages 83--97, Long Beach, CA, January 2005. Springer-Verlag LNCS vol. 3350.

Digital Library

Cited By

van Rooij OKrebbers R(2025)Affect: An Affine Type and Effect SystemProceedings of the ACM on Programming Languages10.1145/37048419:POPL(126-154)Online publication date: 9-Jan-2025
https://dl.acm.org/doi/10.1145/3704841
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
Tang WHillerström DLindley SMorris J(2024)Soundly Handling LinearityProceedings of the ACM on Programming Languages10.1145/36328968:POPL(1600-1628)Online publication date: 5-Jan-2024
https://dl.acm.org/doi/10.1145/3632896
Show More Cited By

Index Terms

Lightweight linear types in system f°
1. Software and its engineering
  1. Software notations and tools
    1. General programming languages
      1. Language features

Recommendations

System F with coercion constraints
CSL-LICS '14: Proceedings of the Joint Meeting of the Twenty-Third EACSL Annual Conference on Computer Science Logic (CSL) and the Twenty-Ninth Annual ACM/IEEE Symposium on Logic in Computer Science (LICS)

We present a second-order λ-calculus with coercion constraints that generalizes a previous extension of System F with parametric coercion abstractions by allowing multiple but simultaneous type and coercion abstractions, as well as recursive coercions ...
Imperative Polymorphism by Store-Based Types as Abstract Interpretations
PEPM '15: Proceedings of the 2015 Workshop on Partial Evaluation and Program Manipulation

Dealing with polymorphism in the presence of imperative features is a long-standing open problem for Hindley-Milner type systems. A widely adopted approach is the value restriction, which inhibits polymorphic generalisation and unfairly rejects various ...
Type inference in intuitionistic linear logic
PPDP '10: Proceedings of the 12th international ACM SIGPLAN symposium on Principles and practice of declarative programming

We study the type checking and type inference problems for intuitionistic linear logic: given a System F typed λ-term, (i) for an alleged linear logic type, determine whether there exists a corresponding typing derivation in linear logic (type checking) ...

Comments

Information & Contributors

Information

Published In

cover image ACM Conferences

TLDI '10: Proceedings of the 5th ACM SIGPLAN workshop on Types in language design and implementation

January 2010

108 pages

ISBN:9781605588919

DOI:10.1145/1708016

General Chair:
Andrew Kennedy
Microsoft Research Cambridge, UK
,
Program Chair:
Nick Benton
Microsoft Research Cambridge, UK

Copyright © 2010 ACM.

Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]

Sponsors

SIGPLAN: ACM Special Interest Group on Programming Languages

In-Cooperation

SIGACT: ACM Special Interest Group on Algorithms and Computation Theory

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 23 January 2010

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Research-article

Conference

POPL '10

Sponsor:

SIGPLAN

POPL '10: The 37th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages

January 23, 2010

Madrid, Spain

Acceptance Rates

Overall Acceptance Rate 11 of 26 submissions, 42%

Upcoming Conference

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

54
Total Citations
View Citations
281
Total Downloads

Downloads (Last 12 months)13
Downloads (Last 6 weeks)1

Reflects downloads up to 08 Mar 2025

Other Metrics

View Author Metrics

Citations

Cited By

van Rooij OKrebbers R(2025)Affect: An Affine Type and Effect SystemProceedings of the ACM on Programming Languages10.1145/37048419:POPL(126-154)Online publication date: 9-Jan-2025
https://dl.acm.org/doi/10.1145/3704841
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
Tang WHillerström DLindley SMorris J(2024)Soundly Handling LinearityProceedings of the ACM on Programming Languages10.1145/36328968:POPL(1600-1628)Online publication date: 5-Jan-2024
https://dl.acm.org/doi/10.1145/3632896
MATSUDA KWANG M(2024) Sparcl : A language for partially invertible computation Journal of Functional Programming10.1017/S095679682300012634Online publication date: 26-Jan-2024
https://doi.org/10.1017/S0956796823000126
Almeida BMordido AVasconcelos V(2023)Kind Inference for the FreeST Programming LanguageElectronic Proceedings in Theoretical Computer Science10.4204/EPTCS.378.1378(1-13)Online publication date: 13-Apr-2023
https://doi.org/10.4204/EPTCS.378.1
Mordido ASpaderna JThiemann PVasconcelos V(2023)Parameterized Algebraic ProtocolsProceedings of the ACM on Programming Languages10.1145/35912777:PLDI(1389-1413)Online publication date: 6-Jun-2023
https://dl.acm.org/doi/10.1145/3591277
Gonnord LHenrio LMorel LRadanne G(2023)A Survey on Parallelism and DeterminismACM Computing Surveys10.1145/356452955:10(1-28)Online publication date: 2-Feb-2023
https://dl.acm.org/doi/10.1145/3564529
Quiña-Mera AFernandez PGarcía JRuiz-Cortés A(2023)GraphQL: A Systematic Mapping StudyACM Computing Surveys10.1145/356181855:10(1-35)Online publication date: 2-Feb-2023
https://dl.acm.org/doi/10.1145/3561818
Ganapathi IAli SPrakash SVu NWerghi N(2023)A Survey of 3D Ear Recognition TechniquesACM Computing Surveys10.1145/356088455:10(1-36)Online publication date: 2-Feb-2023
https://dl.acm.org/doi/10.1145/3560884
Chiarot GSilvestri C(2023)Time Series Compression SurveyACM Computing Surveys10.1145/356081455:10(1-32)Online publication date: 2-Feb-2023
https://dl.acm.org/doi/10.1145/3560814
Show More Cited By

View Options

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 Publication

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Figures

Tables

Media

View Table of Conten