Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

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

Viktor Csimma

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.

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

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.
Paper Structure (21 sections, 2 figures)

This paper contains 21 sections, 2 figures.

Table of Contents

  1. Introduction
  2. Contributions
  3. Motivation
  4. Modelling Haskell libraries
  5. Background calculations
  6. Ease of compilation
  7. Ease of installation
  8. Demonstration of viability
  9. Necessary pre-knowledge
  10. Background -- Agda and agda2hs
  11. Repositories and self-references
  12. The MVVM-based methodology proposed
  13. EvenCounter
  14. Verified code
  15. Backend
  16. ...and 6 more sections

Figures (2)

  • Figure 1: Screenshots of EvenCounter.
  • Figure 2: Screenshots of AcornCalc.