research-article

Open access

Handling delimited continuations with dependent types

Authors:

Kenichi AsaiAuthors Info & Claims

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

Article No.: 69, Pages 1 - 31

https://doi.org/10.1145/3236764

Published: 30 July 2018 Publication History

Abstract

Dependent types are a powerful tool for maintaining program invariants. To take advantage of this aspect in real-world programming, efforts have been put into enriching dependently typed languages with missing constructs, most notably, effects. This paper presents a language that has two practically interesting ingredients: dependent inductive types, and the delimited control constructs shift and reset. When integrating delimited control into a dependently typed language, however, two challenges arise. First, the dynamic nature of control operators, which is the source of their expressiveness, can break fundamental language properties such as logical consistency and subject reduction. Second, CPS translations, which we often use to define the semantics of control operators, do not scale straightforwardly to dependently typed languages. We solve the former issue by restricting dependency of types, and the latter using answer-type polymorphism of pure terms. The main contribution of this paper is to give a sound type system of our language, as well as a type-preserving CPS translation. We also discuss various extensions, which would make our language more like a full-spectrum proof assistant but pose non-trivial issues.

Supplementary Material

WEBM File (a69-cong.webm)

Download
68.81 MB

References

[1]

Danel Ahman. 2017a. Fibred Computational Effects. Ph.D. Dissertation. University of Edinburgh.

[2]

Danel Ahman. 2017b. Handling Fibred Algebraic Effects. Proc. ACM Program. Lang. 2, POPL, Article 7 (Dec. 2017), 29 pages.

Digital Library

[3]

Amal Ahmed and Matthias Blume. 2011. An Equivalence-Preserving CPS Translation via Multi-Language Semantics. In Proceedings of the 16th ACM SIGPLAN International Conference on Functional Programming (ICFP ’11). 431–444.

Digital Library

[4]

Thorsten Altenkirch and Bernhard Reus. 1999. Monadic Presentations of Lambda Terms Using Generalized Inductive Types. In Proceedings of the 13th International Workshop and 8th Annual Conference of the EACSL on Computer Science Logic (CSL ’99). Springer-Verlag, London, UK, 453–468. http://dl.acm.org/citation.cfm?id=647849.737066

Digital Library

[5]

Abhishek Anand, A Appel, Greg Morrisett, Zoe Paraskevopoulou, Randy Pollack, Olivier Savary Bélanger, Matthieu Sozeau, and Matthew Weaver. 2017. CertiCoq: A verified compiler for Coq. In The Third International Workshop on Coq for Programming Languages (CoqPL).

[6]

Zena M. Ariola, Hugo Herbelin, and Amr Sabry. 2009. A Type-Theoretic Foundation of Delimited Continuations. Higher Order and Symbolic Computation 22, 3 (Sept. 2009), 233–273.

Digital Library

[7]

Kenichi Asai and Yukiyoshi Kameyama. 2007. Polymorphic Delimited Continuations. In Proceedings of the 5th Asian Conference on Programming Languages and Systems (APLAS ’07). Springer-Verlag, Berlin, Heidelberg, 239–254. http: //dl.acm.org/citation.cfm?id=1784774.1784797

Digital Library

[8]

Kenichi Asai and Oleg Kiselyov. 2011. Introduction to programming with shift and reset. In ACM SIGPLAN Continuation Workshop 2011.

[9]

Kenichi Asai and Chihiro Uehara. 2018. Selective CPS Transformation for Shift and Reset. In Proceedings of the 2018 ACM SIGPLAN Workshop on Partial Evaluation and Semantics-based Program Manipulation (PEPM ’18). 40–52.

Digital Library

[10]

Gilles Barthe, John Hatcliff, and Morten Heine B. Sørensen. 1999. CPS Translations and Applications: The Cube and Beyond. Higher-Order and Symbolic Computation 12, 2 (Sept. 1999), 125–170.

Digital Library

[11]

Gilles Barthe and Tarmo Uustalu. 2002. CPS Translating Inductive and Coinductive Types. In Proceedings of the 2002 ACM SIGPLAN Workshop on Partial Evaluation and Semantics-based Program Manipulation (PEPM ’02). ACM, New York, NY, USA, 131–142.

Digital Library

[12]

Pierre Boutillier. 2012. A relaxation of Coq’s guard condition. In JFLA - Journées Francophones des langages applicatifs - 2012. Carnac, France, 1 – 14. https://hal.archives- ouvertes.fr/hal- 00651780

[13]

William J. Bowman, Youyou Cong, Nick Rioux, and Amal Ahmed. 2017. Type-preserving CPS Translation of Σ and Π Types is Not Not Possible. Proc. ACM Program. Lang. 2, POPL, Article 22 (Dec. 2017), 33 pages.

Digital Library

[14]

Youyou Cong and Kenichi Asai. 2018. Handling Delimited Continuations with Dependent Types (Technical Appendix). (June 2018). https://github.com/YouyouCong/icfp18/

[15]

Thierry Coquand. 1989. Metamathematical investigations of a calculus of constructions. Ph.D. Dissertation. INRIA.

[16]

Thierry Coquand and Christine Paulin. 1990. Inductively Defined Types. In Proceedings of the International Conference on Computer Logic (COLOG ’88). Springer-Verlag, London, UK, 50–66. http://dl.acm.org/citation.cfm?id=646125.758641

Digital Library

[17]

Pierre-Louis Curien and Hugo Herbelin. 2000. The duality of computation. In ACM sigplan notices, Vol. 35. ACM, 233–243.

Digital Library

[18]

Olivier Danvy. 1996. Type-directed Partial Evaluation. In Proceedings of the 23rd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL ’96). ACM, New York, NY, USA, 242–257.

Digital Library

[19]

Olivier Danvy and Andrzej Filinski. 1989. A functional abstraction of typed contexts. Technical Report. University of Copenhagen.

[20]

Olivier Danvy and Andrzej Filinski. 1990. Abstracting control. In Proceedings of the 1990 ACM conference on LISP and functional programming. ACM, 151–160.

Digital Library

[21]

Olivier Danvy and Andrzej Filinski. 1992. Representing control: a study of the CPS transformation.

[22]

Edsger W. Dijkstra. 1975. Guarded Commands, Nondeterminacy and Formal Derivation of Programs. Commun. ACM 18, 8 (Aug. 1975), 453–457.

Digital Library

[23]

Andrzej Filinski. 1994. Representing Monads. In Proceedings of the 21st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL ’94). ACM, New York, NY, USA, 446–457.

Digital Library

[24]

Matthew Flatt, Gang Yu, Robert Bruce Findler, and Matthias Felleisen. 2007. Adding Delimited and Composable Control to a Production Programming Environment. In Proceedings of the 12th ACM SIGPLAN International Conference on Functional Programming (ICFP ’07). ACM, New York, NY, USA, 165–176.

Digital Library

[25]

Yannick Forster, Ohad Kammar, Sam Lindley, and Matija Pretnar. 2017. On the Expressive Power of User-defined Effects: Effect Handlers, Monadic Reflection, Delimited Control. Proc. ACM Program. Lang. 1, ICFP, Article 13 (Aug. 2017), 29 pages.

Digital Library

[26]

Eduardo Giménez. 1995. Codifying Guarded Definitions with Recursive Schemes. In Selected Papers from the International Workshop on Types for Proofs and Programs (TYPES ’94). Springer-Verlag, London, UK, 39–59. http://dl.acm.org/citation. cfm?id=646535.695850

Digital Library

[27]

Jean-Yves Girard. 1972. Interprétation fonctionnelle et élimination des coupures dans l’arithmétique. Ph.D. Dissertation. Université Paris VII.

[28]

Georges Gonthier. 2008. The four colour theorem: Engineering of a formal proof. In Computer Mathematics. Springer, 333–333.

Digital Library

[29]

Timothy G. Griffin. 1990. A Formulae-as-types Notion of Control. In Proceedings of the 17th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL ’90). ACM, New York, NY, USA, 47–58.

Digital Library

[30]

Hugo Herbelin. 2005. On the degeneracy of Σ-types in presence of computational classical logic. In International Conference on Typed Lambda Calculi and Applications (TLCA ’05). Springer, 209–220.

Digital Library

[31]

Hugo Herbelin. 2012. A constructive proof of dependent choice, compatible with classical logic. In Proceedings of the 2012 27th Annual IEEE/ACM Symposium on Logic in Computer Science (LICS ’12). IEEE Computer Society, 365–374.

Digital Library

[32]

Hugo Herbelin and Silvia Ghilezan. 2008. An Approach to Call-by-name Delimited Continuations. In Proceedings of the 35th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL ’08). ACM, New York, NY, USA, 383–394.

Digital Library

[33]

Danko Ilik. 2012. Delimited control operators prove double-negation shift. Annals of Pure and Applied logic 163, 11 (2012), 1549–1559.

[34]

Limin Jia, Jianzhou Zhao, Vilhelm Sjöberg, and Stephanie Weirich. 2010. Dependent Types and Program Equivalence. In Proceedings of the 37th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL ’10). ACM, New York, NY, USA, 275–286.

Digital Library

[35]

Yukiyoshi Kameyama, Oleg Kiselyov, and Chung-chieh Shan. 2009. Shifting the Stage: Staging with Delimited Control. In Proceedings of the 2009 ACM SIGPLAN Workshop on Partial Evaluation and Program Manipulation (PEPM ’09). ACM, New York, NY, USA, 111–120.

Digital Library

[36]

Oleg Kiselyov, Chung-chieh Shan, and Amr Sabry. 2006. Delimited dynamic binding. In The 33th ACM SIGPLAN-SIGACT symposium on Principles of programming languages (POPL ’06). ACM, 26–37.

Digital Library

[37]

Oleg Kiselyov and KC Sivaramakrishnan. 2016. Eff directly in OCaml. In ML Workshop.

[38]

Shriram Krishnamurthi, Peter Walton Hopkins, Jay McCarthy, Paul T. Graunke, Greg Pettyjohn, and Matthias Felleisen. 2007. Implementation and Use of the PLT Scheme Web Server. Higher Order Symbolic Computation 20, 4 (Dec. 2007), 431–460.

Digital Library

[39]

Rodolphe Lepigre. 2016. A classical realizability model for a semantical value restriction. In European Symposium on Programming Languages and Systems (ESOP ’16). Springer, 476–502.

Digital Library

[40]

Xavier Leroy. 2006. Formal certification of a compiler back-end, or: programming a compiler with a proof assistant. In 33rd ACM Symposium on Principles of Programming Languages (POPL ’06). 42–54.

Digital Library

[41]

Paul Blain Levy. 2012. Call-by-push-value: A Functional/imperative Synthesis. Vol. 2. Springer Science & Business Media.

[42]

Marek Materzok and Dariusz Biernacki. 2011. Subtyping Delimited Continuations. In Proceedings of the 16th ACM SIGPLAN International Conference on Functional Programming (ICFP ’11). ACM, New York, NY, USA, 81–93.

Digital Library

[43]

Ulf Norell. 2007. Towards a practical programming language based on dependent type theory. Ph.D. Dissertation. Chalmers University of Technology.

[44]

Michel Parigot. 1992. Lambda-My-Calculus: An Algorithmic Interpretation of Classical Natural Deduction. In Proceedings of the International Conference on Logic Programming and Automated Reasoning (LPAR ’92). Springer-Verlag, London, UK, 190–201. http://dl.acm.org/citation.cfm?id=645706.663989

Digital Library

[45]

Frank Pfenning and Christine Paulin-Mohring. 1990. Inductively Defined Types in the Calculus of Constructions. In Proceedings of the 5th International Conference on Mathematical Foundations of Programming Semantics. Springer-Verlag, London, UK, 209–228. http://dl.acm.org/citation.cfm?id=645736.666272

Digital Library

[46]

Chung-Chieh Shan. 2003. From shift and reset to polarized linear logic. (2003). Unpublished.

[47]

Chung-chieh Shan. 2007. A static simulation of dynamic delimited control. Higher-Order and Symbolic Computation 20, 4 (2007), 371–401.

Digital Library

[48]

Matthieu Sozeau. 2008. Un environnement pour la programmation avec types dépendants. Ph.D. Dissertation. Université de Paris-Sud. Faculté des Sciences d’Orsay (Essonne).

[49]

Nikhil Swamy, Juan Chen, Cédric Fournet, Pierre-Yves Strub, Karthikeyan Bhargavan, and Jean Yang. 2011. Secure Distributed Programming with Value-dependent Types. In Proceedings of the 16th ACM SIGPLAN International Conference on Functional Programming (ICFP ’11). ACM, New York, NY, USA, 266–278.

Digital Library

[50]

Nikhil Swamy, Cătălin Hriţcu, Chantal Keller, Aseem Rastogi, Antoine Delignat-Lavaud, Simon Forest, Karthikeyan Bhargavan, Cédric Fournet, Pierre-Yves Strub, Markulf Kohlweiss, Jean-Karim Zinzindohoue, and Santiago ZanellaBéguelin. 2016. Dependent Types and Multi-monadic Effects in F*. In Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL ’16). ACM, New York, NY, USA, 256–270.

Digital Library

[51]

Asami Tanaka and Yukiyoshi Kameyama. 2012. A Call-by-Name CPS Hierarchy. In Functional and Logic Programming, Tom Schrijvers and Peter Thiemann (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg, 260–274.

Digital Library

[52]

The Coq Development Team. 2018. The Coq Proof Assistant Reference Manual. https://coq.inria.fr/refman/

[53]

Hayo Thielecke. 2003. From Control Effects to Typed Continuation Passing. In Proceedings of the 30th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages" (POPL ’03).

Digital Library

[54]

Matthijs Vákár. 2017. In Search of Effectful Dependent Types. Ph.D. Dissertation. Oxford University.

[55]

Philip Wadler. 1989. Theorems for Free!. In Proceedings of the Fourth International Conference on Functional Programming Languages and Computer Architecture (FPCA ’89). ACM, ACM, New York, NY, USA, 347–359.

Digital Library

[56]

Benjamin Werner. 1994. Une Théorie des Constructions Inductives. Ph.D. Dissertation. Université Paris-Diderot - Paris VII. https://tel.archives- ouvertes.fr/tel- 00196524

[57]

Andrew K Wright and Matthias Felleisen. 1994. A syntactic approach to type soundness. Information and computation 115, 1 (1994), 38–94.

Digital Library

[58]

Noam Zeilberger. 2010. Polarity and the logic of delimited continuations. In Logic in Computer Science (LICS), 2010 25th Annual IEEE Symposium on. IEEE, 219–227.

Digital Library

Cited By

Kawamata FUnno HSekiyama TTerauchi T(2024)Answer Refinement Modification: Refinement Type System for Algebraic Effects and HandlersProceedings of the ACM on Programming Languages10.1145/36332808:POPL(115-147)Online publication date: 5-Jan-2024
https://dl.acm.org/doi/10.1145/3633280
Sekiyama TUnno H(2023)Temporal Verification with Answer-Effect Modification: Dependent Temporal Type-and-Effect System with Delimited ContinuationsProceedings of the ACM on Programming Languages10.1145/35712647:POPL(2079-2110)Online publication date: 9-Jan-2023
https://dl.acm.org/doi/10.1145/3571264
Sekiyama TTsukada TIgarashi A(2020)Signature restriction for polymorphic algebraic effectsProceedings of the ACM on Programming Languages10.1145/34089994:ICFP(1-30)Online publication date: 3-Aug-2020
https://dl.acm.org/doi/10.1145/3408999

Index Terms

Handling delimited continuations with dependent types
1. Software and its engineering
  1. Software notations and tools
    1. General programming languages
      1. Language features
        Control structures
        Polymorphism
      2. Language types
        Functional languages
2. Theory of computation
  1. Logic
    1. Type theory
  2. Semantics and reasoning
    1. Program constructs
      1. Control primitives

Recommendations

Polymorphic delimited continuations
APLAS'07: Proceedings of the 5th Asian conference on Programming languages and systems

This paper presents a polymorphic type system for a language with delimited control operators, shift and reset. Based on the monomorphic type system by Danvy and Filinski, the proposed type system allows pure expressions to be polymorphic. Thanks to the ...
On typing delimited continuations: three new solutions to the printf problem

In "Functional Unparsing" (J. Funct. Program. 8(6):621---625, 1998), Danvy presented a type-safe printf function using continuations and an accumulator to achieve the effect of dependent types. The key technique employed in Danvy's solution is the non-...
Cayenne—a language with dependent types

Cayenne is a Haskell-like language. The main difference between Haskell and Cayenne is that Cayenne has dependent types, i.e., the result type of a function may depend on the argument value, and types of record components (which can be types or values) ...

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

September 2018

1133 pages

EISSN:2475-1421

DOI:10.1145/3243631

Issue’s Table of Contents

Copyright © 2018 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: 30 July 2018

Published in PACMPL Volume 2, Issue ICFP

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Research-article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

3
Total Citations
View Citations
1,592
Total Downloads

Downloads (Last 12 months)184
Downloads (Last 6 weeks)27

Reflects downloads up to 10 Nov 2024

Other Metrics

View Author Metrics

Citations

Cited By

Kawamata FUnno HSekiyama TTerauchi T(2024)Answer Refinement Modification: Refinement Type System for Algebraic Effects and HandlersProceedings of the ACM on Programming Languages10.1145/36332808:POPL(115-147)Online publication date: 5-Jan-2024
https://dl.acm.org/doi/10.1145/3633280
Sekiyama TUnno H(2023)Temporal Verification with Answer-Effect Modification: Dependent Temporal Type-and-Effect System with Delimited ContinuationsProceedings of the ACM on Programming Languages10.1145/35712647:POPL(2079-2110)Online publication date: 9-Jan-2023
https://dl.acm.org/doi/10.1145/3571264
Sekiyama TTsukada TIgarashi A(2020)Signature restriction for polymorphic algebraic effectsProceedings of the ACM on Programming Languages10.1145/34089994:ICFP(1-30)Online publication date: 3-Aug-2020
https://dl.acm.org/doi/10.1145/3408999

View Options

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Get Access

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