×

Finally tagless, partially evaluated: tagless staged interpreters for simpler typed languages. (English) Zbl 1191.68158

Summary: We have built the first family of tagless interpretations for a higher-order typed object language in a typed metalanguage (Haskell or ML) that require no dependent types, generalized algebraic data types, or postprocessing to eliminate tags. The statically type-preserving interpretations include an evaluator, a compiler (or staged evaluator), a partial evaluator, and call-by-name and call-by-value continuation-passing style (CPS) transformers. Our principal technique is to encode de Bruijn or higher-order abstract syntax using combinator functions rather than data constructors. In other words, we represent object terms not in an initial algebra but using the coalgebraic structure of the \(\lambda\)-calculus. Our representation also simulates inductive maps from types to types, which are required for typed partial evaluation and CPS transformations. Our encoding of an object term abstracts uniformly over the family of ways to interpret it, yet statically assures that the interpreters never get stuck. This family of interpreters thus demonstrates again that it is useful to abstract over higher-kinded types.

MSC:

68N18 Functional programming and lambda calculus
Full Text: DOI

References:

[1] DOI: 10.1145/215465.215469 · doi:10.1145/215465.215469
[2] DOI: 10.1017/S0956796800000423 · Zbl 0817.68051 · doi:10.1017/S0956796800000423
[3] DOI: 10.1016/0022-0000(78)90014-4 · Zbl 0388.68003 · doi:10.1016/0022-0000(78)90014-4
[4] Miller, IEEE Symposium on Logic Programming pp 379– (1987)
[5] DOI: 10.1007/3-540-45350-4_11 · doi:10.1007/3-540-45350-4_11
[6] Läufer, Proceedings of the 4th Annual OOPSLA/ECOOP Workshop on Object-Oriented Reflection and Metalevel Architectures (1993)
[7] DOI: 10.1145/365230.365257 · Zbl 0149.12505 · doi:10.1145/365230.365257
[8] DOI: 10.1007/BF01806312 · doi:10.1007/BF01806312
[9] Jones, Handbook of Logic in Computer Science pp 527– (1994)
[10] Jones, Partial Evaluation and Automatic Program Generation (1993)
[11] DOI: 10.1145/289121.289135 · doi:10.1145/289121.289135
[12] DOI: 10.1145/242224.242477 · doi:10.1145/242224.242477
[13] DOI: 10.1017/S096012959900287X · Zbl 0935.03046 · doi:10.1017/S096012959900287X
[14] DOI: 10.1007/BFb0014057 · doi:10.1007/BFb0014057
[15] Holst, Partial Evaluation and Mixed Computation pp 167– (1988)
[16] Hofer, ACM Conference on Generative Programming and Component Engineering GPCE (2008)
[17] DOI: 10.1016/j.scico.2003.07.001 · Zbl 1091.68025 · doi:10.1016/j.scico.2003.07.001
[18] DOI: 10.2307/1995158 · Zbl 0196.01501 · doi:10.2307/1995158
[19] DOI: 10.1145/199448.199475 · doi:10.1145/199448.199475
[20] Guillemette, PLPV 2006: Programming Languages Meets Program Verification pp 40– (2006)
[21] DOI: 10.1017/S0956796800000058 · Zbl 1155.68350 · doi:10.1017/S0956796800000058
[22] Futamura, Sys. Comp. Controls 2 pp 45– (1971)
[23] Fogarty, Proceedings of the 2007 ACM SIGPLAN Workshop on Partial Evaluation and Semantics-Based Program Manipulation (2007)
[24] DOI: 10.1145/53990.54010 · doi:10.1145/53990.54010
[25] DOI: 10.1145/1159803.1159811 · doi:10.1145/1159803.1159811
[26] Pašalić, ICFP 2002. Proceedings of the ACM International Conference on Functional Programming pp 157– (2002)
[27] DOI: 10.1145/571157.571161 · doi:10.1145/571157.571161
[28] Filinski, POPL ’94: Conference Record of the Annual ACM Symposium on Principles of Programming Languages pp 446– (1994)
[29] DOI: 10.1145/382780.382785 · Zbl 1323.68107 · doi:10.1145/382780.382785
[30] Danvy, Programming Languages and Systems: Proceedings of ESOP 2003, 12th European Symposium on Programming pp 335– (2003)
[31] DOI: 10.1016/j.tcs.2003.11.017 · Zbl 1072.68032 · doi:10.1016/j.tcs.2003.11.017
[32] DOI: 10.1145/604131.604150 · Zbl 1321.68161 · doi:10.1145/604131.604150
[33] DOI: 10.1017/S0960129500001535 · doi:10.1017/S0960129500001535
[34] Danvy, Proceedings of ICALP 98: 25th International Colloquium on Automata, Languages, and Programming pp 908– (1998) · doi:10.1007/BFb0055112
[35] DOI: 10.1145/237721.237784 · doi:10.1145/237721.237784
[36] DOI: 10.1145/154630.154645 · doi:10.1145/154630.154645
[37] DOI: 10.1145/777388.777392 · doi:10.1145/777388.777392
[38] DOI: 10.1017/S0956796807006557 · Zbl 1128.68021 · doi:10.1017/S0956796807006557
[39] Carette, APLAS pp 222– (2007)
[40] Thiemann, Proceedings Informatik 97 pp 582– (1997)
[41] DOI: 10.1007/11561347_18 · doi:10.1007/11561347_18
[42] DOI: 10.1017/S0956796899003469 · Zbl 0945.68029 · doi:10.1017/S0956796899003469
[43] Calcagno, Programming Languages and Systems: Proceedings of ESOP 2004, 13th European Symposium on Programming pp 79– (2004)
[44] DOI: 10.1145/604131.604134 · Zbl 1321.68175 · doi:10.1145/604131.604134
[45] DOI: 10.1016/0167-6423(91)90002-F · Zbl 0745.68073 · doi:10.1016/0167-6423(91)90002-F
[46] DOI: 10.1007/3-540-44978-7_15 · doi:10.1007/3-540-44978-7_15
[47] DOI: 10.1016/0304-3975(85)90135-5 · Zbl 0597.68017 · doi:10.1016/0304-3975(85)90135-5
[48] DOI: 10.1145/328690.328697 · doi:10.1145/328690.328697
[49] DOI: 10.1023/A:1012984529382 · Zbl 0994.68037 · doi:10.1023/A:1012984529382
[50] DOI: 10.1145/258915.258935 · doi:10.1145/258915.258935
[51] Sperber, Partial Evaluation pp 465– (1996) · doi:10.1007/3-540-61580-6_23
[52] DOI: 10.1145/581690.581691 · doi:10.1145/581690.581691
[53] DOI: 10.1145/1053468.1053469 · doi:10.1145/1053468.1053469
[54] DOI: 10.1145/289423.289436 · Zbl 1369.68125 · doi:10.1145/289423.289436
[55] Reynolds, New Directions in Algorithmic Languages 1975 pp 157– (1975)
[56] Reynolds, Automata, Languages and Programming: 2nd Colloquium pp 141– (1974) · doi:10.1007/3-540-06841-4_57
[57] Reynolds, Proceedings of the ACM National Conference pp 717– (1972)
[58] Ramsey, Proceedings of the 2005 Workshop on ML (2005)
[59] DOI: 10.1016/0304-3975(77)90044-5 · Zbl 0369.68006 · doi:10.1016/0304-3975(77)90044-5
[60] DOI: 10.1016/0304-3975(75)90017-1 · Zbl 0325.68006 · doi:10.1016/0304-3975(75)90017-1
[61] DOI: 10.1016/0304-3975(90)90109-U · Zbl 0736.03003 · doi:10.1016/0304-3975(90)90109-U
[62] DOI: 10.1145/289423.289440 · doi:10.1145/289423.289440
[63] Berarducci, Logic and Algebra pp 339– (1996)
[64] DOI: 10.1017/S0956796804005398 · Zbl 1086.68525 · doi:10.1017/S0956796804005398
[65] Bawden, Proceedings of the 1999 ACM SIGPLAN Workshop on Partial Evaluation and Semantics-Based Program Manipulation pp 4– (1999)
[66] DOI: 10.1145/964001.964007 · Zbl 1325.68045 · doi:10.1145/964001.964007
[67] DOI: 10.1145/581478.581494 · Zbl 1322.68035 · doi:10.1145/581478.581494
[68] DOI: 10.1007/BF03037258 · Zbl 0994.68035 · doi:10.1007/BF03037258
[69] DOI: 10.1145/199448.199507 · doi:10.1145/199448.199507
[70] DOI: 10.1145/1088348.1088358 · doi:10.1145/1088348.1088358
[71] Nielson, Two-Level Functional Languages (1992) · Zbl 0763.68023 · doi:10.1017/CBO9780511526572
[72] DOI: 10.1145/73560.73569 · doi:10.1145/73560.73569
[73] DOI: 10.1016/0890-5401(88)90041-7 · Zbl 0636.68018 · doi:10.1016/0890-5401(88)90041-7
[74] DOI: 10.1145/1352582.1352591 · Zbl 1367.03060 · doi:10.1145/1352582.1352591
[75] DOI: 10.1017/S095679680500568X · Zbl 1085.68025 · doi:10.1017/S095679680500568X
[76] DOI: 10.1145/581478.581498 · Zbl 1322.68045 · doi:10.1145/581478.581498
[77] DOI: 10.1145/1449764.1449798 · doi:10.1145/1449764.1449798
[78] DOI: 10.1016/0890-5401(91)90052-4 · Zbl 0723.68073 · doi:10.1016/0890-5401(91)90052-4
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.