Local pattern declarations in Curry

From: Michael Hanus <hanus_at_informatik.rwth-aachen.de>
Date: Mon, 9 Nov 1998 18:13:46 +0100

Dear Colleagues,

before I am distributing the updated version of the Curry definition
(containing the language updates agreed during the last weeks),
I'd like to discuss one (syntactically) small but (semantically)
important extension of Curry, which is related to local
let/where declarations. During the last months, Sergio and I
discussed this topic and we have found a reasonable solution
which I want to sketch in the following.

The problem:
============
In contrast to logic programming, there is no syntactical
difference between variables (parameters) and functions
symbols. However, there are two situations where it is
necessary to distinguish these objects:

1. Different occurrences of the same variable are shared whereas
   different occurrences of the same function are not shared.
   It is well known that sharing of function parameters is
   important in a lazy language. Sharing or non-sharing makes
   no difference from a declarative point of view (in a purely
   functional language, but see also point 2), but if one want
   to reason about the run-time complexity of a program, this
   difference becomes important.

2. If some functions are non-deterministic, the sharing of
   objects influences also the semantics, i.e., the computed results.
   For instance, consider the non-deterministic function
     coin = 0
     coin = 1
   and a function which doubles its argument:
     double x = x+x
   Now consider the expression (double coin). If variables, i.e.,
   function parameters are shared, there are only two outcomes
   (0 or 2), whereas without sharing there are three possible
   outcomes (0, 1, or 2). There are good arguments to adopt
   the "call-time choice" where each parameter denotes a
   particular value at the time when a rule is applied. This
   is also conform with the lazy implementation point of view
   since it can be implemented by sharing the parameters
   (see the ESOP'96 paper from the Madrid group).

Usually, it is easy to distinguish between (non-shared) functions and
(shared) variables: in a rule, the outermost symbol denotes a function
and all non-constructor symbols of the left-hand side and all
explicitly or implicitly declared free variables are considered
as variables. However, this is not so clear with local declarations.
For instance, consider the following definition:

f = c+c where c = coin

If c is considered as a function (since it is the top-level symbol
of the local declaration), f is reducible to 0, 1, or 2.
If c is considered as a variable, f is reducible to 0 or 2.
Thus, the distinction between variables and functions
is semantically important.


Possible solutions:
===================
- Do not allow local declarations: this approach is taken in the
  Toy system from Madrid (which also implements non-deterministic
  functions), but I think most of us agree that this
  is too restrictive for a real programming language.

- Distinguish variables and functions syntactically: this approach
  is not compatible with Haskell

- Introduce some rules for the distinction between local variable and
  local function definitions: this might be ad hoc and leads to
  programs which are difficult to understand.


The proposed solution:
======================
Introduce a syntactic distinction between the local declaration
of a variable (pattern) or a function:

In a function declaration (local or non-local) of the form
  
    f t1 t2 ... tn = r

any non-constructor symbol in t1 t2 ... tn declares a new
variable.

A pattern declaration has the form

    p <- e

where p is a pattern (a constructor term in the current Curry
syntax), i.e., any non-constructor symbol in p is considered as
a new variable. These variables are instantiated by evaluating
e so far that it matches with p. For instance, the semantics of

    f x = q where p <- e or let p <- e in f x = q

is

    f x = f_aux x e
    f_aux x p = q

Pattern declarations are not allowed at the top level and are not
recursive (i.e., variables in p should not occur in e). This restriction
provides a translation of local declarations into global function
definitions (lambda lifting). It might be relaxed in some extension of
Curry supporting the explicit definition of graph structures.

A subtle point is the question whether it is allowed to have
local declarations of the form

    p = e

where p has a constructor at the top. Usually, this is intended
to be a pattern declaration and should be written as "p <- e".
For compatibility with Haskell, we could allow this but in this
case one should read it as a function definition. For instance,
the semantics of

   f x = q where (z1,z2) = e

could be defined as the definition of two projection functions z1,z2 by

   z1 (r,_) = r
   z2 (_,r) = r
   f x = q'

where each occurrence of zi in q is replaced in q' by (zi e)
(provided that zi does not occur in e). By this transformation,
the same results as in Haskell are computed but with possibly more
computation steps (although the complexity aspect in Haskell is
not so clear from the language definition).


An example:
===========
The following example shows the application of the local pattern
definition to define a demand-driven version of permutation sort nicely:

   -- Non-deterministic insertion in a list with local choose function
   insert x [] = [x]
   insert x (y:ys) = choose (x:y:ys) (y:insert x ys)
     where choose x _ = x
           choose _ y = y
   
   -- Non-deterministic generation of permutations
   permute [] = []
   permute (x:xs) = insert x (permute xs)
   
   -- Permutation sort with a lazy (demand-driven) generation of permutations:
   psort xs | sorted ys = ys where ys <- permute xs

("sorted ys" delivers True if ys is a sorted sequence).
Note that the alternative definition

   psort xs | sorted ys = ys where ys = permut xs

computes all possible permutations since the occurrences of ys
are not shared.


I think this is a reasonable solution which leads to
semantically clearer programs. However, any (constructive)
criticism is welcome.

Best regards,

Michael
Received on Mo Nov 09 1998 - 18:25:00 CET