ICFP 2024
Mon 2 - Sat 7 September 2024 Milan, Italy
Fri 6 Sep 2024 16:22 - 16:45 at Orange 1 - Compilers and tooling

The Rust programming language offers a rich type system, including sum- and product types. Developer experience is often similar to that of a high-level functional programming language. Yet, it lacks a tool for interactively synthesizing programs based on types; a feature of many functional languages.

We devise a general term search algorithm, and integrate it with \texttt{rust-analyzer}, Rust’s official language server, making it usable from any client supporting standard LSP features. It suggests expressions for unfinished parts of a Rust program (as long as their type is known), or offers terms of matching type while typing via autocompletion. We develop the algorithm in three iterations. The first iteration is a backward search, inspired by Agsy, a similar tool for Agda proof assistant. The second iteration reverses the search direction, simplifying the caching of intermediate results. In the final iteration, we implement a tactic-based bidirectional search. This algorithm can synthesize terms in many more situations than the previous iterations, without a significant decrease in performance.

To evaluate the performance of our algorithm, we run it on 155 popular open-source Rust libraries. We delete parts of their source code, creating holes, and let the algorithm re-synthesize the missing code. We measure how many holes the algorithm can fill and how often it suggests the original code.

We have upstreamed our code, and term search is available as part of the official \texttt{rust-analyzer} distribution starting from v0.3.1850.

Fri 6 Sep

Displayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

16:00 - 17:30
Compilers and toolingTyDe at Orange 1

Session chair: Sandra Alves

16:00
22m
Talk
Typed, Concise, Nanopass (pick 3) (Extended Abstract)
TyDe
Lawrence Chonavel Utrecht University
File Attached
16:22
22m
Talk
Term Search in Rust
TyDe
Philipp Joram Tallinn University of Technology, Tavo Annus Tallinn University of Technology
16:45
22m
Talk
Towards Type-Directed API Search for Mainstream Languages
TyDe
Marc Etter OST Eastern Switzerland University of Applied Sciences, Farhad Mehta OST Eastern Switzerland University of Applied Sciences
17:07
22m
Meeting
TyDe closing
TyDe