Abstract
Generating high-performance code and applying typical optimizations within the bodies of loops and functions involves moving or storing open code for later use, often in a different binding environment. There are ample opportunities for variables being left unbound or accidentally captured. It has been a tough challenge to statically ensure that by construction the generated code is nevertheless well-typed and well-scoped: all free variables in manipulated and stored code fragments shall eventually be bound, by their intended binders.
We present the calculus for code generation with mutable state that for the first time achieves type-safety and hygiene without ad hoc restrictions. The calculus strongly resembles region-based memory management, but with the orders of magnitude simpler proofs. It employs the rightly abstract representation for free variables, which, like hypothesis in natural deduction, are free from the bureaucracy of syntax imposed by the type environment or numbering conventions.
Although the calculus was designed for the sake of formalization and is deliberately bare-bone, it turns out easily implementable and not too bothersome for writing realistic program.
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
Notes
- 1.
The StagedHaskell library, the prototype of \({\texttt {<\!NJ\!>}}\), is a code-combinator library.
- 2.
This restriction certainly simplifies the formalism. It is also realistic: in all our experience of using MetaOCaml, the multi-stage language, we are yet to come across any real-life example needing more than two stages. Template Haskell is also two-stage.
- 3.
If we generate code for later use, e.g., as a library of specialized algorithms, it makes no sense for the generated code to contain pointers into the generator’s heap. By the time the produced code is run, the generator will be long gone. Although shared heap may be useful in run-time-code specialization, none of the staged calculi to our knowledge consider this case.
References
Calcagno, C., Moggi, E., Taha, W.: Closed types as a simple approach to safe imperative multi-stage programming. In: Montanari, U., Rolim, J.D.P., Welzl, E. (eds.) ICALP 2000. LNCS, vol. 1853, pp. 25–36. Springer, Heidelberg (2000). doi:10.1007/3-540-45022-X_4
Calcagno, C., Taha, W., Huang, L., Leroy, X.: Implementing multi-stage languages using ASTs, gensym, and reflection. In: Pfenning, F., Smaragdakis, Y. (eds.) GPCE 2003. LNCS, vol. 2830, pp. 57–76. Springer, Heidelberg (2003). doi:10.1007/978-3-540-39815-8_4
Chen, C., Xi, H.: Meta-programming through typeful code representation. J. Funct. Program. 15(6), 797–835 (2005)
Davies, R.: A temporal logic approach to binding-time analysis. In: LICS, pp. 184–195 (1996)
Fluet, M., Morrisett, J.G.: Monadic regions. J. Funct. Program. 16(4–5), 485–545 (2006)
Kameyama, Y., Kiselyov, O., Shan, C.: Combinators for impure yet hygienic code generation. Sci. Comput. Program. 112, 120–144 (2015)
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.: The design and implementation of BER MetaOCaml. In: Codish, M., Sumii, E. (eds.) FLOPS 2014. LNCS, vol. 8475, pp. 86–102. Springer, Heidelberg (2014). doi:10.1007/978-3-319-07151-0_6
Le Botlan, D., Rémy, D.: ML\(^{\rm F}\): raising ML to the power of system F. In: ICFP, pp. 27–38 (2003)
Nanevski, A., Pfenning, F., Pientka, B.: Contextual modal type theory. Trans. Comput. Logic 9(3), 1–49 (2008)
POPL 2003: Conference Record of the Annual ACM Symposium on Principles of Programming Languages (2003)
Pottier, F.: Static name control for FreshML. In: LICS, pp. 356–365. IEEE Computer Society (2007)
Pouillard, N., Pottier, F.: A fresh look at programming with names and binders. In: ICFP, pp. 217–228. ACM, New York (2010)
Rompf, T., Amin, N., Moors, A., Haller, P., Odersky, M.: Scala-virtualized: linguistic reuse for deep embeddings. High. Order Symbolic Comput. 25, 165–207 (2013)
Taha, W., Nielsen, M.F.: Environment classifiers. In: POPL [11], pp. 26–37
Thiemann, P.: Combinators for program generation. J. Funct. Program. 9(5), 483–525 (1999)
Westbrook, E., Ricken, M., Inoue, J., Yao, Y., Abdelatif, T., Taha, W.: Mint: Java multi-stage programming using weak separability. In: PLDI 2010. ACM, New York (2010)
Xi, H., Chen, C., Chen, G.: Guarded recursive datatype constructors. In: POPL [11], pp. 224–235
Acknowledgments
We thank anonymous reviewers for many helpful comments. This work was partially supported by JSPS KAKENHI Grant Numbers 15K12007, 16K12409, 15H02681.
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Appendices
AÂ Proof Outlines: Subject Reduction Theorem
Lemma 1
(Substitution). (1) If 
and 
then 
. (2) If 
and 
and 
, then 
(if L was 
it is also replaced with 
).
This lemma is proved straightforwardly.
Theorem 3
(Subject Reduction). If 
, 
, 
, and 
, then 
, 
, 
, for some 
and 
that are the extensions of the corresponding unprimed things.
Proof. We consider a few interesting reductions. The first one is
We are given 
is 
, 
is H, and 
, which means 
and 
for a fresh 
. We choose 
as 
where 
is fresh, and 
as \(\varTheta \). 
is well-formed and is an extension of \(\varUpsilon \). Furthermore, 
. By weakening, 
and 
if it was for \(\varUpsilon \). We only need to show that 
, which follows by (IAbs) from 
, which in turn follows from the fact that 
and the substitution lemma.
The next reduction is
We are given 
, 
and 
. Since N and H are unchanged by the reduction, we do not extend \(\varUpsilon \) and \(\varTheta \). By inversion of (IAbs) we know that \(\varUpsilon \) is 
and 
and 
, or, by inversion of (Code) 
. By weakening, 
. An easy substitution lemma gives us 
where 
is 
, keeping in mind that 
. The crucial step is strengthening. Since we have just substituted away 
, which is the only variable with the classifier 
(the correspondence of variable names and classifiers is the consequence of well-formedness), the derivation 
has no occurrence of the rule (Var) with L equal to 
. Therefore, any subderivation with L being 
must have the occurrence of the (Sub1) rule, applied to the derivation 
where 
and 
is different from 
. The inversion of (IAbs) gave us 
. Therefore, we can always replace each such occurrence of (Sub1) with the one that gives us 
. All in all, we build the derivation of 
, which gives us 
and then 
.
Another interesting case is
Given, 
which means 
. Take 
. It is easy to see that 
and 
. The rest follows from the substitution lemma.
BÂ Generating Code with Arbitrary Many Variables
Our example is the Fibonacci-like function, described in [6, Sect. 2.4]:
For example, 
returns 
. The naive specialization to the given n
is unsatisfactory: 
generates
with many duplicates, exponentially degrading performance. A slight change
gives a much better result: 
produces
which runs in linear time. The improved generator relies on polymorphic recursion: that is why the signature is needed.
Rights and permissions
Copyright information
© 2016 Springer International Publishing AG
About this paper
Cite this paper
Kiselyov, O., Kameyama, Y., Sudo, Y. (2016). Refined Environment Classifiers. In: Igarashi, A. (eds) Programming Languages and Systems. APLAS 2016. Lecture Notes in Computer Science(), vol 10017. Springer, Cham. https://doi.org/10.1007/978-3-319-47958-3_15
Download citation
DOI: https://doi.org/10.1007/978-3-319-47958-3_15
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-47957-6
Online ISBN: 978-3-319-47958-3
eBook Packages: Computer ScienceComputer Science (R0)