- Contemporary messages sorted: [ by date ] [ by thread ] [ by subject ] [ by author ] [ by messages with attachments ]

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

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

*
This archive was generated by hypermail 2.3.0
: Do Aug 06 2020 - 07:15:04 CEST
*