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-equalitydirective. - 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
Sethas been renamed toTypein the agda2hs Prelude - The
Rezztype defined inHaskell.Extra.Erasehas been renamed toSingleton. - The bindings to the Haskell
baselibrary are now located underlib/baseto allow for adding bindings to other Haskell libraries. - Added new module
Haskell.Control.Exceptionwith theassertfunction 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.MaybewithfromMaybeand other functions. - Added new module
Haskell.Data.Listwith functionsnub,deleteAll, andsorttogether with some of their properties. - Added new modules
Haskell.Data.MapandHaskell.Data.Setfrom thecontainerspackage, together with a number of their properties. These libraries are part of the newcontainerspackage located inlib/containers. - Added properties of boolean values and operations under
Haskell.Law.Bool. - Added laws for the
Numtype 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.