article

Closed types for a safe imperative MetaML

Authors:

T. SheardAuthors Info & Claims

Journal of Functional Programming, Volume 13, Issue 3

Pages 545 - 571

https://doi.org/10.1017/S0956796802004598

Published: 01 May 2003 Publication History

Abstract

This paper addresses the issue of safely combining computational effects and multi-stage programming. We propose a type system which exploits a notion of closed type, to check statically that an imperative multi-stage program does not cause run-time errors. Our approach is demonstrated formally for a core language called $\hbox{\sf MiniML}^{\sf meta}_{\sf ref}$. This core language safely combines multi-stage constructs and ML-style references, and is a conservative extension of $\hbox{\sf MiniML}_{\sf ref}$, a simple imperative subset of SML. In previous work, we introduced a closed type constructor, which was enough to ensure the safe execution of dynamically generated code in the pure fragment of $\hbox{\sf MiniML}^{\sf meta}_{\sf ref}$.

References

[1]

Benaissa, Z. El-A., Moggi, E., Taha, W. and Sheard, T. (1999) Logical modalities and multi-stage programming. Federated Logic Conference (FLoC) Satellite Workshop on Intuitionistic Modal Logics and Applications (IMLA).

[2]

Calcagno, C. and Moggi, E. (2000) Multi-stage imperative languages: A conservative extension result. In: Taha, W., editor, Semantics, Applications, and Implementation of Program Generation: Lecture Notes in Computer Science 1924, pp. 92-107. Springer-Verlag.

[3]

Calcagno, C., Moggi, E. and Taha, W. (2000) Closed types as a simple approach to safe imperative multi-stage programming. International Colloquium on Automata, Languages, and Programming (ICALP '00): Lecture Notes in Computer Science 1853, pp. 25-36. Springer-Verlag.

[4]

Cardelli, L. (1997) Type systems. In: Tucker, A. B. Jr., editor, The Computer Science and Engineering Handbook. CRC Press.

[5]

Clement, D., Despeyroux, J., Despeyroux, T. and Kahn, G. (1986) A simple applicative language: Mini-ML. Proceedings ACM Conference on Lisp and Functional Programming, pp. 13-27. ACM press.

Digital Library

[6]

Davies, R. (1996) A temporal-logic approach to binding-time analysis. Symposium on Logic in Computer Science (LICS '96), pp. 184-195. IEEE Press.

Digital Library

[7]

Davies, R. and Pfenning, F. (1996) A modal analysis of staged computation. Symposium on Principles of Programming Languages (POPL '96), pp. 258-270.

Digital Library

[8]

Glück, R. and Jørgensen, J. (1996) Fast binding-time analysis for multi-level specialization. In: Bjørner, D., Broy, M. and Pottosin, I., editors, Perspectives of System Informatics: Lecture Notes in Computer Science 1181, pp. 261-272. Springer-Verlag.

Digital Library

[9]

Gomard, C. K. and Jones, N. D. (1991) A partial evaluator for untyped lambda calculus. J. Functional Program. 1(1), 21-69.

[10]

Harper, R. and Stone, C. (1997) A type-theoretic account of Standard ML 1996 (version 2). Technical report CMU-CS-97-147, Carnegie Mellon University, Pittsburgh, PA.

[11]

Hatcliff, J. and Danvy, O. (1997) A computational formalization for partial evaluation. Math. Struct. Comput. Sci. 7(5), 507-541.

Digital Library

[12]

Jones, N. D., Gomard, C. K. and Sestoft, P. (1993) Partial Evaluation and Automatic Program Generation. Prentice-Hall.

Digital Library

[13]

Kamin, S., Callahan, M. and Clausen, L. (2000) Lightweight and generative components II: Binary-level components. In: Taha, W., editor, Semantics, Applications, and Implementation of Program Generation: Lecture Notes in Computer Science 1924, pp. 28-50. Springer-Verlag.

[14]

MHP (2000) The MetaML Home Page. Provides source code and documentation online at http://www.cse.ogi.edu/PacSoft/projects/metaml/index.html.

[15]

Milner, R. (1978) A theory of type polymorphism in programming. J. Comput. & Syst. Sci. 17, 348-375.

[16]

Milner, R., Tofte, M., Harper, R. and MacQueen, D. (1997) The Definition of Standard ML (revised). MIT Press.

Digital Library

[17]

Moggi, E. (1998) Functor categories and two-level languages. Foundations of Software Science and Computation Structures (FoSSaCS): Lecture Notes in Computer Science 1378. Springer-Verlag.

Digital Library

[18]

Moggi, E., Taha, W., Benaissa, Z. El-A. and Sheard, T. (1999) An idealized MetaML: Simpler, and more expressive. European Symposium on Programming (ESOP): Lecture Notes in Computer Science 1576, pp. 193-207. Springer-Verlag.

[19]

Smith, B. C. (1982) Reflection and semantics in a procedural language. PhD thesis, Massachusetts Institute of Technology.

[20]

Taha, W. (1999) Multi-stage programming: Its theory and applications. PhD thesis, Oregon Graduate Institute of Science and Technology. (Available from ftp://cse. ogi.edu/pub/tech-reports/README.html.)

Digital Library

[21]

Taha, W. (ed) (2000a) Semantics, Applications, and Implementation of Program Generation: Lecture Notes in Computer Science 1924. Springer-Verlag.

[22]

Taha, Wa. (2000b) A sound reduction semantics for untyped CBN multi-stage computation. Or, the theory of MetaML is non-trivial. Proceedings Workshop on Partial Evaluation and Semantics-based Program Manipulation (PEPM). ACM Press.

Digital Library

[23]

Taha, W. and Sheard, T. (1997) Multi-stage programming with explicit annotations. Proceedings Symposium on Partial Evaluation and Semantic-based Program Manipulation (PEPM), pp. 203-217. ACM Press.

Digital Library

[24]

Taha, W. and Sheard, T. (2000) MetaML: Multi-stage programming with explicit annotations. Theor. Comput. Sci. 248(1-2).

Digital Library

[25]

Taha, W., Benaissa, Z.-El-A. and Sheard, T. (1998) Multi-stage programming: Axiomatization and type-safety. 25th International Colloquium on Automata, Languages, and Programming (ICALP): Lecture Notes in Computer Science 1443, pp. 918-929. Springer-Verlag.

Digital Library

[26]

Thiemann, P. and Dussart, D. (1999) Partial evaluation for higher-order languages with state. (Available from http://www.informatik.uni-freiburg.de/~thiemann/papers/index.html.)

[27]

Wickline, P., Lee, P. and Pfenning, F. (1998) Run-time code generation and Modal-ML. Proceedings Conference on Programming Language Design and Implementation (PLDI), pp. 224-235.

Digital Library

[28]

Wright, A. K. and Felleisen, M. (1994) A syntactic approach to type soundness. Infor. & Computation, 115(1), 38-94.

Digital Library

[29]

Xi, H. (1999) Dead code elimination through dependent types. First International Workshop on Practical Aspects of Declarative Languages: Lecture Notes in Computer Science 1551.

Cited By

Suwa TIgarashi A(2024)An ML-Style Module System for Cross-Stage Type Abstraction in Multi-stage ProgrammingFunctional and Logic Programming10.1007/978-981-97-2300-3_13(237-272)Online publication date: 15-May-2024
https://dl.acm.org/doi/10.1007/978-981-97-2300-3_13
Xie NWhite LNicole OYallop J(2023)MacoCaml: Staging Composable and Compilable MacrosProceedings of the ACM on Programming Languages10.1145/36078517:ICFP(604-648)Online publication date: 31-Aug-2023
https://dl.acm.org/doi/10.1145/3607851
Caires LToninho B(2019)Refinement kinds: type-safe programming with practical type-level computationProceedings of the ACM on Programming Languages10.1145/33605573:OOPSLA(1-30)Online publication date: 10-Oct-2019
https://dl.acm.org/doi/10.1145/3360557
Show More Cited By

Index Terms

Closed types for a safe imperative MetaML
1. Theory of computation
  1. Semantics and reasoning
    1. Program semantics

Recommendations

Closed Types as a Simple Approach to Safe Imperative Multi-stage Programming
ICALP '00: Proceedings of the 27th International Colloquium on Automata, Languages and Programming

Safely adding computational effects to a multi-stage language has been an open problem. In previous work, a closed type constructor was used to provide a safe mechanism for executing dynamically generated code. This paper proposes a general notion of ...
Quantified types in an imperative language

We describe universal types, existential types, and type constructors in Cyclone, a strongly typed C-like language. We show how the language naturally supports first-class polymorphism and polymorphic recursion while requiring an acceptable amount of ...
Existential Types for Imperative Languages
ESOP '02: Proceedings of the 11th European Symposium on Programming Languages and Systems

We integrate existential types into a strongly typed C-like language. In particular, we show how a bad combination of existential types, mutation, and aliasing can cause a subtle violation of type safety. We explore two independent ways to strengthen ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image Journal of Functional Programming

Journal of Functional Programming Volume 13, Issue 3

May 2003

253 pages

ISSN:0956-7968

Issue’s Table of Contents

Publisher

Cambridge University Press

United States

Publication History

Published: 01 May 2003

Qualifiers

Article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

29
Total Citations
View Citations
0
Total Downloads

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

Reflects downloads up to 12 Nov 2024

Other Metrics

View Author Metrics

Citations

Cited By

Suwa TIgarashi A(2024)An ML-Style Module System for Cross-Stage Type Abstraction in Multi-stage ProgrammingFunctional and Logic Programming10.1007/978-981-97-2300-3_13(237-272)Online publication date: 15-May-2024
https://dl.acm.org/doi/10.1007/978-981-97-2300-3_13
Xie NWhite LNicole OYallop J(2023)MacoCaml: Staging Composable and Compilable MacrosProceedings of the ACM on Programming Languages10.1145/36078517:ICFP(604-648)Online publication date: 31-Aug-2023
https://dl.acm.org/doi/10.1145/3607851
Caires LToninho B(2019)Refinement kinds: type-safe programming with practical type-level computationProceedings of the ACM on Programming Languages10.1145/33605573:OOPSLA(1-30)Online publication date: 10-Oct-2019
https://dl.acm.org/doi/10.1145/3360557
Sampson AMcKinley KMytkowicz T(2017)Static stages for heterogeneous programmingProceedings of the ACM on Programming Languages10.1145/31338951:OOPSLA(1-27)Online publication date: 12-Oct-2017
https://dl.acm.org/doi/10.1145/3133895
Suwa TTsukada TKobayashi NIgarashi ASchultz UYallop J(2017)Verification of code generators via higher-order model checkingProceedings of the 2017 ACM SIGPLAN Workshop on Partial Evaluation and Program Manipulation10.1145/3018882.3018886(59-70)Online publication date: 2-Jan-2017
https://dl.acm.org/doi/10.1145/3018882.3018886
Davies R(2017)A Temporal Logic Approach to Binding-Time AnalysisJournal of the ACM10.1145/301106964:1(1-45)Online publication date: 24-Mar-2017
https://dl.acm.org/doi/10.1145/3011069
Kameyama YKiselyov OShan C(2015)Combinators for impure yet hygienic code generationScience of Computer Programming10.1016/j.scico.2015.08.007112:P2(120-144)Online publication date: 15-Nov-2015
https://dl.acm.org/doi/10.1016/j.scico.2015.08.007
Kameyama YKiselyov OShan CChin WHage J(2014)Combinators for impure yet hygienic code generationProceedings of the ACM SIGPLAN 2014 Workshop on Partial Evaluation and Program Manipulation10.1145/2543728.2543740(3-14)Online publication date: 11-Jan-2014
https://dl.acm.org/doi/10.1145/2543728.2543740
Mainland G(2012)Explicitly heterogeneous metaprogramming with MetaHaskellACM SIGPLAN Notices10.1145/2398856.236457247:9(311-322)Online publication date: 9-Sep-2012
https://dl.acm.org/doi/10.1145/2398856.2364572
Mainland GThiemann PFindler R(2012)Explicitly heterogeneous metaprogramming with MetaHaskellProceedings of the 17th ACM SIGPLAN international conference on Functional programming10.1145/2364527.2364572(311-322)Online publication date: 9-Sep-2012
https://dl.acm.org/doi/10.1145/2364527.2364572
Show More Cited By

View Options

View options

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 Publication

Media

Figures

Other

Tables

View Issue’s Table of Contents