Papers
2023
-
Live Pattern Matching with Typed HolesProc. ACM Program. Lang., 2023Several modern programming systems, including GHC Haskell, Agda, Idris, and Hazel, support typed holes. Assigning static and, to varying degree, dynamic meaning to programs with holes allows program editors and other tools to offer meaningful feedback and assistance throughout editing, i.e. in a live manner. Prior work, however, has considered only holes appearing in expressions and types. This paper considers, from type theoretic and logical first principles, the problem of typed pattern holes. We confront two main difficulties, (1) statically reasoning about exhaustiveness and irredundancy when patterns are not fully known, and (2) live evaluation of expressions containing both pattern and expression holes. In both cases, this requires reasoning conservatively about all possible hole fillings. We develop a typed lambda calculus, Peanut, where reasoning about exhaustiveness and redundancy is mapped to the problem of deriving first order entailments. We equip Peanut with an operational semantics in the style of Hazelnut Live that allows us to evaluate around holes in both expressions and patterns. We mechanize the metatheory of Peanut in Agda and formalize a procedure capable of deciding the necessary entailments. Finally, we scale up and implement these mechanisms within Hazel, a programming environment for a dialect of Elm that automatically inserts holes during editing to provide static and dynamic feedback to the programmer in a maximally live manner, i.e. for every possible editor state. Hazel is the first maximally live environment for a general-purpose functional language.
@article{10.1145/3586048, author = {Yuan, Yongwei and Guest, Scott and Griffis, Eric and Potter, Hannah and Moon, David and Omar, Cyrus}, title = {Live Pattern Matching with Typed Holes}, year = {2023}, publisher = {Association for Computing Machinery}, address = {New York, NY, USA}, volume = {7}, number = {OOPSLA1}, url = {https://doi.org/10.1145/3586048}, doi = {10.1145/3586048}, journal = {Proc. ACM Program. Lang.}, %month = {}, articleno = {96}, numpages = {27}, %keywords = {pattern matching, typed holes}, %demo = https://hazel.org/build/dev/, artifact = https://doi.org/10.5281/zenodo.7713722, }
2022
-
Contextualized Programming Language DocumentationIn Proceedings of the 2022 ACM SIGPLAN International Symposium on New Ideas, New Paradigms, and Reflections on Programming and Software, 2022Learning the syntax and semantics of a new programming language is a challenge. It is common for learners to refer to language documentation many times and in many contexts as they build comfort and understanding. We review existing functional language documentation, finding that it tends to be organized according to the structure of the language. Each section interleaves narrative explanations, which introduce precise terminology that is then used consistently, with code examples. Sections often start with simpler special cases of a construct before considering it in full generality. To make use of language documentation, learners must step away from the code they are working with, e.g., in an exercise or tutorial, to locate and transfer knowledge from the documentation. We describe a system, ExplainThis, that automatically generates contextualized language documentation, structured based on our study of language documentation but specialized to the particular code at the cursor. This system is integrated into the structure editor of Hazel, a live functional environment. Documentation appears next to the editor and color is used as secondary notation to correlate the explanation with program terms. We also study syntactic and explanatory specificity with a formative user study. We find that participants desire documentation to be tailored to specific syntax of the code a user is working with, while allowing an adaptive level of specificity for code examples.
@inproceedings{10.1145/3563835.3567654, author = {Potter, Hannah and Madadi, Ardi and Just, Ren\'{e} and Omar, Cyrus}, title = {Contextualized Programming Language Documentation}, year = {2022}, isbn = {9781450399098}, publisher = {Association for Computing Machinery}, address = {New York, NY, USA}, url = {https://doi.org/10.1145/3563835.3567654}, doi = {10.1145/3563835.3567654}, booktitle = {Proceedings of the 2022 ACM SIGPLAN International Symposium on New Ideas, New Paradigms, and Reflections on Programming and Software}, pages = {1–15}, numpages = {15}, keywords = {structure editing, programming education, functional programming, documentation}, location = {Auckland, New Zealand}, series = {Onward! 2022}, demo = https://hazel.org/build/explainthis/, artifact = https://doi.org/10.6084/m9.figshare.21381864, }
2020
-
Hazel Tutor: Guiding Novices Through Type-Driven Development StrategiesHannah Potter, and Cyrus Omar2020Hazel Tutor is a work-in-progress editor service for the Hazel programming environment designed to interactively help novices learn type-driven development strategies as they construct, edit, and debug code. The system provides both feedback and, when requested, suggestions on the basis of type information available at the cursor. Hazel is able to supply the Hazel Tutor with the necessary information at all times, including when there are holes in the program. When the cursor is on an empty hole, the system organizes the suggestions based on the type-driven development strategy that we aim to teach students. We are beginning to work on presenting debugging strategies when on an error hole. We outline our hypotheses, specific research questions of interest, and planned future studies.
@misc{hazeltutor, title = {Hazel Tutor: Guiding Novices Through Type-Driven Development Strategies}, author = {Potter, Hannah and Omar, Cyrus}, year = {2020}, }
