More Web Proxy on the site http://driver.im/

research-article

Extensible type-directed editing

Authors:

David Thrane ChristiansenAuthors Info & Claims

TyDe 2018: Proceedings of the 3rd ACM SIGPLAN International Workshop on Type-Driven Development

Pages 38 - 50

https://doi.org/10.1145/3240719.3241791

Published: 27 September 2018 Publication History

Abstract

Dependently typed programming languages, such as Idris and Agda, feature rich interactive environments that use informative types to assist users with the construction of programs. However, these environments have been provided by the authors of the language, and users have not had an easy way to extend and customize them. We address this problem by extending Idris's metaprogramming facilities with primitives for describing new type-directed editing features, making Idris's editors as extensible as its elaborator.

References

[1]

2016. Changelog for Agda-2.5.1. http://hackage.haskell.org/package/ Agda-2.5.1/changelog . (16 April 2016). Accessed: 2018-05-19.

[2]

Thorsten Altenkirch and Conor McBride. 2003. Generic programming within dependently typed programming. In Generic Programming. Springer, 1–20.

Digital Library

[3]

Abhishek Anand, Simon Boulier, Cyril Cohen, Matthieu Sozeau, and Nicolas Tabareau. 2018. Typed Template Coq–Certified MetaProgramming in Coq. In The Fourth International Workshop on Coq for Programming Languages .

[4]

Lennart Augustsson. 2005. Announcing Djinn. http://permalink. gmane.org/gmane.comp.lang.haskell.general/12747 . (2005). Accessed: 2017-10-04.

[5]

Eli Barzilay. 2006. Implementing reflection in Nuprl. Ph.D. Dissertation. Cornell University.

Digital Library

[6]

William J Bowman. 2016. Growing a Proof Assistant. Higher-Order Programming with Effects .

[7]

Edwin Brady. 2013. Idris, a general-purpose dependently typed programming language: Design and implementation. Journal of Functional Programming 23, 5 (2013), 552–593.

[8]

David Christiansen and Edwin Brady. 2016. Elaborator reflection: extending Idris in Idris. In Proceedings of the 21st ACM SIGPLAN International Conference on Functional Programming . ACM.

Digital Library

[9]

David Raymond Christiansen. 2014. Type-Directed Elaboration of Quasiquotations: A High-Level Syntax for Low-Level Reflection. In Proceedings of the 26th 2014 International Symposium on Implementation and Application of Functional Languages . ACM, 1.

Digital Library

[10]

David Raymond Christiansen. 2016. Practical Reflection and Metaprogramming for Dependent Types . Ph.D. Dissertation. IT University of Copenhagen, Software and Systems Section.

[11]

Pierre-´Evariste Dagand, Nicolas Tabareau, and ´Eric Tanter. 2018. Foundations of dependent interoperability. Journal of Functional Programming 28 (2018), e9.

[12]

Leonardo de Moura, Soonho Kong, Jeremy Avigad, Floris Van Doorn, and Jakob von Raumer. 2015. The Lean theorem prover (system description). In International Conference on Automated Deduction. Springer, 378–388.

[13]

Roy Dyckhoff. 1992. Contraction-free sequent calculi for intuitionistic logic. The Journal of Symbolic Logic 57, 3 (1992), 795–807.

[14]

Gabriel Ebner, Sebastian Ullrich, Jared Roesch, Jeremy Avigad, and Leonardo de Moura. 2017. A metaprogramming framework for formal verification. Proceedings of the ACM on Programming Languages 1, ICFP, 34.

Digital Library

[15]

Matthias Felleisen, Robert Bruce Findler, Matthew Flatt, Shriram Krishnamurthi, Eli Barzilay, Jay McCarthy, and Sam Tobin-Hochstadt. 2015. The Racket manifesto. In LIPIcs-Leibniz International Proceedings in Informatics, Vol. 32. Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik.

[16]

Daniel Feltey, Spencer P Florence, Tim Knutson, Vincent St-Amour, Ryan Culpepper, Matthew Flatt, Robert Bruce Findler, and Matthias Felleisen. 2016. Languages the Racket Way. Language Workbench Challenge .

[17]

Matthew Flatt, Robert Bruce Findler, Shriram Krishnamurthi, and Matthias Felleisen. 1999. Programming Languages As Operating Systems (or Revenge of the Son of the Lisp Machine). In Proceedings of the Fourth ACM SIGPLAN International Conference on Functional Programming (ICFP ’99) . ACM, 138–147.

Digital Library

[18]

Daniel P. Friedman and David Thrane Christiansen. 2018. The Little Typer . MIT Press, Cambridge, MA, USA.

[19]

Adele Goldberg. 1984. Smalltalk-80: The Interactive Programming Environment . Addison Wesley.

Digital Library

[20]

Thomas Hallgren. 1998. The proof editor Alfa. http://www.cse. chalmers.se/hallgren/Alfa . (1998).

[21]

Robert Harper. 1997. Notes on Regular Expression Simplification. https: //www.cs.cmu.edu/ ∼ fp/courses/97-212/handouts/regsimp.pdf . (1997). Accessed: 2017-06-06.

[22]

Ralf Hinze and Ross Paterson. 2006. Finger trees: a simple generalpurpose data structure. Journal of functional programming 16, 2 (2006), 197–217.

Digital Library

[23]

Paul Hudak. 1996. Building Domain-specific Embedded Languages. Comput. Surveys 28, 4es, Article 196.

Digital Library

[24]

Wen Kokke and Wouter Swierstra. 2015. Auto in Agda. In International Conference on Mathematics of Program Construction . Springer, 276–301.

[25]

Joomy Korkut. 2018. Edit-Time Tactics in Idris. Master’s thesis. Wesleyan University, Middletown, CT, USA.

[26]

Fredrik Lindblad and Marcin Benke. 2004. A tool for automated theorem proving in Agda. In International Workshop on Types for Proofs and Programs . Springer, 154–169.

Digital Library

[27]

Lena Magnusson. 1994. The implementation of ALF - a proof editor based on Martin-L¨of’s monomorhic type theory with explicit substitution . Ph.D. Dissertation. Chalmers Tekniska H¨ogskolan.

[28]

Lena Magnusson and Bengt Nordstr¨om. 1993. The ALF proof editor and its proof engine. In International Workshop on Types for Proofs and Programs . Springer, 213–237.

Digital Library

[29]

Gregory Michael Malecha. 2014. Extensible Proof Engineering in Intensional Type Theory . Ph.D. Dissertation. Harvard University.

[30]

Conor McBride. 2000. Dependently typed functional programs and their proofs . Ph.D. Dissertation. University of Edinburgh. College of Science and Engineering. School of Informatics.

[31]

Conor McBride and James McKinna. 2004. The view from the left. Journal of functional programming 14, 1 (2004), 69–111.

Digital Library

[32]

Conor McBride and Ross Paterson. 2008. Applicative Programming with Effects. Journal of Functional Programming 18, 1 (2008), 1–13.

Digital Library

[33]

John McCarthy. 1960. Recursive functions of symbolic expressions and their computation by machine, Part I. Commun. ACM 3, 4 (1960), 184–195.

Digital Library

[34]

Cyrus Omar, Ian Voysey, Michael Hilton, Jonathan Aldrich, and Matthew A. Hammer. 2017. Hazelnut: A Bidirectionally Typed Structure Editor Calculus. In 44th ACM SIGPLAN Symposium on Principles of Programming Languages (POPL 2017) .

Digital Library

[35]

Cyrus Omar, Ian Voysey, Michael Hilton, Joshua Sunshine, Claire Le Goues, Jonathan Aldrich, and Matthew A. Hammer. 2017. Toward Semantic Foundations for Program Editors. In Summit on Advances in Programming Languages (SNAPL 2017) .

[36]

Alejandro AR Trejo Ortiz and Guillermo Fern´andez Anaya. 1998. Regular expression simplification. Mathematics and computers in simulation 45, 1-2 (1998), 59–71.

Digital Library

[37]

Robert Pollack. 1990. Implicit syntax. In Informal Proceedings of First Workshop on Logical Frameworks, Antibes, Vol. 4.

[38]

William Pugh. 1991. The Omega test: a fast and practical integer programming algorithm for dependence analysis. In Proceedings of the 1991 ACM/IEEE conference on Supercomputing . ACM, 4–13.

Digital Library

[39]

Tim Sheard and Simon Peyton Jones. 2002. Template metaprogramming for Haskell. In Proceedings of the 2002 ACM SIGPLAN workshop on Haskell . ACM, 1–16.

Digital Library

[40]

Guy L. Steele, Jr. and Richard P. Gabriel. 1993. The Evolution of Lisp. In The Second ACM SIGPLAN Conference on History of Programming Languages (HOPL-II) . ACM, New York, NY, USA, 231–270.

Digital Library

Cited By

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://dl.acm.org/doi/10.1145/3371071
Omar CVoysey IChugh RHammer M(2019)Live functional programming with typed holesProceedings of the ACM on Programming Languages10.1145/32903273:POPL(1-32)Online publication date: 2-Jan-2019
https://dl.acm.org/doi/10.1145/3290327

Index Terms

Extensible type-directed editing
1. Software and its engineering
  1. Software notations and tools
    1. General programming languages
      1. Language features
      2. Language types
        Functional languages

Recommendations

Type-Directed Elaboration of Quasiquotations: A High-Level Syntax for Low-Level Reflection
IFL '14: Proceedings of the 26nd 2014 International Symposium on Implementation and Application of Functional Languages

Idris's reflection features allow Idris metaprograms to manipulate a representation of Idris's core language as a datatype, but these reflected terms were designed for ease of type checking and are therefore exceedingly verbose and tedious to work with. ...
Ur: statically-typed metaprogramming with type-level record computation
PLDI '10: Proceedings of the 31st ACM SIGPLAN Conference on Programming Language Design and Implementation

Dependent types provide a strong foundation for specifying and verifying rich properties of programs through type-checking. The earliest implementations combined dependency, which allows types to mention program variables; with type-level computation, ...
Elaborator reflection: extending Idris in Idris
ICFP 2016: Proceedings of the 21st ACM SIGPLAN International Conference on Functional Programming

Many programming languages and proof assistants are defined by elaboration from a high-level language with a great deal of implicit information to a highly explicit core language. In many advanced languages, these elaboration facilities contain powerful ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Conferences

TyDe 2018: Proceedings of the 3rd ACM SIGPLAN International Workshop on Type-Driven Development

September 2018

90 pages

ISBN:9781450358255

DOI:10.1145/3240719

General Chairs:
Richard A. Eisenberg,
Niki Vazou

Copyright © 2018 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].

Sponsors

SIGPLAN: ACM Special Interest Group on Programming Languages

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 27 September 2018

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Research-article

Conference

ICFP '18

Sponsor:

SIGPLAN

ICFP '18: 23nd ACM SIGPLAN International Conference on Functional Programming

September 27, 2018

MO, St. Louis, USA

Upcoming Conference

ICFP '25

Sponsor:
sigplan

ACM SIGPLAN International Conference on Functional Programming

October 12 - 18, 2025

Singapore , Singapore

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

2
Total Citations
View Citations
109
Total Downloads

Downloads (Last 12 months)4
Downloads (Last 6 weeks)1

Reflects downloads up to 28 Dec 2024

Other Metrics

View Author Metrics

Citations

Cited By

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://dl.acm.org/doi/10.1145/3371071
Omar CVoysey IChugh RHammer M(2019)Live functional programming with typed holesProceedings of the ACM on Programming Languages10.1145/32903273:POPL(1-32)Online publication date: 2-Jan-2019
https://dl.acm.org/doi/10.1145/3290327

View Options

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

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Media

Figures

Other

Tables

View Table of Contents