Dear Colleagues,
I am pleased to announce a new stable release of PAKCS, see
https://www.informatik.uni-kiel.de/~pakcs/download.html
It is a new major release (also part of upcoming
Debian und Ubuntu releases) with many small improvements
but two bigger changes:
1. A new structure of the standard base libraries:
Their structure is more closely with Haskell
(e.g., `List` is renamed to `Data.List`) and some
specialized libraries (Directory, FilePath, Time,...)
have been moved into separate packages. See the
release notes or the detailed migration guide at
https://git.ps.informatik.uni-kiel.de/curry/curry-libs/-/blob/master/Migrat…
2. Addition of class `Data` with operations `===` (equality)
and `aValue` (non-deterministic value generator).
This class solves some open problems w.r.t. logic programming.
The motivation for this class and its advantages are described in a
[DECLARE/WFLP'19 paper](https://doi.org/10.1007/978-3-030-46714-2_15).
A short discussion is also added below.
Most of the existing Curry packages have been made compatible
with this release, see
https://www-ps.informatik.uni-kiel.de/~cpm/
Comments and suggestions for improvements are welcome!
Best regards,
Michael
---
Some details about the new class `Data`:
The class `Data` provides a strict equality operation `===`. Why?
Look at the following "classical" functional logic definition of
computing the last element of a list:
last :: Eq a => [a] -> a
last xs | _ ++ [x] == xs = x where x free
Since `==` is part of the class `Eq`, it is defined on particular
types in instance declarations. If these definitions are different
from the standard `deriving` definitions, it might be possible
that `last` computes an element which is not identical to the
last element of the list. In Haskell, instances of `==` should be
an equivalence relation (rather than "equality", although this
is written in many papers and textbooks) so that `last` would
compute an element equivalent to the last element. This leads
to surprising results (see the "Data" paper for a deeper discussion).
These problems are avoided with class `Data`. For each
`data` declaration, `Data` instances for the defined type
are automatically derived as long as the type is first-order
(i.e., does not contain functional types). Hence it is ensured
that `===` denotes equality rather than equivalence. Thus,
last :: Data a => [a] -> a
last xs | _ ++ [x] === xs = x where x free
Moreover, free variable have type class constraint `Data` so that
they denote first-order values. From a declarative point of view,
a free value is equivalent to the non-deterministic value generator
`aValue` which is also defined in class `Data`, see
> pakcs
...
Prelude> aValue :: Maybe Bool
Nothing
Just False
Just True
This is the only real change with PAKCS 3.x: There are no
"polymorphic" free variables since a free variable has always
the class constraint `Data`.
---