Can The Language Server Protocol Handle Dependent Types?

Master thesis (2024)

Authors

W.L. Stuijt Giacaman Electrical Engineering, Mathematics and Computer Science

Contributors

J.G.H. Cockx Programming Languages - EEMCS (mentor)
D.A.A. Pelsmaeker Programming Languages - EEMCS (graduation committee member)
S. Proksch Software Engineering - EEMCS (graduation committee member)
Faculty
Electrical Engineering, Mathematics and Computer Science, Electrical Engineering, Mathematics and Computer Science
More Info
expand_more

Published Date

26-06-2024

Language

English

Reuse Rights

Other than for strictly personal use, it is not permitted to download, forward or distribute the text or part of it, without the consent of the author(s) and/or copyright holder(s), unless the work is under an open content license such as Creative Commons.

Faculty

Electrical Engineering, Mathematics and Computer Science

Abstract

The Language Server Protocol (LSP) is a protocol that standardizes the way Integrated Development Environments (IDEs) and text editors communicate with language servers to provide language-specific features like autocompletion, go-to-definition, and diagnostics. While LSP has been widely adopted by mainstream programming languages, its adoption in dependently typed languages has been slower due to the unique challenges posed by their complex type systems and interactive theorem proving capabilities. This thesis explores the potential of LSP for enhancing the development of dependently typed programs, focusing on the Agda programming language. We present the implementation of a prototype LSP server for Agda that leverages scope checking to provide fast and responsive IDE features. We evaluate the performance of the prototype and compare its feature completeness with existing Agda development tools. Our findings demonstrate that scope checking can serve as a foundation for implementing efficient LSP features in Agda, offering a promising direction for improving the tooling and overall development experience for dependently typed languages.

Files

Document.pdf
(pdf | 0.296 Mb)