Linearity Requirement for Patterns

[Michael Hanus]

Jerzy Karczmarczuk wrote:
> Logic languages which allow for nonlinear patterns use unification,
> which is usually much more costly than simple pattern compiling.
> Now, I wonder whether in FP where there is no place for "logical
> variable" concept one needs or doesn't need the classical unification,
> with all the substitutions of variables.
> "Read-only" patterns are manipulated more efficiently, but in presence
> of laziness, of ~patterns etc., I feel - for the moment - rather
> lost.
> 
> What is the status of the referential transparency of Prolog or
> Mercury?

Prolog isn't referential transparent due to predefined predicates
with side effects. However, logic programming ("pure Prolog")
is referentially transparent if one considers a "non-deterministic"
semantics where an expression is reduced to a disjunction of
expressions (Prolog systems explore this disjunction in a
left-to-right manner by backtracking). Actually, one can
extend Haskell by "logical variables" in a conservative manner.
This is the idea of the functional logic language Curry
(http://www.informatik.uni-kiel.de/~curry/) where the pattern
matching process is slightly extended so that the operational
behavior is identical to Haskell (i.e., not more costly)
for programs without occurrences of logical variables
and, if a logical variable occurs during pattern matching,
it is (non-deterministically) bound to some pattern.
However, in order to support infinite data structures and
laziness, linear patterns are also required. Non-linear patterns
must be transformed into linear patterns by introducing
a unification constraint in the condition part, i.e., all
non-linearities must be made explicit in the program
(so that pattern matching can be efficiently performed).
Thus, I think that linearity is a natural requirement
even for logic languages that support laziness.

Michael