Article

Polymorphic delimited continuations

Authors:

Yukiyoshi KameyamaAuthors Info & Claims

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

Pages 239 - 254

Published: 29 November 2007 Publication History

Abstract

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 explicit presence of answer types, our type system satisfies various important properties, including strong type soundness, existence of principal types and an inference algorithm, and strong normalization. Relationship to CPS translation as well as extensions to impredicative polymorphism are also discussed. These technical results establish the foundation of polymorphic delimited continuations.

References

[1]

Asai, K.: Logical Relations for Call-by-value Delimited Continuations. Trends in Functional Programming 6, 63-78 (2007).

[2]

Asai, K.: On Typing Delimited Continuations: Three New Solutions to the Printf Problem. See http://pllab.is.ocha.ac.jp/~asai/papers/ (submitted, 2007).

Digital Library

[3]

Asai, K., Kameyama, Y.: Polymorphic Delimited Continuations. Technical Report CS-TR-07-10, Dept. of Computer Science, University of Tsukuba (September 2007).

[4]

Danvy, O.: An Analytical Approach to Program as Data Objects. DSc thesis, Department of Computer Science, University of Aarhus, Aarhus, Denmark (2006).

[5]

Danvy, O., Filinski, A.: A Functional Abstraction of Typed Contexts. Technical Report 89/12, DIKU, University of Copenhagen (July 1989).

[6]

Danvy, O., Filinski, A.: Abstracting Control. In: Proc. 1990 ACM Conference on Lisp and Functional Programming, pp. 151-160 (1990).

Digital Library

[7]

Danvy, O., Filinski, A.: Representing Control: a Study of the CPS Transformation. Mathematical Structures in Computer Science 2(4), 361-391 (1992).

[8]

Filinski, A.: Representing Monads. In: POPL, pp. 446-457 (1994).

Digital Library

[9]

Girard, J.-Y., Lafont, Y., Taylor, P.: Proofs and Types. Cambridge Tracts in Theoretical Computer Science, vol. 7. Cambridge University Press, Cambridge (1989).

Digital Library

[10]

Gunter, C.A., Remy, D., Riecke, J.G.: A Generalization of Exceptions and Control in ML-Like Languages. In: FPCA, pp. 12-23 (1995).

Digital Library

[11]

Harper, R., Duba, B.F., MacQueen, D.: Typing First-Class Continuations in ML. J. Funct. Program. 3(4), 465-484 (1993).

[12]

Harper, R., Lillibridge, M.: Explicit polymorphism and CPS conversion. In: POPL, pp. 206-219 (1993).

Digital Library

[13]

Hasegawa, M.: Relational parametricity and control. Logical Methods in Computer Science 2(3) (2006).

[14]

Kiselyov, O., Shan, C.-c., Sabry, A.: Delimited dynamic binding. In: ICFP, pp. 26-37 (2006).

Digital Library

[15]

Leroy, X.: Polymorphism by name for references and continuations. In: POPL, pp. 220-231 (1993).

Digital Library

[16]

Mogelberg, R.E., Simpson, A.: Relational parametricity for computational effects. In: LICS (2007).

Digital Library

[17]

Strachey, C.: Fundamental concepts in programming languages. International Summer School in Computer Programming, Copenhagen, Denmark (August 1967).

[18]

Thielecke, H.: From Control Effects to Typed Continuation Passing. In: POPL, pp. 139-149. ACM Press, New York (2003).

Digital Library

[19]

Tofte, M.: Type inference for polymorphic references. Inf. Comput. 89(1), 1-34 (1990).

Digital Library

[20]

Wright, A.K.: Simple imperative polymorphism. Lisp and Symbolic Computation 8(4), 343-355 (1995).

Digital Library

[21]

Wright, A.K., Felleisen, M.: A syntactic approach to type soundness. Inf. Comput. 115(1), 38-94 (1994).

Digital Library

Cited By

Cong YAsai K(2018)Handling delimited continuations with dependent typesProceedings of the ACM on Programming Languages10.1145/32367642:ICFP(1-31)Online publication date: 30-Jul-2018
https://dl.acm.org/doi/10.1145/3236764
Asai KUehara CHenglein FKo H(2017)Selective CPS transformation for shift and resetProceedings of the ACM SIGPLAN Workshop on Partial Evaluation and Program Manipulation10.1145/3162069(40-52)Online publication date: 25-Dec-2017
https://dl.acm.org/doi/10.1145/3162069
Leijen DLindley SYorgey B(2017)Structured asynchrony with algebraic effectsProceedings of the 2nd ACM SIGPLAN International Workshop on Type-Driven Development10.1145/3122975.3122977(16-29)Online publication date: 3-Sep-2017
https://dl.acm.org/doi/10.1145/3122975.3122977
Show More Cited By

Recommendations

Type System for Four Delimited Control Operators
GPCE 2022: Proceedings of the 21st ACM SIGPLAN International Conference on Generative Programming: Concepts and Experiences

The operational behavior of control operators has been studied comprehensively in the past few decades, but type systems of control operators have not. There are distinct type systems for shift, control, and shift0 without any relationship between them, ...
Handling delimited continuations with dependent types

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 ...
Subtyping delimited continuations
ICFP '11: Proceedings of the 16th ACM SIGPLAN international conference on Functional programming

We present a type system with subtyping for first-class delimited continuations that generalizes Danvy and Filinski's type system for shift and reset by maintaining explicit information about the types of contexts in the metacontext. We exploit this ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image Guide Proceedings

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

November 2007

431 pages

ISBN:3540766367

Editor:
Zhong Shao
Yale University, Department of Computer Science, New Haven, CT

Sponsors

AAFS: Asian Association for Foundation of Software
Natl University of Singapore: National University of Singapore

Publisher

Springer-Verlag

Berlin, Heidelberg

Publication History

Published: 29 November 2007

Author Tags

Qualifiers

Article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

27
Total Citations
View Citations
2
Total Downloads

Downloads (Last 12 months)0
Downloads (Last 6 weeks)0

Reflects downloads up to 20 Nov 2024

Other Metrics

View Author Metrics

Citations

Cited By

Cong YAsai K(2018)Handling delimited continuations with dependent typesProceedings of the ACM on Programming Languages10.1145/32367642:ICFP(1-31)Online publication date: 30-Jul-2018
https://dl.acm.org/doi/10.1145/3236764
Asai KUehara CHenglein FKo H(2017)Selective CPS transformation for shift and resetProceedings of the ACM SIGPLAN Workshop on Partial Evaluation and Program Manipulation10.1145/3162069(40-52)Online publication date: 25-Dec-2017
https://dl.acm.org/doi/10.1145/3162069
Leijen DLindley SYorgey B(2017)Structured asynchrony with algebraic effectsProceedings of the 2nd ACM SIGPLAN International Workshop on Type-Driven Development10.1145/3122975.3122977(16-29)Online publication date: 3-Sep-2017
https://dl.acm.org/doi/10.1145/3122975.3122977
Leijen D(2017)Type directed compilation of row-typed algebraic effectsACM SIGPLAN Notices10.1145/3093333.300987252:1(486-499)Online publication date: 1-Jan-2017
https://dl.acm.org/doi/10.1145/3093333.3009872
Leijen DCastagna GGordon A(2017)Type directed compilation of row-typed algebraic effectsProceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages10.1145/3009837.3009872(486-499)Online publication date: 1-Jan-2017
https://dl.acm.org/doi/10.1145/3009837.3009872
Biernacki DDanvy OMillikin K(2015)A Dynamic Continuation-Passing Style for Dynamic Delimited ContinuationsACM Transactions on Programming Languages and Systems10.1145/279407838:1(1-25)Online publication date: 16-Oct-2015
https://dl.acm.org/doi/10.1145/2794078
Takikawa AStrickland TTobin-Hochstadt S(2013)Constraining delimited control with contractsProceedings of the 22nd European conference on Programming Languages and Systems10.1007/978-3-642-37036-6_14(229-248)Online publication date: 16-Mar-2013
https://dl.acm.org/doi/10.1007/978-3-642-37036-6_14
Biernacki DLenglet S(2013)Environmental Bisimulations for Delimited-Control OperatorsProceedings of the 11th Asian Symposium on Programming Languages and Systems - Volume 830110.1007/978-3-319-03542-0_24(333-348)Online publication date: 9-Dec-2013
https://dl.acm.org/doi/10.1007/978-3-319-03542-0_24
Tanaka AKameyama Y(2012)A call-by-name CPS hierarchyProceedings of the 11th international conference on Functional and Logic Programming10.1007/978-3-642-29822-6_21(260-274)Online publication date: 23-May-2012
https://dl.acm.org/doi/10.1007/978-3-642-29822-6_21
Tov JPucella R(2011)A theory of substructural types and controlACM SIGPLAN Notices10.1145/2076021.204811546:10(625-642)Online publication date: 22-Oct-2011
https://dl.acm.org/doi/10.1145/2076021.2048115
Show More Cited By

View Options

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

Media

Figures

Other

Tables

View Table of Contents