The Types and Effects

Type and effect systems can be seen as an extension of classical type systems known from functional languages (see [19] for a detailed description). The basic idea is to extend the type annotation for a function with an effect that may occur during the application of this function. For every expression a type and the effect of its reduction can be approximated. Type and effect systems provide for powerful analyses like exception analysis [21], side effect or communication analysis [19, 20]. They can be used to extend classical type systems but also work on any kind of type domain. For instance, they can be applied to imperative languages, too, if one takes the set of states as type domain [19].

Since in Curry nondeterminism is mostly caused by uninstantiated variables in arguments of functions that are evaluated by narrowing, we use a type system to distinguish between ground terms and any terms. Thus, we define the type expressions as follows:

G denotes a ground term, A denotes any term. Of course, a ground term is also any term, so we have subtyping [2], i.e., . just means that any term of type has also type . A common example for this is because every natural number is also an integer. For functions it is important to notice that covariance holds for the result type but contravariance for the argument types, i.e., iff . This is easy to understand if we think of smaller types as more precise information. The type is smaller than and it is more precise, because it provides information about a larger set of inputs. Thus, the larger the input type, the more precise the information, i.e., the smaller the function type. The opposite holds for the output type, i.e., is smaller than , because the information about the target set is more precise.

Our type system allows several types for one expression. For instance, for a function defined by  $$f x = x  the two types and are correct but not related by subtyping!

As an effect we want to collect the names of functions whose application can cause nondeterministic computations. Therefore, we define the effect by

where $F$ is the set of function symbols of a program $P$. The effect annotated for a function declaration must contain all function names that might reduce in a nondeterministic way during the application of this function. For instance, the type annotation for a function $f$ could be

if on the rhs of $f$ a call to the function $g$ causes nondeterminism, whereas $g$ splits the computation because it calls the function $h$ in its body which raises the nondeterminism.

The aim of our analysis is to calculate type judgements

for an expression $e$ with respect to a program $P$, where E is a type environment, i.e., a set of type annotations for function and constructor symbols from $P$ and for variables. means that the expression $e$ has type , and during the reduction of $e$ the effect may occur.

As is the case in most program analyses, we cannot compute precise information for all program parts but only approximations of the real program behaviour. In our case this means that the computed type might be to imprecise, e.g., A instead of G, and the effect might be too large, i.e., it might contain functions that will never raise a nondeterminism. This imprecision can be reduced by refining the type domain (which is future work).

For our approximations to be safe we must show that we find every function which can raise a nondeterminism, and that terms identified as ground by our analysis will reduce to ground terms indeed. We will formalize this at the end of Section 3.2.