Reference. Statically Contextualizing Large Language Models with Typed Holes
Large language models (LLMs) have reshaped the landscape of program synthesis. However, contemporary LLM-based code completion systems often hallucinate broken code because they lack appropriate code context, particularly when working with definitions that are neither in the training data nor near the cursor. This paper demonstrates that tighter integration with the type and binding structure of the programming language in use, as exposed by its language server, can help address this contextualization problem in a token-efficient manner. In short, we contend that AIs need IDEs, too! In particular, we integrate LLM code generation into the Hazel live program sketching environment. The Hazel Language Server is able to identify the type and typing context of the hole that the programmer is filling, with Hazel’s total syntax and type error correction ensuring that a meaningful program sketch is available whenever the developer requests a completion. This allows the system to prompt the LLM with codebase-wide contextual information that is not lexically local to the cursor, nor necessarily in the same file, but that is likely to be semantically local to the developer’s goal. Completions synthesized by the LLM are then iteratively refined via further dialog with the language server, which provides error localization and error messages. To evaluate these techniques, we introduce MVUBench, a dataset of model-view-update (MVU) web applications with accompanying unit tests that have been written from scratch to avoid data contamination, and that can easily be ported to new languages because they do not have large external library dependencies. These applications serve as challenge problems due to their extensive reliance on application-specific data structures. Through an ablation study, we examine the impact of contextualization with type definitions, function headers, and errors messages, individually and in combination. We find that contextualization with type definitions is particularly impactful. After introducing our ideas in the context of Hazel, a low-resource language, we duplicate our techniques and port MVUBench to TypeScript in order to validate the applicability of these methods to higher-resource mainstream languages. Finally, we outline ChatLSP, a conservative extension to the Language Server Protocol (LSP) that language servers can implement to expose capabilities that AI code completion systems of various designs can use to incorporate static context when generating prompts for an LLM.
Cite
Cites 87 works (7 here)
With notes (7)
Total Type Error Localization and Recovery with Holes zhao-2024-total
Type systems typically only define the conditions under which an expression is well-typed, leaving ill-typed expressions formally meaningless. This approach is insufficient as the basis for language servers driving modern programming environments, which are expected to recover from simultaneously localized errors and continue to provide a variety of downstream semantic services. This paper addresses this problem, contributing the first comprehensive formal account of total type error localization and recovery: the marked lambda calculus. In particular, we define a gradual type system for expressions with marked errors, which operate as non-empty holes, together with a total procedure for marking arbitrary unmarked expressions. We mechanize the metatheory of the marked lambda calculus in Agda and implement it, scaled up, as the new basis for Hazel, a full-scale live functional programming environment with, uniquely, no meaningless editor states. The marked lambda calculus is bidirectionally typed, so localization decisions are systematically predictable based on a local flow of typing information. Constraint-based type inference can bring more distant information to bear in discovering inconsistencies but this notoriously complicates error localization. We approach this problem by deploying constraint solving as a type-hole-filling layer atop this gradual bidirectionally typed core. Errors arising from inconsistent unification constraints are localized exclusively to type and expression holes, i.e., the system identifies unfillable holes using a system of traced provenances, rather than localized in an ad hoc manner to particular expressions. The user can then interactively shift these errors to particular downstream expressions by selecting from suggested partially consistent type hole fillings, which returns control back to the bidirectional system. We implement this type hole inference system in Hazel.
Gradual Structure Editing with Obligations moon-2023-gradual
Live Pattern Matching with Typed Holes yuan-2023-live
Several 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.
An Integrative Human-Centered Architecture for Interactive Programming Assistants blinn-2022-an
Program sketching with live bidirectional evaluation lubin-2020-program
We present a system called Smyth for program sketching in a typed functional language whereby the concrete evaluation of ordinary assertions gives rise to input-output examples, which are then used to guide the search to complete the holes. The key innovation, called live bidirectional evaluation, propagates examples “backward” through partially evaluated sketches. Live bidirectional evaluation enables Smyth to (a) synthesize recursive functions without trace-complete sets of examples and (b) specify and solve interdependent synthesis goals. Eliminating the trace-completeness requirement resolves a significant limitation faced by prior synthesis techniques when given partial specifications in the form of input-output examples. To assess the practical implications of our techniques, we ran several experiments on benchmarks used to evaluate Myth, a state-of-the-art example-based synthesis tool. First, given expert examples (and no partial implementations), we find that Smyth requires on average 66% of the number of expert examples required by Myth. Second, we find that Smyth is robust to randomly-generated examples, synthesizing many tasks with relatively few more random examples than those provided by an expert. Third, we create a suite of small sketching tasks by systematically employing a simple sketching strategy to the Myth benchmarks; we find that user-provided sketches in Smyth often further reduce the total specification burden (i.e. the combination of partial implementations and examples). Lastly, we find that Leon and Synquid, two state-of-the-art logic-based synthesis tools, fail to complete several tasks on which Smyth succeeds.
Live functional programming with typed holes omar-2019-live
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.
Hazelnut: a bidirectionally typed structure editor calculus omar-2017-hazelnut
External (80)
- Artifact for Statically Contextualizing Large Language Models with Typed Holes (2024)
- Towards Neural Synthesis for SMT-Assisted Proof-Oriented Programming (2024)
- CoCoMIC: Code Completion by Jointly Modeling In-file and Cross-file Context (2024)
- LongRoPE: Extending LLM Context Window Beyond 2 Million Tokens (2024)
- De-Hallucinator: Iterative Grounding for LLM-Based Code Completion (2024)
- LiveCodeBench: Holistic and Contamination Free Evaluation of Large Language Models for Code (2024)
- Same Task, More Tokens: the Impact of Input Length on the Reasoning Performance of Large Language Models (2024)
- LooGLE: Can Long-Context Language Models Understand Long Contexts? (2024)
- Enhancing LLM-Based Coding Tools through Native Integration of IDE-Derived Static Context (2024)
- STALL+: Boosting LLM-based Repository-level Code Completion with Static Analysis (2024)
- Lost in the Middle: How Language Models Use Long Contexts (2024)
- RepoBench: Benchmarking Repository-Level Code Auto-Completion Systems (2024)
- StarCoder 2 and The Stack v2: The Next Generation (2024)
- The Fact Selection Problem in LLM-Based Program Repair (2024)
- Context Composing for Full Line Code Completion (2024)
- RLCoder: Reinforcement Learning for Repository-Level Code Completion (2024)
- Knowledge Conflicts for LLMs: A Survey (2024)
- Hallucination is inevitable: An innate limitation of large language models (2024)
- PyDex: Repairing Bugs in Introductory Python Assignments using LLMs (2024)
- AutoCodeRover: Autonomous Program Improvement (2024)
- Measuring GitHub Copilot's Impact on Productivity (2024)
- Introducing the next generation of Claude (2024)
- How do you use personal data in model training? (Anthropic support article) (2024)
- Cursor Problems 2024 (Anysphere blog) (2024)
- Bing Image Creator from Designer Terms (2024)
- Hello GPT-4o (2024)
- OpenAI Platform Chat Completions (documentation) (2024)
- Introducing Zed AI (2024)
- Monitor-Guided Decoding of Code LMs with Static Analysis of Repository Context (2023)
- Grounded Copilot: How Programmers Interact with Code-Generating Models (2023)
- Knowledge Transfer from High-Resource to Low-Resource Programming Languages for Code LLMs (2023)
- CrossCodeEval: A Diverse and Multilingual Benchmark for Cross-File Code Completion (2023)
- What Makes Good In-Context Demonstrations for Code Intelligence Tasks with LLMs? (2023)
- Retrieval-Augmented Generation for Large Language Models: A Survey (2023)
- Better Context Makes Better Code Language Models: A Case Study on Function Call Argument Completion (2023)
- Is your code generated by ChatGPT really correct? Rigorous evaluation of large language models for code generation (2023)
- LLM is Like a Box of Chocolates: the Non-determinism of ChatGPT in Code Generation (2023)
- Examining Zero-Shot Vulnerability Repair with Large Language Models (2023)
- The Impact of AI on Developer Productivity: Evidence from GitHub Copilot (2023)
- Repository-level prompt generation for large language models of code (2023)
- Towards More Effective AI-Assisted Programming: A Systematic Design Exploration to Improve Visual Studio IntelliCode’s User Experience (2023)
- Copiloting the Copilots: Fusing Large Language Models with Completion Engines for Automated Program Repair (2023)
- Private-library-oriented code generation with large language models (2023)
- Siren’s song in the AI ocean: a survey on hallucination in large language models (2023)
- Repair Is Nearly Generation: Multilingual Program Repair with LLMs (2023)
- GPT-4 technical report (2023)
- Building a better repository map with tree sitter (Aider blog) (2023)
- Cody Context Architecture Whitepaper (2023)
- Editing support for software languages (2022)
- Training compute-optimal large language models (2022)
- Text and Code Embeddings by Contrastive Pre-Training (2022)
- Can OpenAI's codex fix bugs? (2022)
- Expectation vs. Experience: Evaluating the Usability of Code Generation Tools Powered by Large Language Models (2022)
- A systematic evaluation of large language models of code (2022)
- Emergent abilities of large language models (2022)
- Elm Architecture (Elm guide) (2022)
- The Hole Story: Type-Driven Synthesis and Repair (Licentiate thesis) (2022)
- Evaluating Large Language Models Trained on Code (2021)
- Codetrek: Flexible modeling of code using an extensible relational representation (2021)
- Program Synthesis with Large Language Models (2021)
- Introducing GitHub Copilot: your AI pair programmer (2021)
- Retrieval-augmented generation for knowledge-intensive NLP tasks (2020)
- Pragmatic MVU With React And TypeScript (2020)
- Language models are unsupervised multitask learners (2019)
- Type holes in TypeScript (2019)
- Merlin: a language server for OCaml (experience report) (2018)
- Toward Semantic Foundations for Program Editors (2017)
- Practical Foundations for Programming Languages (2nd ed.) (2016)
- On the naturalness of software (2016)
- OverCode (2015)
- Type-and-Example-Directed Program Synthesis (2015)
- Refined Criteria for Gradual Typing (2015)
- Defects4J: a database of existing faults to enable controlled testing studies for Java programs (2014)
- Contextual modal type theory (2008)
- Types and Programming Languages (2002)
- Photograph of World's First Computer, the Electronic Numerical Integrator and Calculator (1948)
- 10.18653/v1/2023.emnlp-main.308
- 10.18653/v1/2022.acl-long.431
- 10.18653/v1/2023.findings-emnlp.722
- 10.18653/v1/2023.emnlp-main.151