Starting with KiCS2

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.

Start KiCS2

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:

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

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
Prelude> 2*3

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.

Free variables

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
Prelude> 2*3 == 42

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

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

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

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.

Search strategies

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

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.

Example: Regular expressions

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

However, depth-first search without any limit does not reach some words:

RegExp> :set dfs
RegExp> sem abcstar

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.

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
SearchTree RegExp> getAllValuesWith bfsStrategy (sem abcstar) >>= print . take 10
SearchTree RegExp> getAllValuesWith diagStrategy (sem abcstar) >>= print . take 10

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.