Strong static typing such as that used in Gödel [Hill and LloydHill and Lloyd1994] and Mercury [Somogyi, Henderson, and ConwaySomogyi et al.1995] overcome problems with non-lists -- we don't have to consider if merge/3 behaves correctly with non-lists because it can't be called with or return non-lists. However, there are similar problems with unsorted lists: merge/3 can succeed with unsorted lists, it is asymmetric and there are many different definitions with different behaviours for unsorted lists. When code is written there are nearly always implicit assumptions about the context in which it is called. Often the assumptions about the calling context concern what are normally called types (for example, lists), though they can also be more complex and impossible to check statically. There is certainly some merit in having such assumptions documented by programmers declaring (possibly more complex) ``types'', ``assertions'' or ``preconditions''; this was our approach in [NaishNaish1992b]. As well as improving code readability, it can help with finding bugs because the extra information, which is redundant in correct programs, may be inconsistent with the executable part of the program. The Mercury compiler requires declarations concerning types, modes and determinism, and uses this information to produce more efficient code. Optional declarations are also used to increase efficiency in systems such as Ciao [Puebla, Bueno, and HermenegildoPuebla et al.2000]. A more expressive language for defining preconditions could help the Mercury compiler recognise determinism in more cases, for example, or allow certain transformations which would not be correct in general but are correct if the precondition holds.
However, there are several disadvantages and limitations of a semantics which relies on declared preconditions. First, as well as the language used to define merge/3, we have a language (with possibly a different syntax and its own semantics) for defining sorted lists and (typically) a declaration language relating the two. The semantics, and preferably debugging environments, are more complex and must deal with unintended cases such as preconditions which are always false. Second, it is hard to convince programmers to add extra declarations to their programs when they are unnecessary for the procedural semantics. Third, even willing programmers are unable to document all their assumptions using formal languages. For example, code for many declarative debuggers (discussed in the next section) assume that certain predicates are called with (representations of) atoms which have finite SLD trees or refutations and even assume the atoms have particular truth values in the intended interpretation [NaishNaish1992a]. Understanding the preconditions allows us to reason about the soundness and completeness of the debuggers. However, defining them formally would need us to circumvent the undecidability of the halting problem and formalise the intentions of certain programmers in the future!
Our approach to the semantics of a program is based on the view that the behaviours we care about are a subset of its possible behaviours. The subset may be described in some way but is not necessarily codified precisely (and it may not even be possible to do so). For example, we could use type and mode declarations to document the fact we care only about the behaviour of merge/3 when the first two arguments are instantiated to lists of numbers (and this information could be used for program analysis and optimisation). The semantics we propose is thus compatible with various forms of preconditions. However, it also leaves open the possibility that there are further undocumented restrictions on what we care about, such as the sortedness of the lists.