Reasonable Agda Is Correct Haskell: Writing Verified Haskell using agda2hs

Modern dependently typed languages such as Agda can be used to statically enforce the correctness of programs. However, they still lack the large ecosystem of a more popular language like Haskell. To combine the strength of both approaches, we present agda2hs, a tool that translates an expressive subset of Agda to readable Haskell, erasing dependent types and proofs in the process. Thanks to Agda’s support for erasure annotations, this process is both safe and transparent to the user. Compared to other tools for program extraction, agda2hs uses a syntax that is already familiar to functional programmers, allows for both intrinsic and extrinsic approaches to verification, and produces Haskell code that is easy to read and audit by programmers with no knowledge of Agda.

We present a practical use case of agda2hs at IOG to verify properties of a program generator. While both agda2hs and its ecosystem are still young, our experiences so far show that this is a viable approach to make verified functional programming available to a broader audience.

This paper is a literate Agda script, hence all rendered (Agda) code has been typechecked.