The Typing Rules

 

  
Figure 1: Typing rules

Figure 1 shows the typing rules for our analysis, which define the type judgments .

The DECL rules define when a program rule $r$ is correctly typed w.r.t. a type annotation $TA$ (i.e., ): The type annotation $TA$ for the function $f$ must be given in the environment E, and with the according types for the arguments $x$_i added to the environment, the derived type for the right-hand side must match the type of $f$.

For the effect, two cases are distinguished: If the effect of the right-hand side is empty, the function application itself will not cause nondeterminism (only the arguments might do that, but this is caught by the APP rule). Therefore, we do not restrict the effect that is annotated at the type for $f$. Otherwise, if the right-hand side $e$ raises a nondeterministic computation step, $f$ will also reduce nondeterministically, so its effect must contain and $${f}. Note that may contain arbitrary function symbols from the program, because, due to subeffecting (see below), it is still a safe approximation to annotate a larger effect.

The VAR rule is common. If a type is given for $x$ in the environment, this type and an empty effect can be derived. Note that $x$ can be a variable, a function symbol, or a constructor symbol.

The NEWVAR rule handles local (existentially quantified) variables. The newly introduced variable $x$_fresh is uninstantiated, and thus must be given the type A for analysing $e$. By $$e[x/t] we denote the replacement of all free occurrences of $x$ in $e$ by $t$. An occurence of a variable $x$ in $e$ is free if it does not occur inside a subterm $e\text{'}$ of $e$ with $e\text{'}=$  $$let  $x$  $$free in  . A variable $x$ occurs free in $e$ if at least one occurrence of $x$ in $e$ is free.

When applying an expression $e$ to some $e$_i, $e$ itself can be an application, so its reduction might return an effect , which is collected in the APP rule together with the effects of the arguments and the effect which is annotated at the type for $e$. Note that the VAR rule is needed in case that $e$ is not an application but a function or constructor symbol. The $e$_i can also be function calls which are evaluated lazily. At this point we need the groundness information about the arguments to choose the matching type for $e$ if several types can be derived.

The FCASE rule handles nondeterminism caused by narrowing. If the type A is derived for $x$ and more than two case branches exist, a non-empty effect must be returned to signalize the nondeterminism. This is ensured by adding the keyword $case$ (which will be indexed by the function name from the left-hand side in concrete programs) to the effect. Independent from the type of $x$, all effects from the right-hand sides must be collected. Note that for analysing the right-hand sides, the pattern variables are given the type of $x$: If $x$ is ground, the pattern variables will be instantiated to ground terms, too. Otherwise, they could be uninstantiated in the subsequent computation and therefore are given the type A.

If only one right-hand side has type A, the entire fcase-expression might return this type. Thus, with , the maximum type of all right-hand sides is the type of the fcase-expression.

The CASE rule analyses functions which are reduced by residuation. Thus, the case-expression itself will never split the computation and no additional effect is returned.

Nondeterminism which is caused by overlapping left-hand sides is handled by the OR rule, where the keyword $or$ is returned. Like in the (F)CASE rules, the effects of the right-hand sides are collected and the maximal type is returned. Note that by using $case$ and $or$ keywords, nondeterminism caused by narrowing and by overlapping left-hand sides can be distinguished.

The last rule, SUB, defines subtyping and subeffecting [19]. For our type system, the rule expresses that any expression of type G is also of type A, and that every effect can be enlarged without loosing the safety condition. The approximation just becomes more imprecise.

Next we have to show that the typing rules are correct. For that we need the definition of a correct type environment.

Thus, a correct type environment E for a program must contain at least one type for each defined function and constructor. Otherwise, the rules that use these constructors and functions cannot be correctly typed. Typical type annotations are $$c :: G (which is an abbreviation for ) for constants (0-ary constructors) $c$ and ,  for $n$-ary constructors $c$ ().

The correctness of the typing rules is stated by the following theorem:

 
 
The proof is omitted due to lack of space but can be found in a forthcoming technical report.

Thus, we know that every function that might raise a nondeterministic computation step during the reduction of $e$ will be collected in the effect by our typing rules, i.e., we will never miss such a function. This is the meaning of a safe approximation for our analysis. The same holds for the type, i.e., a term analysed as ground will indeed reduce to a ground term (if its reduction terminates). This enables us to chose the right type for a function symbol in a call after deriving the groundness information of its arguments. For arguments analysed as ground we can guarantee that they cannot cause a splitting whenever they are used for pattern matching in a fcase-expression because they cannot reduce to a free variable.

Note that it is not guaranteed that every term that reduces to a ground term will be analysed as a term of type G. Similarly, expressions with non-empty effects might nevertheless reduce deterministically.