Document Open Access Logo

Beyond Polarity: Towards a Multi-Discipline Intermediate Language with Sharing

Authors Paul Downen, Zena M. Ariola

PDF
Thumbnail PDF

File

LIPIcs.CSL.2018.21.pdf
  • Filesize: 0.59 MB
  • 23 pages

Document Identifiers

Author Details

Paul Downen
  • University of Oregon, Eugene, OR, USA
Zena M. Ariola
  • University of Oregon, Eugene, OR, USA

Funding

This work is supported by the National Science Foundation under grants CCF-1719158 and CCF-1423617.

Cite As Get BibTex

Paul Downen and Zena M. Ariola. Beyond Polarity: Towards a Multi-Discipline Intermediate Language with Sharing. In 27th EACSL Annual Conference on Computer Science Logic (CSL 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 119, pp. 21:1-21:23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018) https://doi.org/10.4230/LIPIcs.CSL.2018.21

Abstract

The study of polarity in computation has revealed that an "ideal" programming language combines both call-by-value and call-by-name evaluation; the two calling conventions are each ideal for half the types in a programming language. But this binary choice leaves out call-by-need which is used in practice to implement lazy-by-default languages like Haskell. We show how the notion of polarity can be extended beyond the value/name dichotomy to include call-by-need by only adding a mechanism for sharing and the extra polarity shifts to connect them, which is enough to compile a Haskell-like functional language with user-defined types.

Subject Classification

ACM Subject Classification
  • Theory of computation → Type structures
Keywords
  • call-by-need
  • polarity
  • call-by-push-value
  • control

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

References

  1. Jean-Marc Andreoli. Logic programming with focusing proofs in linear logic. Journal of Logic and Computation, 2(3):297-347, 1992. URL: http://dx.doi.org/10.1093/logcom/2.3.297.
  2. Andrew W. Appel. Compiling with Continuations. Cambridge University Press, New York, NY, USA, 1992. Google Scholar
  3. Zena M. Ariola, Hugo Herbelin, and Alexis Saurin. Classical call-by-need and duality. In Typed Lambda Calculi and Applications: 10th International Conference, TLCA'11, pages 27-44, Berlin, Heidelberg, jun 2011. Springer Berlin Heidelberg. URL: http://dx.doi.org/10.1007/978-3-642-21691-6_6.
  4. Zena M. Ariola, John Maraist, Martin Odersky, Matthias Felleisen, and Philip Wadler. A call-by-need lambda calculus. In Proceedings of the 22nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL '95, pages 233-246, New York, NY, USA, 1995. ACM. URL: http://dx.doi.org/10.1145/199448.199507.
  5. Pierre-Louis Curien and Hugo Herbelin. The duality of computation. In Proceedings of the Fifth ACM SIGPLAN International Conference on Functional Programming, ICFP '00, pages 233-243, New York, NY, USA, 2000. ACM. URL: http://dx.doi.org/10.1145/351240.351262.
  6. Paul Downen. Sequent Calculus: A Logic and a Language for Computation and Duality. PhD thesis, University of Oregon, 2017. Google Scholar
  7. Paul Downen and Zena M. Ariola. The duality of construction. In Zhong Shao, editor, Programming Languages and Systems: 23rd European Symposium on Programming, ESOP 2014, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2014, volume 8410 of Lecture Notes in Computer Science, pages 249-269. Springer Berlin Heidelberg, Berlin, Heidelberg, apr 2014. URL: http://dx.doi.org/10.1007/978-3-642-54833-8_14.
  8. Paul Downen and Zena M. Ariola. A tutorial on computational classical logic and the sequent calculus. Journal of Functional Programming, 28:e3, 2018. URL: http://dx.doi.org/10.1017/S0956796818000023.
  9. Tatsuya Hagino. A typed lambda calculus with categorical type constructors. In David H. Pitt, Axel Poigné, and David E. Rydeheard, editors, Category Theory and Computer Science, pages 140-157, Berlin, Heidelberg, sep 1987. Springer Berlin Heidelberg. URL: http://dx.doi.org/10.1007/3-540-18508-9_24.
  10. Paul Blain Levy. Call-By-Push-Value. PhD thesis, Queen Mary and Westfield College, University of London, 2001. Google Scholar
  11. Paul Blain Levy. Jumbo λ-Calculus, pages 444-455. Springer Berlin Heidelberg, Berlin, Heidelberg, jul 2006. URL: http://dx.doi.org/10.1007/11787006_38.
  12. Luke Maurer, Paul Downen, Zena M. Ariola, and Simon Peyton Jones. Compiling without continuations. In Proceedings of the 38th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI '17, pages 482-494, New York, NY, USA, jun 2017. ACM. URL: http://dx.doi.org/10.1145/3062341.3062380.
  13. Eugenio Moggi. Computational lambda-calculus and monads. In Proceedings of the Fourth Annual Symposium on Logic in Computer Science, pages 14-23, Piscataway, NJ, USA, 1989. IEEE Press. URL: http://dl.acm.org/citation.cfm?id=77350.77353.
  14. Guillaume Munch-Maccagnoni. Syntax and Models of a non-Associative Composition of Programs and Proofs. PhD thesis, Université Paris Diderot, 2013. Google Scholar
  15. Guillaume Munch-Maccagnoni and Gabriel Scherer. Polarised intermediate representation of lambda calculus with sums. In 30th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2015, pages 127-140. IEEE, jul 2015. URL: http://dx.doi.org/10.1109/LICS.2015.22.
  16. Michel Parigot. λμ-calculus: An algorithmic interpretation of classical natural deduction. In Andrei Voronkov, editor, Logic Programming and Automated Reasoning: International Conference, LPAR '92, pages 190-201, Berlin, Heidelberg, 1992. Springer Berlin Heidelberg. URL: http://dx.doi.org/10.1007/BFb0013061.
  17. Simon Peyton Jones and Erik Meijer. Henk: a typed intermediate language. In Proceedings of the First International Workshop on Types in Compilation, 1997. Google Scholar
  18. Simon L. Peyton Jones and John Launchbury. Unboxed values as first class citizens in a non-strict functional language. In John Hughes, editor, Functional Programming Languages and Computer Architecture: 5th ACM Conference, pages 636-666, Berlin, Heidelberg, aug 1991. Springer Berlin Heidelberg. URL: http://dx.doi.org/10.1007/3540543961_30.
  19. Gordon D. Plotkin. Call-by-name, call-by-value and the λ-calculus. Theoretical Computer Science, 1:125-159, 1975. URL: http://dx.doi.org/10.1016/0304-3975(75)90017-1.
  20. Amr Sabry and Matthias Felleisen. Reasoning about programs in continuation-passing style. Lisp and Symbolic Computation, 6(3-4):289-360, nov 1993. URL: http://dx.doi.org/10.1007/BF01019462.
  21. Philip Wadler. Call-by-value is dual to call-by-name. In Proceedings of the Eighth ACM SIGPLAN International Conference on Functional Programming, pages 189-201, New York, NY, USA, 2003. ACM. URL: http://dx.doi.org/10.1145/944705.944723.
  22. Noam Zeilberger. On the unity of duality. Annals of Pure and Applied Logic, 153(1):660-96, 2008. URL: http://dx.doi.org/10.1016/j.apal.2008.01.001.
  23. Noam Zeilberger. The Logical Basis of Evaluation Order and Pattern-Matching. PhD thesis, Carnegie Mellon University, 2009. Google Scholar
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact