Cyrus Omar
Ian Voysey
Ravi Chugh
Skip Abstract Section
Skip Supplemental Material SectionAbstract
Live programming environments aim to provide programmers (and sometimes audiences) with continuous feedback about a program's dynamic behavior as it is being edited. The problem is that programming languages typically assign dynamic meaning only to programs that are complete, i.e. syntactically well-formed and free of type errors. Consequently, live feedback presented to the programmer exhibits temporal or perceptive gaps.
This paper confronts this "gap problem" from type-theoretic first principles by developing a dynamic semantics for incomplete functional programs, starting from the static semantics for incomplete functional programs developed in recent work on Hazelnut. We model incomplete functional programs as expressions with holes, with empty holes standing for missing expressions or types, and non-empty holes operating as membranes around static and dynamic type inconsistencies. Rather than aborting when evaluation encounters any of these holes as in some existing systems, evaluation proceeds around holes, tracking the closure around each hole instance as it flows through the remainder of the program. Editor services can use the information in these hole closures to help the programmer develop and confirm their mental model of the behavior of the complete portions of the program as they decide how to fill the remaining holes. Hole closures also enable a fill-and-resume operation that avoids the need to restart evaluation after edits that amount to hole filling. Formally, the semantics borrows machinery from both gradual type theory (which supplies the basis for handling unfilled type holes) and contextual modal type theory (which supplies a logical basis for hole closures), combining these and developing additional machinery necessary to continue evaluation past holes while maintaining type safety. We have mechanized the metatheory of the core calculus, called Hazelnut Live, using the Agda proof assistant.
We have also implemented these ideas into the Hazel programming environment. The implementation inserts holes automatically, following the Hazelnut edit action calculus, to guarantee that every editor state has some (possibly incomplete) type. Taken together with this paper's type safety property, the result is a proof-of-concept live programming environment where rich dynamic feedback is truly available without gaps, i.e. for every reachable editor state.
Supplemental Material
- Martín Abadi, Luca Cardelli, Pierre-Louis Curien, and Jean-Jacques Lévy. 1991. Explicit Substitutions. J. Funct. Program. 1, 4 (1991), 375–416.Google Scholar
Cross Ref
- Andreas Abel and Brigitte Pientka. 2010. Explicit Substitutions for Contextual Type Theory. In International Workshop on Logical Frameworks and Meta-languages: Theory and Practice (LFMTP).Google Scholar
- Samson Abramsky. 1990. The lazy lambda calculus. In Research Topics in Functional Programming. Addison-Wesley Longman Publishing Co., Inc., 65–116. http://moscova.inria.fr/~levy/courses/X/M1/lambda/bib/90abramskylazy.pdf Google ScholarDigital Library
- Mehrdad Afshari, Earl T. Barr, and Zhendong Su. 2012. Liberating the programmer with prorogued programming. In Symposium on New Ideas in Programming and Reflections on Software (Onward!). Google ScholarDigital Library
- Alfred V. Aho and Thomas G. Peterson. 1972. A Minimum Distance Error-Correcting Parser for Context-Free Languages. SIAM J. Comput. 1, 4 (1972), 305–312.Google ScholarDigital Library
- Luís Eduardo de Souza Amorim, Sebastian Erdweg, Guido Wachsmuth, and Eelco Visser. 2016. Principled Syntactic Code Completion Using Placeholders. In International Conference on Software Language Engineering (SLE). Google ScholarDigital Library
- Dimitar Asenov and Peter Müller. 2014. Envision: A fast and flexible visual code editor with fluid interactions (Overview). In IEEE Symposium on Visual Languages and Human-Centric Computing (VL/HCC).Google ScholarCross Ref
- Steve Awodey, Nicola Gambino, and Kristina Sojakova. 2012. Inductive types in homotopy type theory. In Symposium on Logic in Computer Science (LICS). Google ScholarDigital Library
- Brian E Aydemir, Aaron Bohannon, Matthew Fairbairn, J Nathan Foster, Benjamin C Pierce, Peter Sewell, Dimitrios Vytiniotis, Geoffrey Washburn, Stephanie Weirich, and Steve Zdancewic. 2005. Mechanized metatheory for the masses: the POPLMark challenge. In International Conference on Theorem Proving in Higher Order Logics. Springer, 50–65. Google ScholarDigital Library
- Roberto Baldoni, Emilio Coppa, Daniele Cono D’Elia, Camil Demetrescu, and Irene Finocchi. 2018. A Survey of Symbolic Execution Techniques. ACM Comput. Surv. 51, 3, Article 50 (2018). Google ScholarDigital Library
- H.P. Barendregt. 1984. The Lambda Calculus. Studies in Logic, Vol. 103. Elsevier.Google Scholar
- Michael Bayne, Richard Cook, and Michael D. Ernst. 2011. Always-available Static and Dynamic Feedback. In International Conference on Software Engineering (ICSE). Google ScholarDigital Library
- Tomasz Blanc, Jean-Jacques Lévy, and Luc Maranget. 2005. Sharing in the Weak Lambda-Calculus. In Processes, Terms and Cycles: Steps on the Road to Infinity, Essays Dedicated to Jan Willem Klop, on the Occasion of His 60th Birthday (Lecture Notes in Computer Science), Vol. 3838. Springer, 70–87. Google ScholarDigital Library
- Maximilian C. Bolingbroke and Simon L. Peyton Jones. 2010. Supercompilation by evaluation. In Symposium on Haskell. Google ScholarDigital Library
- Edwin Brady. 2013. Idris, A General-Purpose Dependently Typed Programming Language: Design and Implementation. Journal of Functional Programming 23, 05 (2013), 552–593.Google ScholarCross Ref
- Sebastian Burckhardt, Manuel Fähndrich, Peli de Halleux, Sean McDirmid, Michal Moskal, Nikolai Tillmann, and Jun Kato. 2013. It’s Alive! Continuous Feedback in UI Programming. In Programming Language Design and Implementation (PLDI). Google ScholarDigital Library
- Margaret M. Burnett, John W. Atwood Jr., and Zachary T. Welch. 1998. Implementing Level 4 Liveness in Declarative Visual Programming Languages. In IEEE Symposium on Visual Languages. Google ScholarDigital Library
- Philippe Charles. 1991. A Practical Method for Constructing Efficient LALR(k) Parsers with Automatic Error Recovery. Ph.D. Dissertation. New York, NY, USA. Google ScholarDigital Library
- Sheng Chen and Martin Erwig. 2014. Counter-Factual Typing for Debugging Type Errors. In Principles of Programming Languages (POPL). Google ScholarDigital Library
- Sheng Chen and Martin Erwig. 2018. Systematic identification and communication of type errors. J. Funct. Program. 28 (2018).Google Scholar
- Adam Chlipala, Leaf Petersen, and Robert Harper. 2005. Strict bidirectional type checking. In International Workshop on Types in Language Design and Implementation (TLDI). Google ScholarDigital Library
- David Raymond Christiansen. 2013. Bidirectional Typing Rules: A Tutorial. http://davidchristiansen.dk/tutorials/bidirectional. pdf .Google Scholar
- Ravi Chugh, Brian Hempel, Mitchell Spradlin, and Jacob Albers. 2016. Programmatic and Direct Manipulation, Together at Last. In Programming Language Design and Implementation (PLDI). Google ScholarDigital Library
- Matteo Cimini and Jeremy G. Siek. 2016. The gradualizer: a methodology and algorithm for generating gradual type systems. In Principles of Programming Languages (POPL). Google ScholarDigital Library
- Pierre-Louis Curien. 1991. An Abstract Framework for Environment Machines. Theor. Comput. Sci. 82, 2 (1991), 389–402. Google ScholarDigital Library
- Evan Czaplicki. 2012. Elm: Concurrent FRP for Functional GUIs. Senior thesis, Harvard University (2012).Google Scholar
- Evan Czaplicki. 2018. An Introduction to Elm. (2018). https://guide.elm-lang.org/ . Retrieved Apr. 7, 2018.Google Scholar
- Curtis D’Alves, Tanya Bouman, Christopher Schankula, Jenell Hogg, Levin Noronha, Emily Horsman, Rumsha Siddiqui, and Christopher Kumar Anand. 2017. Using Elm to Introduce Algebraic Thinking to K-8 Students. In International Workshop on Trends in Functional Programming in Education (TFPIE).Google Scholar
- Luis Damas and Robin Milner. 1982. Principal type-schemes for functional programs. In Principles of Programming Languages (POPL). Google ScholarDigital Library
- Rowan Davies and Frank Pfenning. 2001. A modal analysis of staged computation. J. ACM 48, 3 (2001), 555–604. Google ScholarDigital Library
- Philippe de Groote. 2002. On the Strong Normalisation of Intuitionistic Natural Deduction with Permutation-Conversions. Inf. Comput. 178, 2 (2002), 441–464.Google ScholarCross Ref
- Dominique Devriese, Marco Patrignani, and Frank Piessens. 2018. Parametricity versus the universal type. PACMPL 2, POPL (2018), 38:1–38:23. Google ScholarDigital Library
- Joshua Dunfield and Neelakantan R. Krishnaswami. 2013. Complete and easy bidirectional typechecking for higher-rank polymorphism. In International Conference on Functional Programming (ICFP). Google ScholarDigital Library
- Matthias Felleisen and Robert Hieb. 1992. The Revised Report on the Syntactic Theories of Sequential Control and State. Theor. Comput. Sci. 103, 2 (1992), 235–271. Google ScholarDigital Library
- Francisco Ferreira and Brigitte Pientka. 2014. Bidirectional Elaboration of Dependently Typed Programs. In Symposium on Principles and Practice of Declarative Programming (PPDP). Google ScholarDigital Library
- Sue Fitzgerald, Gary Lewandowski, Renee McCauley, Laurie Murphy, Beth Simon, Lynda Thomas, and Carol Zander. 2008. Debugging: finding, fixing and flailing, a multi-institutional study of novice debuggers. Computer Science Education 18, 2 (2008), 93–116.Google ScholarCross Ref
- Flutter Developers. 2017. Technical Overview - Flutter. https://flutter.io/technical-overview/ . Retrieved Sep. 21, 2017.Google Scholar
- Jonathan Frankle, Peter-Michael Osera, David Walker, and Steve Zdancewic. 2016. Example-directed synthesis: a typetheoretic interpretation. In Principles of Programming Languages (POPL). Google ScholarDigital Library
- Ronald Garcia. 2013. Calculating Threesomes, With Blame. In International Conference on Functional Programming (ICFP). Google ScholarDigital Library
- Ronald Garcia and Matteo Cimini. 2015. Principal Type Schemes for Gradual Programs. In Principles of Programming Languages (POPL). Google ScholarDigital Library
- Herman Geuvers and Gueorgui I. Jojgov. 2002. Open Proofs and Open Terms: A Basis for Interactive Logic. In International Workshop on Computer Science Logic (CSL). Google ScholarDigital Library
- Adele Goldberg and David Robson. 1983. Smalltalk-80: the language and its implementation. Addison-Wesley Longman Publishing Co., Inc. Google ScholarDigital Library
- Susan L. Graham, Charles B. Haley, and William N. Joy. 1979. Practical LR Error Recovery. In Symposium on Compiler Construction (CC). Google ScholarDigital Library
- Philip J. Guo. 2013. Online Python tutor: embeddable web-based program visualization for CS education. In Technical Symposium on Computer Science Education (SIGCSE). Google ScholarDigital Library
- Matthew A. Hammer, Yit Phang Khoo, Michael Hicks, and Jeffrey S. Foster. 2014. Adapton: composable, demand-driven incremental computation. In Programming Language Design and Implementation (PLDI). Google ScholarDigital Library
- Robert Harper. 2016. Practical Foundations for Programming Languages (2nd ed.). Cambridge University Press. Google ScholarDigital Library
- Robert Harper and Christopher Stone. 2000. A Type-Theoretic Interpretation of Standard ML. In Proof, Language and Interaction: Essays in Honour of Robin Milner. MIT Press. Google ScholarDigital Library
- Christopher M. Hayden, Stephen Magill, Michael Hicks, Nate Foster, and Jeffrey S. Foster. 2012. Specifying and Verifying the Correctness of Dynamic Software Updates. In International Conference on Verified Software: Theories, Tools, Experiments (VSTTE). Google ScholarDigital Library
- Brian Hempel and Ravi Chugh. 2016. Semi-Automated SVG Programming via Direct Manipulation. In Symposium on User Interface Software and Technology (UIST). Google ScholarDigital Library
- David Herman, Aaron Tomb, and Cormac Flanagan. 2010. Space-efficient gradual typing. Higher-Order and Symbolic Computation 23, 2 (2010), 167. Google ScholarDigital Library
- Michael W. Hicks and Scott Nettles. 2005. Dynamic software updating. ACM Trans. Program. Lang. Syst. 27, 6 (2005), 1049–1096. Google ScholarDigital Library
- Catalin Hritcu, Michael Greenberg, Ben Karel, Benjamin C. Pierce, and Greg Morrisett. 2013. All Your IFCException Are Belong to Us. In IEEE Symposium on Security and Privacy. IEEE Computer Society, 3–17. Google ScholarDigital Library
- Yuu Igarashi, Taro Sekiyama, and Atsushi Igarashi. 2017. On Polymorphic Gradual Typing. Proc. ACM Program. Lang. 1, ICFP, Article 40 (Aug. 2017), 29 pages. Google ScholarDigital Library
- Mike Jones. 2017. Edit Code and Continue Debugging in Visual Studio (C#, VB, C++). https://docs.microsoft.com/en-us/ visualstudio/debugger/edit-and-continue . Retrieved Apr. 27, 2018.Google Scholar
- Neil D. Jones, Carsten K. Gomard, and Peter Sestoft. 1993. Partial evaluation and automatic program generation. Prentice-Hall, Inc. Google ScholarDigital Library
- Gilles Kahn and David B. MacQueen. 1977. Coroutines and Networks of Parallel Processes. In IFIP Congress. 993–998.Google Scholar
- Lennart C. L. Kats, Maartje de Jonge, Emma Nilsson-Nyman, and Eelco Visser. 2009. Providing rapid feedback in generated modular language environments: adding error recovery to scannerless generalized-LR parsing. In Conference on ObjectOriented Programming, Systems, Languages, and Applications (OOPSLA). Google ScholarDigital Library
- James C. King. 1976. Symbolic Execution and Program Testing. Commun. ACM 19, 7 (July 1976), 385–394. Google ScholarDigital Library
- Joomy Korkut and David Thrane Christiansen. 2018. Extensible Type-Directed Editing. In International Workshop on Type-Driven Development (TyDe). Google ScholarDigital Library
- Nico Lehmann and Éric Tanter. 2017. Gradual refinement types. In Principles of Programming Languages (POPL). http: //dl.acm.org/citation.cfm?id=3009856 Google ScholarDigital Library
- Benjamin Lerner, Dan Grossman, and Craig Chambers. 2006. Seminal: Searching for ML Type-error Messages. In Workshop on ML. Google ScholarDigital Library
- Jean-Jacques Lévy and Luc Maranget. 1999. Explicit substitutions and programming languages. In International Conference on Foundations of Software Technology and Theoretical Computer Science. Springer, 181–200. Google ScholarDigital Library
- Eyal Lotem and Yair Chuchem. 2016. Project Lamdu. http://www.lamdu.org/ . Accessed: 2016-04-08.Google Scholar
- Lena Magnusson. 1995. The implementation of ALF: a proof editor based on Martin-Löf’s monomorphic type theory with explicit substitution. Ph.D. Dissertation. Chalmers Institute of Technology.Google Scholar
- Conor McBride. 2000. Dependently typed functional programs and their proofs. Ph.D. Dissertation. University of Edinburgh, UK. http://hdl.handle.net/1842/374Google Scholar
- Renee McCauley, Sue Fitzgerald, Gary Lewandowski, Laurie Murphy, Beth Simon, Lynda Thomas, and Carol Zander. 2008. Debugging: a review of the literature from an educational perspective. Computer Science Education 18, 2 (2008), 67–92.Google ScholarCross Ref
- Sean McDirmid. 2007. Living It Up with a Live Programming Language. In Conference on Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA). Google ScholarDigital Library
- Aleksandar Nanevski, Frank Pfenning, and Brigitte Pientka. 2008. Contextual modal type theory. ACM Trans. Comput. Log. 9, 3 (2008). Google ScholarDigital Library
- Greg L. Nelson, Benjamin Xie, and Andrew J. Ko. 2017. Comprehension First: Evaluating a Novel Pedagogy and Tutoring System for Program Tracing in CS1. In Conference on International Computing Education Research (ICER). Google ScholarDigital Library
- Ulf Norell. 2007. Towards a practical programming language based on dependent type theory. Ph.D. Dissertation. Department of Computer Science and Engineering, Chalmers University of Technology, SE-412 96 Göteborg, Sweden.Google Scholar
- Ulf Norell. 2009. Dependently typed programming in Agda. In International Workshop on Types in Languages Design and Implementation (TLDI). Google ScholarDigital Library
- Martin Odersky, Christoph Zenger, and Matthias Zenger. 2001. Colored local type inference. In Principles of Programming Languages (POPL). Google ScholarDigital Library
- Cyrus Omar, Ian Voysey, Ravi Chugh, and Matthew A. Hammer. 2018. Live Functional Programming with Typed Holes (Extended Version). ArXiv e-prints (Nov. 2018). https://arxiv.org/abs/1805.00155Google Scholar
- Cyrus Omar, Ian Voysey, Michael Hilton, Jonathan Aldrich, and Matthew A. Hammer. 2017a. Hazelnut: A Bidirectionally Typed Structure Editor Calculus. In Principles of Programming Languages (POPL). http://dl.acm.org/citation.cfm?id= 3009900 Google ScholarDigital Library
- Cyrus Omar, Ian Voysey, Michael Hilton, Joshua Sunshine, Claire Le Goues, Jonathan Aldrich, and Matthew A. Hammer. 2017b. Toward Semantic Foundations for Program Editors. In Summit on Advances in Programming Languages (SNAPL).Google Scholar
- Zvonimir Pavlinovic, Tim King, and Thomas Wies. 2015. Practical SMT-Based Type Error Localization. In International Conference on Functional Programming (ICFP). Google ScholarDigital Library
- Roly Perera, Umut A. Acar, James Cheney, and Paul Blain Levy. 2012. Functional programs that explain their work. In International Conference on Functional Programming (ICFP). Google ScholarDigital Library
- Fernando Pérez and Brian E. Granger. 2007. IPython: a System for Interactive Scientific Computing. Computing in Science and Engineering 9, 3 (May 2007), 21–29. http://ipython.org Google ScholarDigital Library
- Simon Peyton Jones, Sean Leather, and Thijs Alkemade. 2014. Language options — Glasgow Haskell Compiler 8.4.1 User’s Guide (Typed Holes). http://downloads.haskell.org/~ghc/latest/docs/html/users_guide/glasgow_exts.html . Retrieved Apr 16, 2018.Google Scholar
- Brigitte Pientka. 2010. Beluga: Programming with Dependent Types, Contextual Data, and Contexts. In International Symposium on Functional and Logic Programming (FLOPS). Google ScholarDigital Library
- Brigitte Pientka and Andrew Cave. 2015. Inductive Beluga: Programming Proofs. In International Conference on Automated Deduction.Google Scholar
- Brigitte Pientka and Joshua Dunfield. 2008. Programming with proofs and explicit contexts. In Conference on Principles and Practice of Declarative Programming (PPDP). Google ScholarDigital Library
- Benjamin C. Pierce. 2002. Types and Programming Languages. MIT Press. Google ScholarDigital Library
- Benjamin C. Pierce and David N. Turner. 2000. Local type inference. ACM Trans. Program. Lang. Syst. 22, 1 (2000), 1–44. Google ScholarDigital Library
- Gordon D. Plotkin. 2004. A structural approach to operational semantics. J. Log. Algebr. Program. 60-61 (2004), 17–139.Google Scholar
- Patrick Rein, Stefan Ramson, Jens Lincke, Robert Hirschfeld, and Tobias Pape. 2019. Exploratory and Live, Programming and Coding - A Literature Study Comparing Perspectives on Liveness. Programming Journal 3, 1 (2019).Google Scholar
- Mitchel Resnick, John Maloney, Andrés Monroy-Hernández, Natalie Rusk, Evelyn Eastmond, Karen Brennan, Amon Millner, Eric Rosenbaum, Jay Silver, Brian Silverman, and Yasmin Kafai. 2009. Scratch: Programming for All. Commun. ACM 52, 11 (Nov. 2009), 60–67. Google ScholarDigital Library
- Wilmer Ricciotti, Jan Stolarek, Roly Perera, and James Cheney. 2017. Imperative functional programs that explain their work. PACMPL 1, ICFP (2017). Google ScholarDigital Library
- Martin C. Rinard. 2012. Obtaining and reasoning about good enough software. In Design Automation Conference (DAC). Google ScholarDigital Library
- Eric L. Seidel, Ranjit Jhala, and Westley Weimer. 2016. Dynamic Witnesses for Static Type Errors (or, Ill-typed Programs Usually Go Wrong). In International Conference on Functional Programming (ICFP). Google ScholarDigital Library
- Jeremy G. Siek and Walid Taha. 2006. Gradual Typing for Functional Languages. In Scheme and Functional Programming Workshop. http://scheme2006.cs.uchicago.edu/13-siek.pdfGoogle Scholar
- Jeremy G. Siek and Walid Taha. 2007. Gradual Typing for Objects. In European Conference on Object-Oriented Programming (ECOOP). Google ScholarDigital Library
- Jeremy G. Siek, Michael M. Vitousek, Matteo Cimini, and John Tang Boyland. 2015a. Refined Criteria for Gradual Typing. In Summit on Advances in Programming Languages (SNAPL).Google Scholar
- Jeremy G. Siek, Michael M. Vitousek, Matteo Cimini, Sam Tobin-Hochstadt, and Ronald Garcia. 2015b. Monotonic References for Efficient Gradual Typing. In European Symposium on Programming (ESOP). Google ScholarDigital Library
- Jeremy G. Siek and Philip Wadler. 2010. Threesomes, With and Without Blame. In Principles of Programming Languages (POPL). Google ScholarDigital Library
- Armando Solar-Lezama. 2009. The Sketching Approach to Program Synthesis. In Asian Symposium on Programming Languages and Systems (APLAS). Google ScholarDigital Library
- Saurabh Srivastava, Sumit Gulwani, and Jeffrey S Foster. 2013. Template-based program verification and program synthesis. International Journal on Software Tools for Technology Transfer 15, 5-6 (2013), 497–518. Google ScholarDigital Library
- Gareth Paul Stoyle, Michael W. Hicks, Gavin M. Bierman, Peter Sewell, and Iulian Neamtiu. 2007. Mutatis Mutandis: Safe and predictable dynamic software updating. ACM Trans. Program. Lang. Syst. 29, 4 (2007), 22. Google ScholarDigital Library
- M. Strecker, M. Luther, and F. von Henke. 1998. Interactive and automated proof construction in type theory. In Automated Deduction — A Basis for Applications. Vol. I: Foundations. Kluwer Academic Publishers, Chapter 3: Interactive Theorem Proving.Google Scholar
- Matúš Sulír and Jaroslav Porubän. 2018. Augmenting Source Code Lines with Sample Variable Values. In Conference on Program Comprehension (ICPC). Google ScholarDigital Library
- Asumu Takikawa, Daniel Feltey, Earl Dean, Matthew Flatt, Robert Bruce Findler, Sam Tobin-Hochstadt, and Matthias Felleisen. 2015. Towards Practical Gradual Typing. In European Conference on Object-Oriented Programming (ECOOP).Google Scholar
- Steven L. Tanimoto. 1990. VIVA: A visual language for image processing. J. Vis. Lang. Comput. 1, 2 (1990), 127–139. Google ScholarDigital Library
- Steven L. Tanimoto. 2013. A perspective on the evolution of live programming. In International Workshop on Live Programming (LIVE). Google ScholarDigital Library
- Andrew P. Tolmach and Andrew W. Appel. 1995. A Debugger for Standard ML. J. Funct. Program. 5, 2 (1995), 155–200.Google ScholarCross Ref
- Christian Urban, Stefan Berghofer, and Michael Norrish. 2007. Barendregt’s Variable Convention in Rule Inductions. In Conference on Automated Deduction (CADE). Google ScholarDigital Library
- B Victor. 2012. Inventing on principle, Invited talk at the Canadian University Software Engineering Conference (CUSEC). http://worrydream.com/#!/InventingOnPrincipleGoogle Scholar
- Markus Voelter, Daniel Ratiu, Bernhard Schaetz, and Bernd Kolb. 2012. mbeddr: An Extensible C-based Programming Language and IDE for Embedded Systems. In SPLASH. Google ScholarDigital Library
- Markus Voelter, Janet Siegmund, Thorsten Berger, and Bernd Kolb. 2014. Towards User-Friendly Projectional Editors. In International Conference on Software Language Engineering (SLE).Google Scholar
- Dimitrios Vytiniotis, Simon L. Peyton Jones, and José Pedro Magalhães. 2012. Equality proofs and deferred type errors: a compiler pearl. In International Conference on Functional Programming (ICFP). Google ScholarDigital Library
- Philip Wadler and Robert Bruce Findler. 2009. Well-Typed Programs Can’t Be Blamed. In European Symposium on Programming (ESOP). Google ScholarDigital Library
- David Wakeling. 2007. Spreadsheet functional programming. J. Funct. Program. 17, 1 (2007), 131–143. Google ScholarDigital Library
- Gerald M Weinberg. 1971. The Psychology of Computer Programming. Van Nostrand Reinhold New York.Google ScholarDigital Library
- David Weintrop, Afsoon Afzal, Jean Salac, Patrick Francis, Boyang Li, David C. Shepherd, and Diana Franklin. 2018. Evaluating CoBlox: A Comparative Study of Robotics Programming Environments for Adult Novices. In Conference on Human Factors in Computing (CHI). Google ScholarDigital Library
- David Weintrop and Uri Wilensky. 2015. To block or not to block, that is the question: students’ perceptions of blocks-based programming. In International Conference on Interaction Design and Children (IDC). Google ScholarDigital Library
- John Whitington and Tom Ridge. 2017. Visualizing the Evaluation of Functional Programs for Debugging. In Symposium on Languages, Applications and Technologies (SLATE).Google Scholar
- Andrew K. Wright and Matthias Felleisen. 1994. A syntactic approach to type soundness. Information and Computation 115, 1 (1994), 38–94. Google ScholarDigital Library
- Ningning Xie, Xuan Bi, and Bruno C. d. S. Oliveira. 2018. Consistent Subtyping for All. In European Symposium on Programming (ESOP).Google Scholar
- Y. S. Yoon and B. A. Myers. 2014. A longitudinal study of programmers’ backtracking. In IEEE Symposium on Visual Languages and Human-Centric Computing (VL/HCC).Google Scholar
- Danfeng Zhang, Andrew C. Myers, Dimitrios Vytiniotis, and Simon L. Peyton Jones. 2017. SHErrLoc: A Static Holistic Error Locator. ACM Trans. Program. Lang. Syst. 39, 4 (2017), 18:1–18:47. Google ScholarDigital Library
- John Zhang, Anirudh Verma, Chinmay Sheth, Christopher W Schankula, Stephanie Koehl, Andrew Kelly, Yumna Irfan, and Christopher K Anand. 2018. Graphics Programming in Elm Develops Math Knowledge & Social Cohesion. In International Conference on Computer Science and Software Engineering (CASCON). Google ScholarDigital Library
Index Terms
- Live functional programming with typed holes
Recommendations
Hazelnut: a bidirectionally typed structure editor calculus
POPL '17: Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming LanguagesStructure editors allow programmers to edit the tree structure of a program directly. This can have cognitive benefits, particularly for novice and end-user programmers. It also simplifies matters for tool designers, because they do not need to contend ...
Filling typed holes with live GUIs
PLDI 2021: Proceedings of the 42nd ACM SIGPLAN International Conference on Programming Language Design and ImplementationText editing is powerful, but some types of expressions are more naturally represented and manipulated graphically. Examples include expressions that compute colors, music, animations, tabular data, plots, diagrams, and other domain-specific data ...
Hazelnut: a bidirectionally typed structure editor calculus
POPL '17Structure editors allow programmers to edit the tree structure of a program directly. This can have cognitive benefits, particularly for novice and end-user programmers. It also simplifies matters for tool designers, because they do not need to contend ...
Comments