Adapting the MVVM pattern to C++ frontends and Agda-based backends

TL;DR

This paper introduces a comprehensive methodology for integrating Agda and Haskell in C++ frontends using MVVM architecture, enabling use of arbitrary Haskell libraries and improving development with automated tools and novel interruption handling.

Contribution

It presents a general, well-documented methodology for combining Agda and Haskell in C++ applications, including solutions for using arbitrary Haskell libraries and a new interruption mechanism.

Findings

Benchmarks show the agda2hs compiler is competitive with OCaml and MAlonzo backends.

The methodology allows seamless integration of Agda and Haskell in C++ frontends.

A novel Haskell future design supports arbitrary interruption via FFI.

Abstract

Using agda2hs and ad-hoc Haskell FFI bindings, writing Qt applications in C++ with Agda- or Haskell-based backends (possibly including correctness proofs) is already possible. However, there was no repeatable methodology to do so, nor to use \emph{arbitrary} Haskell built-in libraries in Agda code. We present a well-documented, general methodology to address this, applying the ideas of the Model-View-ViewModel architecture to models implemented in functional languages. This is augmented by a software development kit providing easy installation and automated compilation. For obstacles arising, we provide solutions and ideas that are novel contributions by themselves. We describe and compare solutions for using arbitrary Haskell built-ins in Agda code, highlighting their advantages and disadvantages. Also, for user interruption, we present a new Haskell future design that, to the best of our knowledge, is the first to provide for arbitrary interruption and the first to provide for interruption via direct FFI calls from C and C++. Finally, we prove with benchmarks that the agda2hs compiler at the base of our methodology is viable when compared to other solutions, specifically to the OCaml extraction feature of Rocq and the default MAlonzo backend of Agda.