Changelog of @hackage/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 the Haskell. prefix will be dropped from the module name.

Additions to the agda2hs Prelude:

  • The builtin sort Set has been renamed to Type in the agda2hs Prelude
  • The Rezz type defined in Haskell.Extra.Erase has been renamed to Singleton.
  • The bindings to the Haskell base library are now located under lib/base to allow for adding bindings to other Haskell libraries.
  • Added new module Haskell.Control.Exception with the assert 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 with fromMaybe and other functions.
  • Added new module Haskell.Data.List with functions nub, deleteAll, and sort together with some of their properties.
  • Added new modules Haskell.Data.Map and Haskell.Data.Set from the containers package, together with a number of their properties. These libraries are part of the new containers package located in lib/containers.
  • Added properties of boolean values and operations under Haskell.Law.Bool.
  • Added laws for the Num type class and its instances under Haskell.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.