agda2hs
agda2hs copied to clipboard
agda
Compiling Agda code to readable Haskell
When trying to bind to an existing datatype (like `Aeson.Value`, for example), I believe I should add a custom rewrite rule, like: ```yaml rewrites: - from: "Data.AesonBind.Value" to: "Value" importing:...
_Originally posted by @omelkonian in https://github.com/agda/agda2hs/pull/277#discussion_r1491144111_ ----- When we changed to RWS for our TC monad (in PR #277), we dropped support for GHC versions 8.6.5 and 9.02 because of...
We currently rely on `haskell-src-exts`. It doesn't support all modern Haskell syntax, is barely maintained and only offers a String pretty-printer. We may be interested in using this library instead:...
It can be found in `Haskell.Data.Map`. I've also added a mechanism to import `Haskell.Data.Something` modules as `Data.Something`.
This also depends on #297.
Useful when writing parsers, for example. It is in Haskell.Control.Applicative, as in Haskell, it can be found in Control.Applicative. But this also depends on the rewriting feature in #297.
It would be useful and relatively easy to add support for associated types to type classes. Here's an example: ```agda open import Haskell.Prelude record Collection (c : Set) : Set₁...
A sub-bug of #273 is that Agda is performing an η-reduction that creates a mismatch between what the user wrote and what the user gets on the Haskell side, e.g....
It would be good to have standard definitions of the type class laws for the classes in the Prelude, and prove them for the instances we provide. Here is an...
When defining a fancy version of an existing datatype (e.g. `All` as a fancy version of `List`), it would be nice to be able to mark it as the ornamented...