Nondeterminism analysis of functional logic programs

Information about the nondeterminism behavior of a functional logic program is important for various reasons. For instance, a nondeterministic choice in I/O operations results in a run-time error. Thus, it is desirable to ensure at compile time that a given program is not going to crash in this way. Furthermore, knowledge about nondeterminism can be exploited to optimize programs. In particular, if functional logic programs are compiled to target languages without builtin support for nondeterministic computations, the transformation can be much simpler if it is known that the source program is deterministic. In this paper we present a nondeterminism analysis of functional logic programs in form of a type/effect system. We present a type inferencer to approximate the nondeterminism behavior via nonstandard types and show its correctness w.r.t. the operational semantics of functional logic programs. The type inference is based on a new compact representation of sets of types and effects.