Changelog for agda2hs-1.4
Release notes for agda2hs v1.4
Changes
Changes to agda2hs:
- Increased Agda base version to 2.8.
- Increased bounds to support GHC 9.12.2.
- agda2hs will now skip compilation of files that are up-to-date.
- Added support for multi-parameter type classes.
- Added support for quantified constraints.
- Agda record types that compile to a Haskell data type are now
required to have the
no-eta-equality
directive. - agda2hs will now assume that any modules under the
Haskell.
namespace are part of the trusted FFI with Haskell. Concretely, no code will be generated for these modules and theHaskell.
prefix will be dropped from the module name.
Additions to the agda2hs Prelude:
- The builtin sort
Set
has been renamed toType
in the agda2hs Prelude - The
Rezz
type defined inHaskell.Extra.Erase
has been renamed toSingleton
. - The bindings to the Haskell
base
library are now located underlib/base
to allow for adding bindings to other Haskell libraries. - Added new module
Haskell.Control.Exception
with theassert
function which can be used to assert any decidable property, with the decidability proof being compiled to a boolean check in Haskell. - Added new module
Haskell.Data.Maybe
withfromMaybe
and other functions. - Added new module
Haskell.Data.List
with functionsnub
,deleteAll
, andsort
together with some of their properties. - Added new modules
Haskell.Data.Map
andHaskell.Data.Set
from thecontainers
package, together with a number of their properties. These libraries are part of the newcontainers
package located inlib/containers
. - Added properties of boolean values and operations under
Haskell.Law.Bool
. - Added laws for the
Num
type class and its instances underHaskell.Law.Num
.
See https://github.com/agda/agda2hs/issues?q=milestone%3A1.4+is%3Apr for the full list of changes.
Fixed issues
See https://github.com/agda/agda2hs/issues?q=milestone%3A1.4+is%3Aissue for the full list of fixed issues.