What is it about?

Software developers often need to search for and combine functions from different libraries when writing code. While most rely on general text-based search engines, a few specialized type-based tools exist for certain programming languages. The type-based approach allows searching for a function more precisely, on the basis of a formal specification of its input and output (i.e., its type). This paper introduces a new, largely language-independent type-based search method that applies concepts from logic and type theory to this problem. By making it easier to adopt for various programming languages, this approach could significantly broaden the availability of specialized search tools, saving developers time and effort.

Featured Image

Why is it important?

Our search method is language-independent, meaning it can be applied across various programming languages without the need to develop separate search engines for each one. This broad applicability significantly reduces the effort required to support type-based search for additional programming languages, and allows advances in search techniques for one language to benefit another. Additionally, by basing our approach on well-founded concepts from logic and type theory, we can be more confident of the quality of our results compared to heuristic-based methods. This ensures that developers can rely on more precise search results, improving their overall coding experience.

Perspectives

The theoretical foundation is solid, but the current implementation is not much more than a proof-of-concept. Although promising, more effort needs to be invested to improve the performance and user-experience of the tool. We currently also only have support for Java. However, with further improvements, this approach and its implementation certainly has potential, and I am looking forward to using it in my own day-to-day development - which was the driving motivation behind this research in the first place!

Marc Etter
OST - Eastern Switzerland University of Applied Sciences

For me, this work is a great example of how the deep link between programming and theorem proving, the Curry-Howard correspondence, a discovery held until now by many as an interesting, but largely theoretical curiosity, can be used to aid programmers in their everyday work. It reinforces my belief, that valuing systematic, principled approaches over heuristic ad-hoc ones leads to solutions that are more sound, scalable, and fun to use and develop. I thank Marc for taking this leap of faith, despite his initial doubts.

Prof. Dr. Farhad Mehta
OST Eastern Switzerland University of Applied Sciences

Read the Original

This page is a summary of: Towards Type-Directed API Search for Mainstream Languages, August 2024, ACM (Association for Computing Machinery),
DOI: 10.1145/3678000.3678207.
You can read the full text:

Read

Contributors

The following have contributed to this page