×

Type-specialized staged programming with process separation. (English) Zbl 1256.68022

Summary: Staging is a powerful language construct that allows a program at one stage of evaluation to manipulate and specialize a program to be executed at a later stage.
We propose a new staged language calculus, \(\langle ML\rangle \), which extends the programmability of staged languages in two directions. First, \(\langle ML\rangle \) supports dynamic type specialization: types can be dynamically constructed, abstracted, and passed as arguments, while preserving decidable typechecking via a System \(F_{\leq }\)-style semantics combined with a restricted form of \(\lambda _{\omega }\)-style runtime type construction. With dynamic type specialization the data structure layout of a program can be optimized via staging. Second, \(\langle ML\rangle \) works in a context where different stages of computation are executed in different process spaces, a property we term staged process separation. Programs at different stages can directly communicate program data in \(\langle ML\rangle \) via a built-in serialization discipline.
The language \(\langle ML\rangle \) is endowed with a metatheory including type preservation, type safety, and decidability as demonstrated constructively by a sound type checking algorithm. While our language design is general, we are particularly interested in future applications of staging in resource-constrained and embedded systems: these systems have limited space for code and data, as well as limited CPU time, and specializing code for the particular deployment at hand can improve efficiency in all of these dimensions.
The combination of dynamic type specialization and staging across processes greatly increases the utility of staged programming in these domains. We illustrate this via wireless sensor network programming examples.

MSC:

68N15 Theory of programming languages
68M14 Distributed systems
PDFBibTeX XMLCite
Full Text: DOI

References:

[1] Aiken, A., Wimmers, E.L., Lakshman, T.K.: Soft typing with conditional types. In: Conference Record of the Twenty-First Annual ACM Symposium on Principles of Programming Languages, pp. 163–173 (1994)
[2] Barendregt, H.: Introduction to generalized type systems. J. Funct. Program. 1(2), 125–154 (1991) · Zbl 0931.03019
[3] Bove, A., Dybjer, P., Norell, U.: A brief overview of agda–a functional language with dependent types. In: Berghofer, S., Nipkow, T., Urban, C., Wenzel, M. (eds.) Theorem Proving in Higher Order Logics. Lecture Notes in Computer Science, vol. 5674, pp. 73–78. Springer, Berlin (2009) · Zbl 1252.68062
[4] Brady, E.: Irdis: a language with dependent types. http://www.idris-lang.org (2009)
[5] Brady, E., Hammond, K.: A verified staged interpreter is a verified compiler. In: GPCE’06: Proceedings of the 5th International Conference on Generative Programming and Component Engineering, pp. 111–120. ACM, New York (2006)
[6] Calcagno, C., Moggi, E., Taha, W.: Closed types as a simple approach to safe imperative multi-stage programming. In: ICALP ’00: Proceedings of the 27th International Colloquium on Automata, Languages and Programming, pp. 25–36. Springer, London (2000) · Zbl 0973.68037
[7] Cardelli, L.: Program fragments, linking, and modularization. In: Conference Record of POPL’97: The 24th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pp. 266–277 (1997)
[8] Cardelli, L., Wegner, P.: On understanding types, data abstraction, and polymorphism. ACM Comput. Surv. 17(4), 471–523 (1985) · doi:10.1145/6041.6042
[9] Chen, C., Xi, H.: Meta-programming through typeful code representation. In: ICFP’03 (2003) · Zbl 1315.68038
[10] Chen, C., Xi, H.: Combining programming with theorem proving. In: Proceedings of the Tenth ACM SIGPLAN International Conference on Functional Programming, ICFP ’05, pp. 66–77. ACM, New York (2005) · Zbl 1302.68241
[11] Consel, C., Hornof, L., Marlet, R., Muller, G., Thibault, S., Volanschi, E.-N., Lawall, J., Noyé, J.: Tempo: specializing systems applications and beyond. ACM Comput. Surv., 19 (1998)
[12] Coquand, T., Huet, G.: The calculus of constructions. Inf. Comput. 76(2–3), 95–120 (1988) · Zbl 0654.03045 · doi:10.1016/0890-5401(88)90005-3
[13] Coquand, T., Huet, G., et al.: The Coq proof assistant. http://coq.inria.fr
[14] Crary, K., Weirich, S., Morrisett, G.: Intensional polymorphism in type-erasure semantics. J. Funct. Program. 12(6), 567–600 (2002) · Zbl 1040.68059
[15] Davies, R., Pfenning, F.: A modal analysis of staged computation. J. ACM 48(3), 555–604 (2001) · Zbl 1323.68107 · doi:10.1145/382780.382785
[16] Dreyer, D.: A type system for well-founded recursion. In: Proceedings of the 31st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL ’04, pp. 293–305 (2004) · Zbl 1325.68046
[17] Eifrig, J., Smith, S., Trifonov, V.: Type inference for recursively constrained types and its application to OOP. In: Mathematical Foundations of Programming Language Semantics (MFPS). Electronic Lecture Notes in Computer Science, vol. 1 (1995) · Zbl 0910.68143
[18] Flatt, M., Felleisen, M.: Units: cool modules for HOT languages. In: Proceedings of the ACM SIGPLAN ’98 Conference on Programming Language Design and Implementation, pp. 236–248 (1998)
[19] Fogarty, S., Pasalic, E., Siek, J., Taha, W.: Concoqtion: indexed types now! In: Proceedings of the 2007 ACM SIGPLAN Symposium on Partial Evaluation and Semantics-Based Program Manipulation, PEPM ’07, pp. 112–121. ACM, New York (2007)
[20] Ganz, S.E., Sabry, A., Taha, W.: Macros as multi-stage computations: type-safe, generative, binding macros in MacroML. In: ICFP’01: Proceedings of the Sixth ACM SIGPLAN International Conference on Functional Programming, pp. 74–85. ACM, New York (2001) · Zbl 1323.68116
[21] Gay, D., Levis, P., von Behren, R., Welsh, M., Brewer, E., Culler, D.: The nesC language: a holistic approach to networked embedded systems. In: PLDI’03: Proceedings of the ACM SIGPLAN 2003 Conference on Programming Language Design and Implementation, pp. 1–11. ACM, New York (2003)
[22] Ghelli, G., Pierce, B.: Bounded existentials and minimal typing. Theor. Comput. Sci. 193(1–2), 75–96 (1998) · Zbl 0909.03017 · doi:10.1016/S0304-3975(96)00300-3
[23] Gillenwater, J., Malecha, G., Salama, C., Zhu, A.Y., Taha, W., Grundy, J., O’Leary, J.: Synthesizable high level hardware descriptions: using statically typed two-level languages to guarantee verilog synthesizability. In: Proceedings of the 2008 ACM SIGPLAN Symposium on Partial Evaluation and Semantics-Based Program Manipulation, PEPM ’08, pp. 41–50. ACM, New York (2008)
[24] Harper, R., Mitchell, J.C., Moggi, E.: Higher-order modules and the phase distinction. In: Seventeenth ACM Symposium on Principles of Programming Languages, pp. 341–354. ACM Press, New York (1990)
[25] Harper, R., Morrisett, G.: Compiling polymorphism using intensional type analysis. In: Twenty-Second ACM Symposium on Principles of Programming Languages, pp. 130–141. ACM Press, New York (1995)
[26] Hill, J., Szewczyk, R., Woo, A., Hollar, S., Culler, D.E., Pister, K.S.J.: System architecture directions for networked sensors. In: Architectural Support for Programming Languages and Operating Systems, pp. 93–104 (2000)
[27] Honsell, F., Mason, I.A., Smith, S., Talcott, C.: A variable typed logic of effects. Inf. Comput. 119, 55–90 (1993) · Zbl 0832.68009 · doi:10.1006/inco.1995.1077
[28] Kameyama, Y., Kiselyov, O., Shan, C.-c.: Shifting the stage: staging with delimited control. In: PEPM’09: Proceedings of the 2009 ACM SIGPLAN Workshop on Partial Evaluation and Program Manipulation, pp. 111–120. ACM, New York (2009) · Zbl 1248.68132
[29] Kiselyov, O., Swadi, K.N., Taha, W.: A methodology for generating verified combinatorial circuits. In: Proceedings of the 4th ACM International Conference on Embedded Software, EMSOFT ’04, pp. 249–258. ACM, New York (2004)
[30] Krishnamurthi, S., Felleisen, M., Duba, B.F.: From macros to reusable generative programming. In: International Symposium on Generative and Component-Based Software Engineering. Lecture Notes in Computer Science, vol. 1799, pp. 105–120. Springer, Berlin (1999)
[31] Leroy, X.: Applicative functors and fully transparent higher-order modules. In: POPL, pp. 142–153 (1995)
[32] Leroy, X.: A modular module system. J. Funct. Program. 10(3), 269–303 (2000) · Zbl 0957.68026 · doi:10.1017/S0956796800003683
[33] Liu, Y.D., Skalka, C., Smith, S.: Type-specialized staged programming with process separation. In: Workshop on Generic Programming (WGP 09), Edinburgh, Scotland (2009) · Zbl 1256.68022
[34] MacQueen, D.: Modules for standard ML. In: Proceedings of ACM Conference on Lisp and Functional Programming, pp. 409–423 (1984)
[35] Madden, S., Franklin, M.J., Hellerstein, J.M., Hong, W.: TAG: a Tiny AGgregation service for ad-hoc sensor networks. SIGOPS Oper. Syst. Rev. 36(SI), 131–146 (2002) · doi:10.1145/844128.844142
[36] Mainland, G., Morrisett, G., Welsh, M.: Flask: staged functional programming for sensor networks. In: 13th ACM SIGPLAN International Conference on Functional Programming (ICFP 2008), September (2008)
[37] Martin-Löf, P.: An intuitionistic theory of types: predicative part. In: Rose, H.F., Shepherdson, J.C. (eds.) Logic Colloquium ’73, pp. 73–118. North-Holland, Amsterdam (1973)
[38] Moggi, E., Fagorzi, S.: A monadic multi-stage metalanguage. In: Gordon, A.D. (ed.) FoSSaCS. Lecture Notes in Computer Science, vol. 2620, pp. 358–374. Springer, Berlin (2003) · Zbl 1029.68042
[39] Moggi, E., Taha, W., El abidine Benaissa, Z., Sheard, T.: An idealized MetaML: simpler, and more expressive. In: European Symposium on Programming (ESOP), pp. 193–207. Springer, Berlin (1999)
[40] Monnier, S., Shao, Z.: Inlining as staged computation. J. Funct. Program. 13(3), 647–676 (2003) · Zbl 1036.68018 · doi:10.1017/S0956796802004616
[41] Murphy VII, T., Crary, K., Harper, R., Pfenning, F.: A symmetric modal lambda calculus for distributed computing. In: LICS ’04: Proceedings of the 19th Annual IEEE Symposium on Logic in Computer Science, pp. 286–295. IEEE Computer Society, Washington (2004)
[42] Nanevski, A.: Meta-programming with names and necessity. In: ICFP’02: Proceedings of the Seventh ACM SIGPLAN International Conference on Functional Programming pp. 206–217. ACM, New York (2002) · Zbl 1322.68045
[43] Nanevski, A., Morrisett, G., Shinnar, A., Govereau, P., Birkedal, L.: Ynot: dependent types for imperative programs. In: ICFP ’08: Proceedings of the 13th ACM SIGPLAN International Conference on Functional Programming (2008) · Zbl 1323.68142
[44] Newton, R., Morrisett, G., Welsh, M.: The regiment macroprogramming system. In: IPSN’07: Proceedings of the 6th International Conference on Information Processing in Sensor Networks, pp. 489–498 (2007)
[45] Pasalic, E., Taha, W., Sheard, T., Tim, S.: Tagless staged interpreters for typed languages. In: The International Conference on Functional Programming (ICFP’02), pp. 218–229. ACM, New York (2002) · Zbl 1322.68033
[46] Pottier, F.: A versatile constraint-based type inference system. Nord. J. Comput. 7(4), 312–347 (2000) · Zbl 0970.68017
[47] Salama, C., Malecha, G., Taha, W., Grundy, J., O’Leary, J.: Static consistency checking for verilog wire interconnects: using dependent types to check the sanity of verilog descriptions. In: Proceedings of the 2009 ACM SIGPLAN Workshop on Partial Evaluation and Program Manipulation, PEPM’09, pp. 121–130. ACM, New York (2009)
[48] Schurgers, C., Kulkarni, G., Srivastava, M.B.: Distributed on-demand address assignment in wireless sensor networks. IEEE Trans. Parallel Distrib. Syst. 13(10), 1056–1065 (2002) · Zbl 05107727 · doi:10.1109/TPDS.2002.1041881
[49] Shi, R., Chen, C., Xi, H.: Distributed meta-programming. In: GPCE’06: Proceedings of the 5th International Conference on Generative Programming and Component Engineering, pp. 243–248 (2006)
[50] Taha, W.: A gentle introduction to multi-stage programming. In: Lengauer, C., Batory, D., Consel, C., Odersky, M. (eds.) Domain-Specific Program Generation. Lecture Notes in Computer Science, vol. 3016, pp. 30–50. Springer, Berlin (2004). doi: 10.1007/978-3-540-25935-03
[51] Taha, W.: Resource-aware programming. In: Wu, Z., Chen, C., Guo, M., Bu, J. (eds.) ICESS. Lecture Notes in Computer Science, vol. 3605, pp. 38–43. Springer, Berlin (2004)
[52] Taha, W., El-abidine Benaissa, Z., Sheard, T.: Multi-stage programming: axiomatization and type safety (extended abstract). In: 25th International Colloquium on Automata, Languages, and Programming, pp. 918–929. Springer, Berlin (1998)
[53] Taha, W., Ellner, S., Xi, H.: Generating heap-bounded programs in a functional setting. In: EMSOFT, pp. 340–355. Springer, Berlin (2003)
[54] Taha, W., et al.: MetaOCaml: a compiled, type-safe multi-stage programming language. http://www.metaocaml.org/
[55] Taha, W., Nielsen, M.F.: Environment classifiers. In: POPL’03 (2003) · Zbl 1321.68175
[56] Taha, W., Sheard, T.: Multi-stage programming with explicit annotations. In: PEPM ’97: Proceedings of the 1997 ACM SIGPLAN Symposium on Partial Evaluation and Semantics-Based Program Manipulation, pp. 203–217 (1997) · Zbl 0949.68047
[57] Wan, Z., Hudak, P.: Functional reactive programming from first principles. In: PLDI ’00: Proceedings of the ACM SIGPLAN 2000 Conference on Programming Language Design and Implementation, pp. 242–252. ACM, New York (2000)
[58] Xi, H., Chen, C., Chen, G.: Guarded recursive datatype constructors. In: POPL’03: Proceedings of the 30th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pp. 224–235. ACM, New York (2003) · Zbl 1321.68161
[59] Xi, H., Pfenning, F.: Dependent types in practical programming. In: Proceedings of the 26th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL’99, pp. 214–227. ACM, New York (1999)
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.