In this section, we sketch the ideas behind our analysis before we provide and explain the typing rules in detail. Finally, we show a few small examples to clarifiy how the analysis works.
From the last section we know that a nondeterministic computation can lead to an unexpected (and unwanted!) behaviour of the program if it appears in combination with monadic I/O. Therefore, we want to identify the functions that can cause such nondeterminism. As we have seen in the examples in Section 2, uninstantiated variables as arguments may cause nondeterministic steps when using narrowing. Hence, we propose a type and effect system that allows us to identify the form of arguments, i.e., if they are ground terms or not. This is not a trivial task because the arguments can be function calls which are evaluated lazily in Curry. Thus, the type of the arguments cannot be derived from their actual form but the analysis must take into account their reduction behaviour. We will collect the names of the functions that might split the computation as an effect of this computation.
In a first step, the program will be typed, either by hand or by a type
inferencer.
As a second step, we will analyse an expression with
respect to the program and receive a result like ``The expression reduces
deterministically'' or ``The reduction of the expression raises a
nondeterminism caused by the evaluation of the function