research-article

Public Access

Type systems as macros

Authors:

Ben GreenmanAuthors Info & Claims

ACM SIGPLAN Notices, Volume 52, Issue 1

Pages 694 - 705

https://doi.org/10.1145/3093333.3009886

Published: 01 January 2017 Publication History

Abstract

We present Turnstile, a metalanguage for creating typed embedded languages. To implement the type system, programmers write type checking rules resembling traditional judgment syntax. To implement the semantics, they incorporate elaborations into these rules. Turnstile critically depends on the idea of linguistic reuse. It exploits a macro system in a novel way to simultaneously type check and rewrite a surface program into a target language. Reusing a macro system also yields modular implementations whose rules may be mixed and matched to create other languages. Combined with typical compiler and runtime reuse, Turnstile produces performant typed embedded languages with little effort.

References

[1]

The computer language benchmarks game.

[2]

C. Andreae, J. Noble, S. Markstrum, and T. Millstein. A framework for implementing pluggable type systems. In Proceedings of the 21st Annual ACM SIGPLAN Conference on Object-oriented Programming Systems, Languages, and Applications, pages 57–74, 2006.

Digital Library

[3]

P. Bagwell. DSLs - A powerful Scala feature, 2009.

[4]

G. Bracha. Pluggable type systems. In OOPSLA Workshop on Revival of Dynamic Languages, 2004.

[5]

N. G. D. Bruijn. Lambda calculus notation with nameless dummies, a tool for automatic formula manipulation, with application to the Church-Rosser theorem. INDAG. MATH, 34:381–392, 1972.

[6]

E. Burmako. Scala macros: Let our powers combine!: On how rich syntax and static types work with metaprogramming. In Proceedings of the 4th Workshop on Scala, 2013.

Digital Library

[7]

M. Butterick. Pollen: the book is a program, 2013.

[8]

N. Cameron. Sets of scopes macro hygiene in Rust, 2015.

[9]

R. Culpepper and M. Felleisen. Fortifying macros. In Proceeding of the 15th ACM SIGPLAN International Conference on Functional Programming, pages 235–246, 2010.

Digital Library

[10]

T. Disney. Hygienic Macros for JavaScript. PhD thesis, University of California Santa Cruz, 2015.

[11]

S. Erdweg, T. Rendel, C. Kästner, and K. Ostermann. SugarJ: Librarybased syntactic language extensibility. In Proceedings of the ACM SIGPLAN International Conference on Object-oriented Programming Systems Languages and Applications, pages 391–406, 2011.

Digital Library

[12]

M. Felleisen, R. B. Findler, M. Flatt, S. Krishnamurthi, E. Barzilay, J. McCarthy, and S. Tobin-Hochstadt. The Racket Manifesto. In 1st Summit on Advances in Programming Languages (SNAPL 2015), pages 113–128, 2015.

[13]

D. Fisher and O. Shivers. Static analysis for syntax objects. In Proceedings of the 11th ACM SIGPLAN International Conference on Functional Programming, pages 111–121, 2006.

Digital Library

[14]

M. Flatt. Binding as sets of scopes. In Proceedings of the 43rd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pages 705–717, 2016.

Digital Library

[15]

M. Flatt and PLT. Reference: Racket. Technical Report PLT-TR-2010- 1, PLT Design Inc., 2010. http://racket-lang.org/tr1/.

[16]

M. Flatt, R. Culpepper, D. Darais, and R. B. Findler. Macros that work together. Journal of Functional Programming, 22(2):181–216, 2012.

Digital Library

[17]

M. Fowler and R. Parsons. Domain-Specific Languages. Addison-Wesley, 2010.

Digital Library

[18]

S. Freeman, T. Mackinnon, N. Pryce, and J. Walnes. Mock roles, not objects. In Companion to the 19th Annual ACM SIGPLAN Conference on Object-oriented Programming Systems, Languages, and Applications, pages 236–246, 2004.

Digital Library

[19]

M. Gasbichler and M. Sperber. Integrating user-level threads with processes in Scsh. Higher Order Symbol. Comput., 18(3-4):327–354, 2005.

Digital Library

[20]

P. Graham. On Lisp. Prentice Hall, 1993.

[21]

B. Greenman. Trivial: Observably smarter typechecking, 2016.

[22]

D. Herman, L. Wagner, and A. Zakai. asm.js working draft, 2014.

[23]

P. Hudak. Building domain-specific embedded languages. ACM Comput. Surv., 28(4es), 1996.

Digital Library

[24]

P. Hudak. Modular domain specific languages and tools. In Proceedings of the 5th International Conference on Software Reuse, pages 134–142, 1998.

Digital Library

[25]

S. Kamin and D. Hyatt. A special-purpose language for picturedrawing. In Proceedings of the USENIX Conference on Domain-Specific Languages, pages 297–310, 1997.

Digital Library

[26]

G. Kossakowski, N. Amin, T. Rompf, and M. Odersky. JavaScript as an embedded DSL. In European Conference on Object-Oriented Programming, pages 409–434. Springer Berlin Heidelberg, 2012.

Digital Library

[27]

S. Krishnamurthi. Linguistic Reuse. PhD thesis, Rice University, 2001.

Digital Library

[28]

B. S. Lerner, J. G. Politz, A. Guha, and S. Krishnamurthi. Tejas: retrofitting type systems for JavaScript. In Proceedings of the 9th Symposium on Dynamic Languages, pages 1–16, 2013.

Digital Library

[29]

M. Y. Levin and B. C. Pierce. TinkerType: A language for playing with formal systems. J. Funct. Program., 13(2):295–316, 2003.

Digital Library

[30]

F. Lorenzen and S. Erdweg. Sound type-dependent syntactic language extension. In Proceedings of the 43rd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pages 204–216, 2016.

Digital Library

[31]

Y. Minsky, A. Madhavapeddy, and J. Hickey. Real World OCaml. O’Reilly Media, 2013.

[32]

S. Moore, C. Dimoulas, D. King, and S. Chong. Shill: A secure shell scripting language. In Proceedings of the 11th USENIX Conference on Operating Systems Design and Implementation, pages 183–199, 2014.

Digital Library

[33]

F. Nielson and H. R. Nielson. Correct System Design: Recent Insights and Advances, chapter Type and Effect Systems, pages 114– 136. Springer Berlin Heidelberg, 1999.

Digital Library

[34]

C. Okasaki. Purely Functional Data Structures. Cambridge University Press, 1999.

Digital Library

[35]

C. Omar and J. Aldrich. Programmable semantic fragments: The design and implementation of typy. In Proceedings of the 15th International Conference on Generative Programming: Concepts & Experience, page (to appear), 2016.

Digital Library

[36]

C. Omar, D. Kurilova, L. Nistor, B. Chung, A. Potanin, and J. Aldrich. Safely composable type-specific languages. In Proceedings of the European Conference on Object-Oriented Programming, pages 105– 130. 2014.

Digital Library

[37]

M. M. Papi, M. Ali, T. L. Correa Jr., J. H. Perkins, and M. D. Ernst. Practical pluggable types for Java. In Proceedings of the 2008 International Symposium on Software Testing and Analysis, pages 201–212, 2008.

Digital Library

[38]

B. C. Pierce. Types and Programming Languages. MIT Press, 2002.

Digital Library

[39]

B. C. Pierce and D. N. Turner. Local type inference. In Proceedings of the 25th ACM SIGPLAN–SIGACT Symposium on Principles of Programming Languages, pages 252–265, 1998.

Digital Library

[40]

J. G. Siek, M. M. Vitousek, M. Cimini, and J. T. Boyland. Refined criteria for gradual typing. In 1st Summit on Advances in Programming Languages, pages 274–293, 2015.

[41]

T. S. Strickland, B. M. Ren, and J. S. Foster. Contracts for domainspecific languages in Ruby. In Proceedings of the 10th ACM Symposium on Dynamic Languages, pages 23–34, 2014.

Digital Library

[42]

S. Tobin-Hochstadt and M. Felleisen. The design and implementation of Typed Scheme. In Proceedings of the 35th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pages 395– 406, 2008.

Digital Library

[43]

S. Tobin-Hochstadt, V. St-Amour, R. Culpepper, M. Flatt, and M. Felleisen. Languages as libraries. In Proceedings of the 32nd ACM SIGPLAN Conference on Programming Language Design and Implementation, pages 132–141, 2011.

Digital Library

[44]

E. Torlak and R. Bodik. A lightweight symbolic virtual machine for solver-aided host languages. In Proceedings of the 35th ACM SIGPLAN Conference on Programming Language Design and Implementation, pages 530–541, 2014.

Digital Library

[45]

B. Valiron, N. J. Ross, P. Selinger, D. S. Alexander, and J. M. Smith. Programming the quantum future. Communications of the ACM, 58 (8):52–61, 2015.

Digital Library

[46]

T. Veldhuizen. Using C++ template metaprograms. C++ Report, 7 (4):36–43, May 1995.

[47]

P. Wadler and S. Blott. How to make ad-hoc polymorphism less adhoc. In Proceedings of the 16th ACM Symposium on Principles of Programming Languages, pages 60–76, 1989.

Digital Library

[48]

J. Yallop and L. White. Modular macros. In Proceedings of the OCaml Users and Developers Workshop, 2015.

Cited By

Flatt MAllred TAngle NDe Gabrielle SFindler RFirth JGopinathan KGreenman BKasivajhula SKnauth AMcCarthy JPhillips SPorncharoenwase SSøgaard JTobin-Hochstadt S(2023)Rhombus: A New Spin on Macros without All the ParenthesesProceedings of the ACM on Programming Languages10.1145/36228187:OOPSLA2(574-603)Online publication date: 16-Oct-2023
https://dl.acm.org/doi/10.1145/3622818
Ballantyne MKing AFelleisen M(2020)Macros for domain-specific languagesProceedings of the ACM on Programming Languages10.1145/34282974:OOPSLA(1-29)Online publication date: 13-Nov-2020
https://doi.org/10.1145/3428297
CALDWELL SGARNOCK-JONES TFELLEISEN M(2020)Typed dataspace actorsJournal of Functional Programming10.1017/S095679682000024630Online publication date: 24-Aug-2020
https://doi.org/10.1017/S0956796820000246
Show More Cited By

Index Terms

Type systems as macros
1. Software and its engineering
  1. Software notations and tools
    1. General programming languages
      1. Language types

Recommendations

Type systems as macros
POPL '17: Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages

We present Turnstile, a metalanguage for creating typed embedded languages. To implement the type system, programmers write type checking rules resembling traditional judgment syntax. To implement the semantics, they incorporate elaborations into these ...
Macros for domain-specific languages

Macros provide a powerful means of extending languages. They have proven useful in both general-purpose and domain-specific programming contexts. This paper presents an architecture for implementing macro-extensible DSLs on top of macro-extensible host ...
Dependent type systems as macros

We present Turnstile+, a high-level, macros-based metaDSL for building dependently typed languages.

With it, programmers may rapidly prototype and iterate on the design of new dependently typed features and extensions.

Or they may create entirely new ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM SIGPLAN Notices

ACM SIGPLAN Notices Volume 52, Issue 1

POPL '17

January 2017

901 pages

ISSN:0362-1340

EISSN:1558-1160

DOI:10.1145/3093333

Editor:
Matthew Fluet

Issue’s Table of Contents

POPL '17: Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages
January 2017
901 pages
ISBN:9781450346603
DOI:10.1145/3009837
General Chair:
Giuseppe Castagna
Paris Diderot University, France / CNRS, France
,
Program Chair:
Andrew D. Gordon
Microsoft Research, UK / University of Edinburgh, UK

Copyright © 2017 ACM.

Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than the author(s) must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected].

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 01 January 2017

Published in SIGPLAN Volume 52, Issue 1

Check for updates

Author Tags

Qualifiers

Research-article

Funding Sources

National Science Foundation

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

22
Total Citations
View Citations
1,268
Total Downloads

Downloads (Last 12 months)324
Downloads (Last 6 weeks)43

Reflects downloads up to 15 Feb 2025

Other Metrics

View Author Metrics

Citations

Cited By

Flatt MAllred TAngle NDe Gabrielle SFindler RFirth JGopinathan KGreenman BKasivajhula SKnauth AMcCarthy JPhillips SPorncharoenwase SSøgaard JTobin-Hochstadt S(2023)Rhombus: A New Spin on Macros without All the ParenthesesProceedings of the ACM on Programming Languages10.1145/36228187:OOPSLA2(574-603)Online publication date: 16-Oct-2023
https://dl.acm.org/doi/10.1145/3622818
Ballantyne MKing AFelleisen M(2020)Macros for domain-specific languagesProceedings of the ACM on Programming Languages10.1145/34282974:OOPSLA(1-29)Online publication date: 13-Nov-2020
https://doi.org/10.1145/3428297
CALDWELL SGARNOCK-JONES TFELLEISEN M(2020)Typed dataspace actorsJournal of Functional Programming10.1017/S095679682000024630Online publication date: 24-Aug-2020
https://doi.org/10.1017/S0956796820000246
Chang SBallantyne MTurner MBowman W(2019)Dependent type systems as macrosProceedings of the ACM on Programming Languages10.1145/33710714:POPL(1-29)Online publication date: 20-Dec-2019
https://doi.org/10.1145/3371071
Andersen LChang SFelleisen M(2017)Super 8 languages for making movies (functional pearl)Proceedings of the ACM on Programming Languages10.1145/31102741:ICFP(1-29)Online publication date: 29-Aug-2017
https://dl.acm.org/doi/10.1145/3110274
Lee YGopinathan KYang ZFlatt MSergey ILaemmel RPereira JMosses P(2024)DSLs in Racket: You Want It How, Now?Proceedings of the 17th ACM SIGPLAN International Conference on Software Language Engineering10.1145/3687997.3695645(84-103)Online publication date: 17-Oct-2024
https://dl.acm.org/doi/10.1145/3687997.3695645
Ballantyne MGamburg MHemann J(2024)Compiled, Extensible, Multi-language DSLs (Functional Pearl)Proceedings of the ACM on Programming Languages10.1145/36746278:ICFP(64-87)Online publication date: 15-Aug-2024
https://dl.acm.org/doi/10.1145/3674627
Gu QKe W(2024)Typing Requirement Model as CoroutinesIEEE Access10.1109/ACCESS.2024.335211512(8449-8460)Online publication date: 2024
https://doi.org/10.1109/ACCESS.2024.3352115
Flatt MAllred TAngle NDe Gabrielle SFindler RFirth JGopinathan KGreenman BKasivajhula SKnauth AMcCarthy JPhillips SPorncharoenwase SSøgaard JTobin-Hochstadt S(2023)Rhombus: A New Spin on Macros without All the ParenthesesProceedings of the ACM on Programming Languages10.1145/36228187:OOPSLA2(574-603)Online publication date: 16-Oct-2023
https://dl.acm.org/doi/10.1145/3622818
Cimini M(2021)A Calculus for Multi-language Operational SemanticsSoftware Verification10.1007/978-3-030-95561-8_3(25-42)Online publication date: 18-Jul-2021
https://dl.acm.org/doi/10.1007/978-3-030-95561-8_3
Show More Cited By

View Options

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

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

Figures

Tables

Media

View Issue’s Table of Contents