agda2hs: Compiling Agda code to readable Haskell.
Produces verified and readable Haskell code by extracting it from a
(lightly annotated) Agda program.
The tool is implemented as an Agda backend, which means that agda2hs is a
fully functional Agda compiler.
[Skip to Readme]
Downloads
- agda2hs-1.1.tar.gz [browse] (Cabal source package)
- Package description (as included in the package)
Maintainer's Corner
For package maintainers and hackage trustees
Candidates
| Versions [RSS] | 1.0, 1.1, 1.2, 1.3, 1.4 |
|---|---|
| Change log | CHANGELOG.md |
| Dependencies | Agda (>=2.6.4 && <2.6.5), base (>=4.10 && <4.18), bytestring (>=0.11.5 && <0.12), containers (>=0.6 && <0.7), deepseq (>=1.4.4 && <1.5), directory (>=1.2.6.2 && <1.4), filepath (>=1.4.1.0 && <1.5), haskell-src-exts (>=1.23 && <1.25), mtl (>=2.2.2 && <2.3), process (>=1.6.3.0 && <1.7), syb (>=0.7.2 && <0.8), text (>=2.0.2 && <2.1), unordered-containers (>=0.2.19 && <0.3), yaml-light (>=0.1.4 && <2.0) [details] |
| License | BSD-3-Clause |
| Copyright | 2023 Ulf Norell, Jesper Cockx, Orestis Melkonian, Sára Juhošová, James Chapman, Lucas Escot, Henry Blanchette |
| Author | Ulf Norell, Jesper Cockx, Orestis Melkonian, Sára Juhošová, James Chapman, Lucas Escot, Henry Blanchette |
| Maintainer | jesper@sikanda.be |
| Category | Language, Compiler |
| Source repo | head: git clone https://github.com/agda/agda2hs.git |
| Uploaded | by jcockx at 2023-10-23T09:28:01Z |
| Distributions | NixOS:1.3 |
| Executables | agda2hs-mode, agda2hs |
| Downloads | 335 total (4 in the last 30 days) |
| Rating | 2.0 (votes: 1) [estimated by Bayesian average] |
| Your Rating | |
| Status | Docs not available [build log] Last success reported on 2023-10-23 [all 1 reports] |
Readme for agda2hs-1.1
[back to package description]
agda2hs
Agda2hs is a tool for producing verified and readable Haskell code by extracting it from a (lightly annotated) Agda program. For example, the following Agda program encodes well-formed binary search trees:
open import Haskell.Prelude
_≤_ : {{Ord a}} → a → a → Set
x ≤ y = (x <= y) ≡ True
data BST (a : Set) {{@0 _ : Ord a}} (@0 lower upper : a) : Set where
Leaf : (@0 pf : lower ≤ upper) → BST a lower upper
Node : (x : a) (l : BST a lower x) (r : BST a x upper) → BST a lower upper
{-# COMPILE AGDA2HS BST #-}
agda2hs translates this to the following Haskell datatype:
module BST where
data BST a = Leaf
| Node a (BST a) (BST a)
Objective
The goal of this project is not to translate arbitrary Agda code to Haskell. Rather it is to carve out a common sublanguage between Agda and Haskell, with a straightforward translation from the Agda side to the Haskell side. This lets you write your program in the Agda fragment, using full Agda to prove properties about it, and then translate it to nice looking readable Haskell code that you can show your Haskell colleagues without shame.
Documentation
Documentation can be viewed at https://agda.github.io/agda2hs. You can also find
examples in the test directory of this repository, in particular the file
Test.agda. The
documentation is a work in progress, so if you have been using agda2hs and want
to contribute in some way, adding documentation or examples would be very
welcome.
agda2hs was introduced in the Haskell Symposium '22 paper Reasonable Agda is Correct Haskell: Writing Verified Haskell using agda2hs.
Future work
Currently agda2hs is under active development, please take a look at the issue tracker. If you have a suggestion for a new feature that is not yet on the issue tracker, you are welcome to create a new issue or a PR. Feature requests should be of the form "Add support for Haskell feature X", not "Add support for Agda feature Y" (see "Objective" above). If you want to compile arbitrary Agda code to Haskell, you are advised to use Agda's built-in GHC backend instead.