Here is a short introduction to the Curry system KiCS2. This does not replace the detailed user manual but should only highlight some features of KiCS2, in particular, those which are different from other Curry systems. We assume some familiarity with functional and functional logic programming, e.g., as described in the short review on functional logic programming.
After downloading and installing KiCS2,
you can start it by typing kics2 in a terminal.
If everythings was correctly installed, you see something like
_ _ ____ ___ ___ ___ ( )/ )(_ _)/ __)/ __)(__ \ ) ( _)(_( (__ \__ \ / _/ (_)\_)(____)\___)(___/(____) Version 0.5.0 of 2016-01-12 (installed at Tue Jan 12 14:31:03 CET 2016) Type ":h" for help (contact: kics2@curry-lang.org) Prelude>
Similarly to other Curry systems, KiCS2 is an interactive
system with a top-level "read-eval-print" loop.
The prefix Prelude> indicates that the module
Prelude is already loaded and the system waits for input.
Thus, you can enter an expression which is evaluated by KiCS2
so that its value is finally shown:
Prelude> 2*20+2 [1 of 2] Analyzing Prelude ( /opt/kics2/lib/Prelude.curry, /opt/kics2/lib/.curry/kics2/Curry_Prelude.nda ) [2 of 2] Compiling Curry_Main_Goal ( Curry_Main_Goal.curry, .curry/kics2/Curry_Curry_Main_Goal.hs ) Evaluating expression: 2*20+2 42 Prelude>
Since the output of the compiler is not quite interesting,
we use the KiCS2 command :set v0
(KiCS2 commands always start with a colon) to set the
verbosity level to 0 so that no intermediate output is shown:
Prelude> :set v0 Prelude> 2*20+2 42 Prelude> 2*3 6
Note that you have to wait a little bit to see the result.
This is due to the fact that each top-level expression
is evaluated by putting it into a program and compile
the complete program with the KiCS2 and Haskell compiler.
If you want to see what's going on in more detail,
you might try the KiCS2 command :set v4.
In contrast to purely functional languages, it is reasonable in Curry that expressions have no value or also more than one value. For instance, the division operation does not yield a value if the divisor is zero, or the head (first element) of an empty list is undefined:
Prelude> div 1 0 ! Prelude> head [] !
The output ! shows that the main expression has no value.
Since Curry searches for different ways
to evaluate expressions or to satisfy constraints,
! indicates a failure of a computation branch
and not an exception.
An important feature of Curry are constraints which are checked
for satisfiability in order to apply some operation.
A simple kind of constraints are equations.
The (infix) operator == evaluates to True
if both sides have identical values, and it evaluates to False
if the values are different:
Prelude> 2*3 == 6 True Prelude> 2*3 == 42 False
The additional power induced by the search abilities of functional logic programming becomes obvious when we try to satisfy equations including free (logic, unbound) variables. In this case, KiCS2 searches for values for these variables in order to evaluate the expressions (note that free variables in top-level expressions must be explicitly declared, similarly to free variables in program rules):
Prelude> x*3 == 6 where x free
{x = (-_x2)} False
{x = 0} False
{x = 1} False
{x = 2} True
{x = (2 * _x3 + 1)} False
{x = (4 * _x4)} False
{x = 6} False
{x = (8 * _x5 + 2)} False
{x = (8 * _x5 + 6)} False
In this case, KiCS2 answers with the value bound to this variable
together with the computed value. As we can see, there are many
different values for the variable x (some of them, like
{x = (-_x2)}, are only partially specified).
However, only one of them ({x = 2}) yields the desired value
True.
In order to evaluate a Boolean expression only to True values,
which is usually of our interest,
we can wrap the expression with the operation solve:
Prelude> solve $ x*3 == 6 where x free
{x = 2} True
The prelude operation solve is simply defined as follows:
solve :: Bool -> Bool solve True = True
Hence, the evaluation of solve fails if the argument
has not the value True.
In general, one can use any number of free variables so that
more than one solution (i.e., variable binding) might be computed:
Prelude> solve $ x*y == 6 where x,y free
{x = -1, y = -6} True
{x = -2, y = -3} True
{x = 1, y = 6} True
{x = -6, y = -1} True
{x = -3, y = -2} True
{x = 2, y = 3} True
{x = 6, y = 1} True
{x = 3, y = 2} True
We can also combine several equations by the Boolean conjunction operator
&&:
Prelude> solve $ x*y == 6 && x+y == 5 where x,y free
{x = 2, y = 3} True
{x = 3, y = 2} True
Now the fun starts and we try to use KiCS2 to compute Pythagorean triples:
Prelude> solve $ x*x + y*y == z*z where x,y,z free
{x = -1, y = 0, z = -1} True
{x = 0, y = -1, z = -1} True
{x = 0, y = 0, z = 0} True
{x = -1, y = 0, z = 1} True
{x = 0, y = -1, z = 1} True
{x = 0, y = 1, z = -1} True
{x = 1, y = 0, z = -1} True
{x = -2, y = 0, z = -2} True
Control-C
Oops, here we get infinitely many solutions so that we stop
their enumeration by Control-C.
A more elegant way is to enumerate the solutions one by one on user request.
This can be done in KiCS2 by setting the "interactive" option:
Prelude> :set +interactive
Prelude> solve $ x*x + y*y == z*z where x,y,z free
{x = -1, y = 0, z = -1} True
More values? [Y(es)/n(o)/a(ll)] y
{x = 0, y = -1, z = -1} True
More values? [Y(es)/n(o)/a(ll)] y
{x = 0, y = 0, z = 0} True
More values? [Y(es)/n(o)/a(ll)] y
{x = -1, y = 0, z = 1} True
More values? [Y(es)/n(o)/a(ll)] n
Prelude>
However, these are not really Pythagorean triples since we missed the condition that all numbers must be positive. Hence, we add some inequations to restrict the number of desired solutions:
Prelude> solve $ x*x + y*y == z*z && 0<x && x<y && y<z where x,y,z free
{x = 3, y = 4, z = 5} True
More values? [Y(es)/n(o)/a(ll)] y
{x = 6, y = 8, z = 10} True
More values? [Y(es)/n(o)/a(ll)] y
{x = 5, y = 12, z = 13} True
More values? [Y(es)/n(o)/a(ll)] y
{x = 9, y = 12, z = 15} True
More values? [Y(es)/n(o)/a(ll)] y
{x = 12, y = 16, z = 20} True
More values? [Y(es)/n(o)/a(ll)] n
Prelude>
BTW, you have seen a feature of KiCS2 which is not standard in other Curry systems: the guessing of values for integer variables. This is done by an internal binary representation of numbers.
Note that a successful search, like in the Pythagorean triples, often requires a fair strategy to avoid getting stuck in infinite but unsuccessful parts of the search space. Therefore, KiCS2 uses (in constrast to other Curry or logic programming systems) breadth-first search as the default search strategy. However, KiCS2 is not limited to this strategy. KiCS2 offers various built-in search strategies (depth-first search, breadth-first search, iterative deepening search, parallel search) which can easily be selected by setting a KiCS2 option. For instance, we can select depth-first search and try to solve our previous constraint again:
Prelude> :set dfs Prelude> solve $ x*x + y*y == z*z && 0<x && x<y && y<z where x,y,z free Control-C
However, we don't get any result due to the unfairness of depth-first search. Thus, we have to interrupt the computation and we will see the effect of different search strategies with a different example.
Guessing integers is nice but often not practical since there are more efficient algorithms to solve arithmetic equations and inequations. However, Curry as well as KiCS2 is not limited to numbers so that one can define arbitrary algebraic data types and constraints over them. For example, consider the following data type to describe regular expressions over some alphabet (see also the complete Curry program for this example):
data RE a = Lit a
| Alt (RE a) (RE a)
| Conc (RE a) (RE a)
| Star (RE a)
Despite of the unusual syntax, this definition covers the
standard definition of regular expressions which consists
of some letter (Lit),
a choice between two regular expressions (Alt),
a concatenation of two regular expressions (Conc),
or zero or more repetitions of a regular expression (Star).
For instance, the regular expression a(b|c)*
can be defined as follows:
abcstar :: RE Char abcstar = Conc (Lit 'a') (Star (Alt (Lit 'b') (Lit 'c')))
The semantics of a regular expression is the set of a words
over the given alphabet.
Since Curry supports nondeterministic operations, i.e.,
operations that yield more than one value for some given input,
we prefer to define the semantics as a mapping of a regular
expression into all possible words denoted by this expression.
Using the nondeterministic choice operation ?,
we define the semantics operation in the following concise manner:
sem :: RE a -> [a] sem (Lit c) = [c] sem (Alt a b) = sem a ? sem b sem (Conc a b) = sem a ++ sem b sem (Star a) = [] ? sem (Conc a (Star a))
Hence, "a", "acb", or "accbcb"
are possible values of the expression sem abcstar.
In order to check whether a regular expression matches a given string,
we can define the following operation which demonstrates
the usage of equations in the condition of a rule:
match :: RE a -> [a] -> Bool match r s | sem r == s = True
A Unix grep like tool to check whether a substring described by a regular expression is contained in a string can be specified as follows:
grep :: RE a -> [a] -> Bool grep r s | _ ++ sem r ++ _ == s = True
Another operation on regular expressions is to check whether
all words of a given list belong to the semantics of the regular
expression. This can be easily defined by exploiting the
match operation (and the prelude operation all
which checks whether a given predicate is satisfied for all elements
of a list):
contains :: RE a -> [[a]] -> Bool contains r xs = all (match r) xs
In Curry, we can use this operation not only to check properties of a given regular expression, but we can also use the same operation to search for regular expressions describing some given words:
RegExp> contains re ["a","ab","abb"] where re free
{re = (Conc (Lit 'a') (Star (Lit 'b')))} True
...
It should be noted that no result would be computed with depth-first search. It is also interesting to see the influence of the search strategy to the enumeration of the semantics of regular expressions. The standard breadth-first search strategy enumerates all expected words:
RegExp> sem abcstar "a" "ab" "ac" "abb" "abc" "acb" "acc" "abbb" "abbc" "abcb"
However, depth-first search without any limit does not reach some words:
RegExp> :set dfs RegExp> sem abcstar "a" "ab" "abb" "abbb" "abbbb" "abbbbb" "abbbbbb"
In both cases, we had to stop the enumeration by typing Control-C. Another possibility to control the enumeration of nondeterministic results is encapsulated search.
KiCS2 offers possibilities to encapsulate nondeterministic computations
so that one can select some computed values inside a program.
For this purpose, there is a library
SearchTree
that defines a data type of search trees (to represent a search space)
and various strategies to traverse search trees,
like depth-first (dfsStrategy),
breadth-first (bfsStrategy), or
diagonalization (diagStrategy).
A programmer could also define other search strategies as tree traversals.
Furthermore, there are operations to map an expression
into its search tree so that one can select the values
in the tree w.r.t. some search strategy.
For instance,
getAllValuesWith :: Strategy a -> a -> IO [a]
computes the list of values for a given expression w.r.t. some search strategy. Hence, if we add this library, we can print a limited number of words described by our regular expression w.r.t. different search strategies:
RegExp> :add SearchTree SearchTree RegExp> getAllValuesWith dfsStrategy (sem abcstar) >>= print . take 10 ["a","ab","abb","abbb","abbbb","abbbbb","abbbbbb","abbbbbbb","abbbbbbbb","abbbbbbbbb"] SearchTree RegExp> getAllValuesWith bfsStrategy (sem abcstar) >>= print . take 10 ["a","ab","ac","abb","abc","acb","acc","abbb","abbc","abcb"] SearchTree RegExp> getAllValuesWith diagStrategy (sem abcstar) >>= print . take 10 ["a","ab","ac","abb","abc","abbb","acb","abbc","abbbb","acc"]
Using encapsulated search, one can compute values and, if its number is finite, select the smallest or best value according to some criterion.
An alternative to encapsulate search via search trees
are set functions
which have better semantical properties and
are also provided in KiCS2 via the library
SetFunctions.
In this generality, these features are not available in other Curry or logic programming systems. For instance, Prolog's findall computes all solutions via a fixed depth-first search strategy.