Abstract
Multi-stage programming (MSP) is a means for run-time code generation, and has been found promising in various fields including numerical computation and domain specific languages. An important problem in designing MSP languages is the dilemma of safety and expressivity; many foundational calculi have been proposed and proven to be type safe, yet, they are not expressive enough. Taha’s MetaOCaml provides us a very expressive tool for MSP, yet, the corresponding theory covers its purely functional subset only.
In this paper, we propose a polymorphic multi-stage calculus with delimited-control operators. Kameyama, Kiselyov, and Shan proposed a multi-stage calculus with computation effects, but their calculus lacks polymorphism. In the presence of control effects, polymorphism in types is indispensable as all pure functions are polymorphic over answer types, and in MSP languages, polymorphism in stages is indispensable to write custom generators as library functions. We show that the proposed calculus satisfies type soundness and type inference. The former is the key to guarantee the absence of scope extrusion - open codes are never generated or executed. The latter is important in the ML-like programming languages. Following Calcagno, Moggi and Taha’s work, we propose a Hindley-Milner style type inference algorithm to obtain principal types for given expressions (if they exist).
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
Asai, K., Kameyama, Y.: Polymorphic Delimited Continuations. In: Shao, Z. (ed.) APLAS 2007. LNCS, vol. 4807, pp. 239–254. Springer, Heidelberg (2007)
Calcagno, C., Moggi, E., Taha, W.: Ml-Like Inference for Classifiers. In: Schmidt, D. (ed.) ESOP 2004. LNCS, vol. 2986, pp. 79–93. Springer, Heidelberg (2004)
Danvy, O., Filinski, A.: Abstracting control. In: LISP and Functional Programming, pp. 151–160 (1990)
Davies, R.: A temporal logic approach to binding-time analysis. In: LICS, pp. 184–195 (1996)
Davies, R., Pfenning, F.: A modal analysis of staged computation. Journal of the ACM 48(3), 555–604 (2001)
Filinski, A.: Representing Monads. In: Proc. 21st Symposium on Principles of Programming Languages, pp. 446–457 (1994)
Kameyama, Y., Kiselyov, O., Shan, C.-c.: Shifting the stage: staging with delimited control. In: PEPM, pp. 111–120 (2009)
Kim, I.-S., Yi, K., Calcagno, C.: A polymorphic modal type system for lisp-like multi-staged languages. In: POPL, pp. 257–268 (2006)
Kiselyov, O., Shan, C.-c., Sabry, A.: Delimited dynamic binding. In: Reppy, J.H., Lawall, J.L. (eds.) ICFP, pp. 26–37. ACM (2006)
Sugiura, K., Kameyama, Y.: Multi-stage language with control effect and code execution. Computer Software Journal of Japan Society of Software Science and Technology 28(1), 217–229 (2011) (in Japanese)
Taha, W.: A gentle introduction to multi-stage programming. In: Domain-Specific Program Generation, pp. 30–50 (2003)
Taha, W.: A Gentle Introduction to Multi-stage Programming, Part II. In: GTTSE, pp. 260–290 (2007)
Taha, W., Nielsen, M.F.: Environment classifiers. In: POPL, pp. 26–37 (2003)
Thielecke, H.: From control effects to typed continuation passing. In: POPL, pp. 139–149. ACM Press (2003)
Tsukada, T., Igarashi, A.: A logical foundation for environment classifiers. Logical Methods in Computer Science 6(4/9), 1–43 (2010)
Westbrook, E., Ricken, M., Inoue, J., Yao, Y., Abdelatif, T., Taha, W.: Mint: Java multi-stage programming using weak separability. In: PLDI, pp. 400–411 (2010)
Yuse, Y., Igarashi, A.: A modal type system for multi-level generating extensions with persistent code. In: PPDP, pp. 201–212 (2006)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2011 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Kokaji, Y., Kameyama, Y. (2011). Polymorphic Multi-stage Language with Control Effects. In: Yang, H. (eds) Programming Languages and Systems. APLAS 2011. Lecture Notes in Computer Science, vol 7078. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-25318-8_11
Download citation
DOI: https://doi.org/10.1007/978-3-642-25318-8_11
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-25317-1
Online ISBN: 978-3-642-25318-8
eBook Packages: Computer ScienceComputer Science (R0)