The Agda UHC Backend

Abstract

This thesis studies how we can facilitate combined Haskell/Agda developments. As foundation for our research we have created the Agda UHC backend, targeting the intermediate Core language of the Utrecht Haskell Compiler. We will present a formal description of our translation scheme, which now powers all major Agda backends. Building upon our new backend, we introduce a Contract framework specifically aimed at the Foreign Function Interface (FFI). As with most FFI implementations, a major challenge are the different type systems of the languages involved. Our contract library provides a concise and powerful way to translate data between Agda foreign languages like Haskell. We also provide a formal specification of our contract framework, making it feasible to implement a similar scheme in other languages. Furthermore, we provide an improved Agda FFI interface for function calls which combines well with our Contract framework. Our contributions make Agda a more viable choice for applied dependently-typed programming and provide an elegant and novel solution for the FFI problem in a dependently typed setting.