[HATRA'25] Imperative Syntax for Dependent Types

Описание: Imperative Syntax for Dependent Types (Video, HATRA 2025)
Bhakti Shah, and Edwin Brady
(University of St. Andrews; University of St. Andrews)

Abstract: The average programming language researcher holds the opinion that syntax is the least important part of a programming language. The average programmer disagrees. The syntax of a functional, dependently typed programming language differs significantly from that of a typical imperative language. As a part of our goal to develop a dependent type theory and programming language tailored to imperative programmers, we wish to explore the impact of syntax on comprehensibility and usability of a dependently typed language, specifically for experienced imperative programmers. To this end, we develop a prototypical imperative syntax that can be transformed into an existing dependently typed language, Idris. We develop several transformation algorithms to take imperative constructs such as loops and statements from this syntax to terms that typecheck in Idris, allowing programs to be executed within Idris’s ecosystem. We also develop an algorithm to automatically derive decidable equality instances for custom types, enabling dependent elimination with no additional effort from the programmer. As future work, we aim to conduct a formal user study to evaluate the effectiveness of this syntax for our purposes.


Presentation at the HATRA 2025 workshop, Oct 14, 2025, https://conf.researchr.org/home/icfp-...
Sponsored by ACM SIGPLAN.