More Web Proxy on the site http://driver.im/

research-article

Open access

Kinds are calling conventions

Authors:

Zena M. Ariola,

Simon Peyton Jones,

Richard A. EisenbergAuthors Info & Claims

Proceedings of the ACM on Programming Languages, Volume 4, Issue ICFP

Article No.: 104, Pages 1 - 29

https://doi.org/10.1145/3408986

Published: 03 August 2020 Publication History

Abstract

A language supporting polymorphism is a boon to programmers: they can express complex ideas once and reuse functions in a variety of situations. However, polymorphism is pain for compilers tasked with producing efficient code that manipulates concrete values.

This paper presents a new intermediate language that allows for efficient static compilation, while still supporting flexible polymorphism. Specifically, it permits polymorphism over not only the types of values, but also the representation of values, the arity of primitive machine functions, and the evaluation order of arguments---all three of which are useful in practice. The key insight is to encode information about a value's calling convention in the kind of its type, rather than in the type itself.

Supplementary Material

Presentation at ICFP '20 (a104-downen-presentation.mp4)

Download
147.31 MB

References

[1]

Jean-Marc Andreoli. 1992. Logic Programming with Focusing Proofs in Linear Logic. Journal of Logic and Computation 2, 3 ( 1992 ), 297-347. https://doi.org/10.1093/logcom/2.3. 297

[2]

Zena M. Ariola and Matthias Felleisen. 1997. The Call-By-Need Lambda Calculus. Journal of Functional Programming 7, 3 (May 1997 ), 265-301. https://doi.org/10.1017/S0956796897002724

Digital Library

[3]

Maximilian C. Bolingbroke and Simon L. Peyton Jones. 2009. Types Are Calling Conventions. In Proceedings of the 2nd ACM SIGPLAN Symposium on Haskell (Edinburgh, Scotland) ( Haskell '09). ACM, 1-12.

[4]

Joachim Breitner. 2014. Call Arity. In Trends in Functional Programming-15th International Symposium, TFP 2014, Soesterberg, The Netherlands, May 26-28, 2014. Revised Selected Papers. 34-50.

[5]

Joachim Breitner, Richard A. Eisenberg, Simon Peyton Jones, and Stephanie Weirich. 2016. Safe zero-cost coercions for Haskell. Journal of Functional Programming 26 ( 2016 ), e15. https://doi.org/10.1017/S0956796816000150

[6]

Zaynah Dargaye and Xavier Leroy. 2009. A verified framework for higher-order uncurrying optimizations. Higher-Order and Symbolic Computation 22, 3 ( 2009 ), 199-231.

[7]

Paul Downen and Zena M. Ariola. 2018. Beyond Polarity: Towards a Multi-Discipline Intermediate Language with Sharing. In 27th EACSL Annual Conference on Computer Science Logic, CSL 2018, September 4-7, 2018, Birmingham, UK. 21 : 1-21 : 23.

[8]

Paul Downen, Zachary Sullivan, Zena M. Ariola, and Simon Peyton Jones. 2019. Making a Faster Curry with Extensional Types. In Proceedings of the 12th ACM SIGPLAN International Symposium on Haskell (Berlin, Germany) ( Haskell 2019 ). Association for Computing Machinery, New York, NY, USA, 58-70. https://doi.org/10.1145/3331545.3342594

Digital Library

[9]

Joshua Dunfield. 2015. Elaborating evaluation-order polymorphism. In Proceedings of the 20th ACM SIGPLAN International Conference on Functional Programming, ICFP 2015, Vancouver, BC, Canada, September 1-3, 2015. 256-268.

Digital Library

[10]

Richard Eisenberg. 2019. GHC Proposal 29: revised levity polymorphism. https://github.com/ghc-proposals/ghc-proposals/ blob/master/proposals/0029-levity-polymorphism.rst

[11]

Richard A. Eisenberg and Simon Peyton Jones. 2017. Levity polymorphism. In Proceedings of the 38th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2017, Barcelona, Spain, June 18-23, 2017. 525-539.

[12]

Sebastian Graf. 2020. GHC Proposal 265: unlifted data types. https://github.com/ghc-proposals/ghc-proposals/blob/master/ proposals/0265-unlifted-datatypes.rst

[13]

John Hannan and Patrick Hicks. 1998. Higher-Order unCurrying. In POPL '98, Proceedings of the 25th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, San Diego, CA, USA, January 19-21, 1998. 1-11.

Digital Library

[14]

Jean-Louis Krivine. 2007. A Call-By-Name Lambda-Calculus Machine. Higher-Order and Symbolic Computation 20, 3 ( 2007 ), 199-207.

[15]

Olivier Laurent. 2002. Étude de la polarisation en logique. Ph.D. Dissertation. Université de la Méditerranée-Aix-Marseille II.

[16]

Xavier Leroy. 1990. The ZINC experiment: an economical implementation of the ML language. Technical report 117. INRIA.

[17]

Paul Blain Levy. 2001. Call-By-Push-Value. Ph.D. Dissertation. Queen Mary and Westfield College, University of London.

[18]

Simon Marlow and Simon L. Peyton Jones. 2004. Making a fast curry: push/enter vs. eval/apply for higher-order languages. In Proceedings of the Ninth ACM SIGPLAN International Conference on Functional Programming, ICFP 2004, Snow Bird, UT, USA, September 19-21, 2004. ACM, 4-15.

Digital Library

[19]

Andrew Martin. 2019a. GHC Proposal 112: unlifted arrays. https://github.com/ghc-proposals/ghc-proposals/blob/master/ proposals/0112-unlifted-array.rst

[20]

Andrew Martin. 2019b. GHC Proposal 203: pointer rep. https://github.com/ghc-proposals/ghc-proposals/blob/master/ proposals/0203-pointer-rep.rst

[21]

Andrew Martin. 2019c. GHC Proposal 98: unlifted newtypes. https://github.com/ghc-proposals/ghc-proposals/blob/master/ proposals/0098-unlifted-newtypes.rst

[22]

Dylan McDermott and Alan Mycroft. 2019. Extended Call-by-Push-Value : Reasoning About Efectful Programs and Evaluation Order. In Programming Languages and Systems, Luís Caires (Ed.). Springer International Publishing, Cham, 235-262.

[23]

Guillaume Munch-Maccagnoni. 2009. Focalisation and Classical Realisability. In Computer Science Logic: 23rd international Workshop, CSL 2009, 18th Annual Conference of the EACSL (Coimbra, Portugal) (CSL 2009), Erich Grädel and Reinhard Kahle (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg, 409-423.

[24]

Guillaume Munch-Maccagnoni. 2013. Syntax and Models of a non-Associative Composition of Programs and Proofs. Ph.D. Dissertation. Université Paris Diderot.

[25]

Simon L. Peyton Jones. 1992. Implementing Lazy Functional Languages on Stock Hardware: The Spineless Tagless G-machine. Journal of Functional Programming 2, 2 ( 1992 ), 127-202.

[26]

Simon L. Peyton Jones and John Launchbury. 1991. Unboxed Values As First Class Citizens in a Non-Strict Functional Language. In Proceedings of the 5th ACM Conference on Functional Programming Languages and Computer Architecture. Springer-Verlag, London, UK, UK, 636-666.

[27]

Amr Sabry and Matthias Felleisen. 1993. Reasoning About Programs in Continuation-Passing Style. Lisp and Symbolic Computation 6, 3-4 ( Nov. 1993 ), 289-360.

Digital Library

[28]

Amr Sabry and Philip Wadler. 1997. A Reflection on Call-by-Value. ACM Transactions on Programming Languages and Systems 19, 6 ( 1997 ), 916-941.

Digital Library

[29]

Alex Theriault. 2019. GHC Proposal 209: levity-polymorphic Lift. https://github.com/ghc-proposals/ghc-proposals/blob/ master/proposals/0209-levity-polymorphic-lift.rst

[30]

Philip Wadler, Walid Taha, and David Macqueen. 1998. How to add laziness to a strict language without even being odd. In Proceedings of the Standard ML Workshop.

[31]

Stephanie Weirich, Justin Hsu, and Richard A. Eisenberg. 2013. System FC with Explicit Kind Equality. In International Conference on Functional Programming (Boston, Massachusetts, USA) ( ICFP '13). ACM.

[32]

Noam Zeilberger. 2008. On the Unity of Duality. Annals of Pure and Applied Logic 153, 1 ( 2008 ), 660-96.

[33]

Noam Zeilberger. 2009. The Logical Basis of Evaluation Order and Pattern-Matching. Ph.D. Dissertation. Carnegie Mellon University.

Digital Library

Cited By

Wagner AEisbach ZAhmed A(2024)Realistic Realizability: Specifying ABIs You Can Count OnProceedings of the ACM on Programming Languages10.1145/36897558:OOPSLA2(1249-1278)Online publication date: 8-Oct-2024
https://dl.acm.org/doi/10.1145/3689755
Downen P(2024)Call-by-Unboxed-ValueProceedings of the ACM on Programming Languages10.1145/36746548:ICFP(845-879)Online publication date: 15-Aug-2024
https://dl.acm.org/doi/10.1145/3674654
Kovács A(2024)Closure-Free Functional Programming in a Two-Level Type TheoryProceedings of the ACM on Programming Languages10.1145/36746488:ICFP(659-692)Online publication date: 15-Aug-2024
https://dl.acm.org/doi/10.1145/3674648
Show More Cited By

Index Terms

Kinds are calling conventions
1. Software and its engineering
  1. Software notations and tools
    1. Compilers
    2. Formal language definitions
      1. Semantics

Recommendations

Type inference, principal typings, and let-polymorphism for first-class mixin modules
Proceedings of the tenth ACM SIGPLAN international conference on Functional programming

A mixin module is a programming abstraction that simultaneously generalizes λ-abstractions, records, and mutually recursive definitions. Although various mixin module type systems have been developed, no one has investigated principal typings or ...
Type inference, principal typings, and let-polymorphism for first-class mixin modules
ICFP '05: Proceedings of the tenth ACM SIGPLAN international conference on Functional programming

A mixin module is a programming abstraction that simultaneously generalizes λ-abstractions, records, and mutually recursive definitions. Although various mixin module type systems have been developed, no one has investigated principal typings or ...
Polymorphic type inference for machine code
PLDI '16

For many compiled languages, source-level types are erased very early in the compilation process. As a result, further compiler passes may convert type-safe source into type-unsafe machine code. Type-unsafe idioms in the original source and type-unsafe ...

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 4, Issue ICFP

August 2020

1070 pages

EISSN:2475-1421

DOI:10.1145/3415018

Issue’s Table of Contents

Copyright © 2020 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: 03 August 2020

Published in PACMPL Volume 4, Issue ICFP

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Research-article

Funding Sources

National Science Foundation

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

5
Total Citations
View Citations
993
Total Downloads

Downloads (Last 12 months)321
Downloads (Last 6 weeks)25

Reflects downloads up to 10 Dec 2024

Other Metrics

View Author Metrics

Citations

Cited By

Wagner AEisbach ZAhmed A(2024)Realistic Realizability: Specifying ABIs You Can Count OnProceedings of the ACM on Programming Languages10.1145/36897558:OOPSLA2(1249-1278)Online publication date: 8-Oct-2024
https://dl.acm.org/doi/10.1145/3689755
Downen P(2024)Call-by-Unboxed-ValueProceedings of the ACM on Programming Languages10.1145/36746548:ICFP(845-879)Online publication date: 15-Aug-2024
https://dl.acm.org/doi/10.1145/3674654
Kovács A(2024)Closure-Free Functional Programming in a Two-Level Type TheoryProceedings of the ACM on Programming Languages10.1145/36746488:ICFP(659-692)Online publication date: 15-Aug-2024
https://dl.acm.org/doi/10.1145/3674648
Chen YParreaux L(2024)The Long Way to Deforestation: A Type Inference and Elaboration Technique for Removing Intermediate Data StructuresProceedings of the ACM on Programming Languages10.1145/36746348:ICFP(249-283)Online publication date: 15-Aug-2024
https://dl.acm.org/doi/10.1145/3674634
Elsman M(2024)Double-Ended Bit-Stealing for Algebraic Data TypesProceedings of the ACM on Programming Languages10.1145/36746288:ICFP(88-120)Online publication date: 15-Aug-2024
https://dl.acm.org/doi/10.1145/3674628

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