[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
Declarative LETREC and DEFINE
We have been thinking about recursive declarations in Scheme. One of
the issues that has resurfaced is Alan Bawden's complaint about letrec
not being purely declarative. We agree with Alan and would like to
propose a change to the Report that avoids this problem. Please save
and latex the rest of this message.
-- Bruce Duba & Matthias Felleisen
% ------------------------------------------------------------------
\documentstyle[11pt]{article}
\setlength{\oddsidemargin}{.25in}
\setlength{\evensidemargin}{.25in}
\setlength{\textheight}{8.5 in}
\setlength{\textwidth}{6 in}
\setlength{\topmargin}{-.25 in}
\setlength{\baselineskip}{19pt}
\setlength{\marginparwidth}{0.9in}
\setlength{\marginparsep}{3pt}
\def\noi{\noindent}
\def\map{\longrightarrow}
\def\pair#1#2{\langle{#1}, {#2}\rangle}
\def\LB{{\lbrack\!\lbrack}}
\def\RB{{\rbrack\!\rbrack}}
\def\bracket#1{\LB#1\RB}
\def\of#1#2{{#1}\bracket{#2}}
\def\morph#1{{\cal {#1}}}
\def\E{\morph{E}}
\def\Eof#1{\of\E{#1}}
\def\mlet{\underline{{\it let\/}}}
\def\min{\underline{{\it in\/}}}
\begin{document}
\title{Declarative {\tt letrec} and {\tt define}\ \\}
\author{Bruce Duba \qquad Matthias Felleisen\\ \ \\ Rice University\\ \ \\}
\date{\fbox{{\sc Draft}: \today}}
\maketitle
\section{A Problem with {\tt letrec}}
Approximately two years ago, Alan Bawden demonstrated in a
message\footnote{ {\tt Message-ID:
<19890302162742.4.ALAN@PIGPEN.AI.MIT.EDU>}} to the bulletin board {\it
comp.lang.scheme} that Scheme's {\tt letrec} is not a purely
declarative facility. More precisely, removing {\tt set!} and
procedures with side-effects from Scheme does not result in a purely
functional language with continuations. In particulaer, reference
cells can be implemented via a combination of {\tt letrec} and {\tt
call-with-current-continuation} [Bawden: as above]:
\begin{verbatim}
(define (make-cell)
(call-with-current-continuation
(lambda (return-from-make-cell)
(letrec ((state
(call-with-current-continuation
(lambda (return-new-state)
(return-from-make-cell
(lambda (op)
(case op
((set)
(lambda (value)
(call-with-current-continuation
(lambda (return-from-access)
(return-new-state
(list value return-from-access))))))
((get) (car state)))))))))
((cadr state) 'done)))))
(define (set-cell cell value) ((cell 'set) value)) ; added by authors
(define (ref-cell cell) (cell 'get)) ; added by authors
\end{verbatim}
The reason for this phenomenon is the use of {\tt set!} for the
definition of {\tt letrec}'s semantics, which can be exposed by using
continuation operations. The same is also true for {\tt define}
statements since they too are expanded into {\tt set!}'s according to
the Report.
\section{Declarative Versions of {\tt letrec} and {\tt define}}
% We agree with the implicit message behind Alan Bawden's posting that
% this is a deplorable situation
We believe that {\tt letrec} should not be an imperative construct and
that a programmer should not be able to exploit it as one. To fix the
problem we propose a change in the semantics of {\tt letrec} and {\tt
define} such that they have a purely declarative character. The
following subsections describe the changes that are necessary to make
{\tt letrec} and {\tt define} fully declarative in the context of full
Scheme.
The idea behind the fix is to consider the evaluation of definitional
expressions in {\tt define} and {\tt letrec} expressions as separate
programs. This solution still permits the use of continuation
operations in {\tt letrec} and {\tt define}, but disables their
capability to reveal the {\tt set!} in their implementation. By being
simple and minimally restrictive, we believe that our proposal is in
the spirit of the rest of the Report.
\subsection{New Paragraph on {\tt letrec}, Subsection 4.2.2}
\def\hyper#1{\mbox{$\langle{\rm #1}\rangle$}}
\noindent({\tt letrec} \hyper{bindings} \hyper{body}) \hfill {essential syntax}
\medskip
\noindent {\it Syntax:\/}
\hyper{bindings} should have the form
\begin{center}
((\hyper{variable} \hyper{init}) \ldots),
\end{center}
and \hyper{body} should be a sequence of
one or more expressions. It is an error for a \hyper{variable} to appear more
than once in the list of variables being bound.
\medskip
\noindent {\it Semantics:\/}
The \hyper{variable}s are bound to fresh locations holding undefined
values, the \hyper{init}s are evaluated in the resulting environment
(in some unspecified order), each \hyper{variable} is assigned to the
result of the corresponding \hyper{init}, the \hyper{body} is
evaluated in the resulting environment, and the value of the last
expression in \hyper{body} is returned. Each binding of a
\hyper{variable} has the entire {{\tt letrec}} expression as its
region, making it possible to define mutually recursive procedures.
\begin{verbatim}
(letrec ((even?
(lambda (n)
(if (zero? n)
#f
(odd? (- n 1)))))
(odd?
(lambda (n)
(if (zero? n)
#f
(even? (- n 1))))))
(even? 88))
=> #t
\end{verbatim}
There are two important restrictions on {\tt letrec} expressions:
\begin{enumerate}
\item
It must be possible to evaluate each \hyper{init} without assigning or
referring to the value of any \hyper{variable}. If this restriction
is violated, then it is an error. The restriction is necessary
because Scheme passes arguments by value rather than by name.
\item
The evaluation of each \hyper{init} proceeds as if it were an isolated
program by itself, only sharing the lexical environment (including the
new bindings) with the rest of the program. This restriction is
necessary to enforce that {\tt letrec}-definitions are purely
declarative.
\end{enumerate}
In the most common uses of {\tt letrec}, all the \hyper{init}s are
{\tt lambda}-expressions and the restrictions are satisfied
automatically.
\subsection{New Version of Subsection 5.2.1}
At the top level of a program, a definition
\begin{center}
({\tt define} \hyper{variable} \hyper{expression})%
\end{center}
has almost the same effect as the assignment expression
\begin{center}
({\tt set!}\ \hyper{variable} \hyper{expression})%
\end{center}
if \hyper{variable} is bound. If \hyper{variable} is not bound,
however, then the definition will bind \hyper{variable} to a new
location before performing the assignment, whereas it would be an
error to perform a {\tt set!}\ on an unbound {unbound} variable.
\begin{verbatim}
(define add3
(lambda (x) (+ x 3)))
(add3 3) => 6
(define first car)
(first '(1 2)) => 1
\end{verbatim}
In analogy to {\tt letrec} expressions, there are two important
restrictions on definitions:
\begin{enumerate}
\item
It must be possible to evaluate \hyper{expression} without assigning
or referring to \hyper{variable}. If this restriction is violated,
then it is an error. The restriction is necessary because Scheme
passes arguments by value rather than by name.
\item
The evaluation of \hyper{expression} proceeds as if it were an
isolated program by itself, only sharing the lexical environment
(including the new bindings) with the rest of the program.
\end{enumerate}
All Scheme implementations must support top level definitions.
Some implementations of Scheme use an initial environment in
which all possible variables are bound to locations, most of
which contain undefined values. Top level definitions in
such an implementation are truly equivalent to assignments.
\subsection{New Paragraph on {\tt call-with-current-continuation},
Subsection 6.9}
({\tt call-with-current-continuation}\ {\it proc\/})\hfill{essential procedure}
\medskip
{\it Proc} must be a procedure of one argument. The procedure \\ {\tt
call-with-current-continuation} packages up the current continuation
(see the rationale below) as an ``escape procedure'' and passes it as
an argument to {\it proc}. The escape procedure is a Scheme procedure
of one argument that, if it is later passed a value, will ignore
whatever continuation is in effect at that later time and will give
the value instead to the continuation that was in effect when the
escape procedure was created.
The escape procedure that is passed to {\it proc} has unlimited extent
just like any other procedure in Scheme. It may be stored in
variables or data structures and may be called as many times as
desired.
The following examples show only the most common uses of \\ {\tt
call-with-current-continuation}. If all real programs were as simple
as these examples, there would be no need for a procedure with the
power of \\ {\tt call-with-current-continuation}.
\begin{verbatim}
(call-with-current-continuation
(lambda (exit)
(for-each (lambda (x)
(if (negative? x)
(exit x)))
'(54 0 37 -3 245 19))
#t)) => -3
(define list-length
(lambda (obj)
(call-with-current-continuation
(lambda (return)
(letrec ((r
(lambda (obj)
(cond ((null? obj) 0)
((pair? obj)
(+ (r (cdr obj)) 1))
(else (return #f))))))
(r obj))))))
(list-length '(1 2 3 4)) => 4
(list-length '(a b . c)) => #f
\end{verbatim}
The construction and the use of escape procedures is subject to the
restrictions for the evaluation of \hyper{init} expressions in {\tt
letrec} (see Subsection~4.2.2 above) and the evaluation of
\hyper{expression} in definitions (see Subsection~5.2.1
above). In both cases, the evaluation of the respective expressions
acts as if a {\it new\/} program were evaluated at the top-level in
the current lexical environment. This is equivalent to the statement
that the expression is evaluated in the initial continuation. It
follows that the evaluation is forced to return a value, to diverge,
or to result in {\it wrong\/}; and that escape procedures constructed
during the evaluation of the expressions only represent the rest of
the computation of the definitional expressions. For example,
\begin{verbatim}
(letrec ((stop (call-with-current-continuation (lambda (x) x)))) stop)
\end{verbatim}
returns a procedure that terminates a program evaluation and returns
its argument as the result of the program. The definiton
\begin{verbatim}
(define stop (call-with-current-continuation (lambda (x) x))
\end{verbatim}
defines the same procedure.
\medskip
\noi {\it Rationale for {\tt call-with-current-continuation}:\/}
A common use of {\tt call-with-current-continuation} is for
structured, non-local exits from loops or procedure bodies, but in fact
{\tt call-with-current-continuation} is extremely useful for implementing a
wide variety of advanced control structures.
Whenever a Scheme expression is evaluated there is a {continuation}
wanting the result of the expression. The continuation represents an
entire (default) future for the computation. If the expression is
evaluated at top level, for example, then the continuation will take
the result and return it to the programming environment for further
processing. Most of the time the continuation includes actions
specified by user code, as in a continuation that will take the
result, multiply it by the value stored in a local variable, add
seven, and give the answer to the top level continuation. Normally
these ubiquitous continuations are hidden behind the scenes and
programmers don't think much about them. On rare occasions, however,
a programmer may need to deal with continuations explicitly. {\tt
Call-with-current-continuation} allows Scheme programmers to do that
by creating a procedure that acts just like the current continuation.
Most programming languages incorporate one or more special-purpose
escape constructs with names like {\tt exit}, \hbox{{\tt return}}, or
even {\tt goto}. In 1965, however, Peter Landin~[{Landin65}] invented
a general purpose escape operator called the J-operator. John
Reynolds~[{Reynolds72}] described a simpler but equally powerful
construct in 1972. The {\tt catch} special form described by Sussman
and Steele in the 1975 report on Scheme is exactly the same as
Reynolds's construct, though its name came from a less general
construct in MacLisp. Several Scheme implementors noticed that the
full power of the {\tt catch} construct could be provided by a
procedure instead of by a special syntactic construct, and the name
{\tt call-with-current-continuation} was coined in 1982. This name is
descriptive, but opinions differ on the merits of such a long name,
and some people use the name {\tt call/cc} instead.
\subsection{Additions to the denotational semantics (Section~7)}
\def\out{{\it out\/}_A}
\def\in{{\it in\/}_A}
\subsubsection*{Change Last paragraph of the Introduction to Section~7.2}
If {\it P}{} is a program in which all variables are defined before being
referenced or assigned, then the meaning of {\it P}{} is
$$\Eof{\hbox{\tt(({\tt lambda} ({\rm I}${}^*$) {\it P}')
\hyper{undefined} \ldots)}}$$
where I${}^*$ is the sequence of variables defined in {\it P}, ${\it P}'$
is the sequence of expressions obtained by replacing every definition
\begin{center}
({\tt define} I Exp)
\end{center}
in {\it P}{} by an assignment,
\begin{center}
({\tt set!} I ({\tt letrec} ((V Exp)) V))
\end{center}
where V is an identifier that does not occur in Exp;
\hyper{undefined} is an expression that evaluates to {\it undefined},
and $\E$ is the semantic function that assigns meaning to expressions.
\subsubsection*{The Domain of Expression Continuations}
Add the following remark to the domain equation for {\tt K}:
Expression continuations are {\it strict\/} in $\perp$ and values from
{\tt X} (errors).
\subsubsection*{Add at the end of Subsection~7.2.3}
\noi{\it Answers, Expressed Values, and the Initial Continuation}
We assume the existence of two functions relating expressed values,
{\tt E}, with answers, {\tt A}. First, we assume that there is an
initial continuation:
\begin{eqnarray*}
\in &:& {\tt E} \map {\tt S} \map {\tt A} \\
\end{eqnarray*}
Second, we assume that the initial continuation has a left-inverse:
\begin{eqnarray*}
\out &:& {\tt A} \map {\tt E} \times {\tt S}
\end{eqnarray*}
such that
\[ \out(\in\ \epsilon\ \sigma) = \pair\epsilon\sigma. \]
\subsubsection*{Add to the semantic function $\E$ after last clause}
\def\lentie{%
\newdimen\p\setbox4=\hbox{$\qquad {\it tievals\/}(\lambda\alpha^*\sigma.$}\p=\wd4\kern\p}
\def\lents{%
\newdimen\p\setbox5=\hbox{$\qquad {\it tievals\/}$}\p=\wd5\kern\p}
\begin{eqnarray*}
&&
\Eof{({\rm letrec}\
(({\rm I}_1\ {\rm E}_1) \cdots ({\rm I}_n\ {\rm E}_n))\ {\rm E})} = \\
&&\quad \lambda\rho\kappa.\\
&&\qquad {\it tievals\/}(\lambda\alpha^*\sigma. % \\ &&\lentie
\mlet\ \langle l_1,\ldots,l_n \rangle = \alpha^*\ \min\\
&&\lentie
\mlet\ \rho =
{\it extends\/}\ \rho\ \langle {\rm I}_1, \ldots, {\rm I}_n\rangle\ \alpha^*\min\\
&&\lentie
\mlet\ \pair{\epsilon_1}{\sigma_1} = \out(\Eof{{\rm E}_{i_1}}\rho\in\sigma)\ \min\\
&&\lentie
\vdots\\
&&\lentie
\mlet\ \pair{\epsilon_{j+1}}{\sigma_{j+1}} =
\out(\Eof{{\rm E}_{i_{j+1}}}\rho\in\sigma_j)\ \min\\
&&\lentie
\vdots\\
&&\lentie\qquad
\Eof{{\rm E}}\rho\kappa
({\it update\/}\ l_{i_1}\ \epsilon_1\ \ldots
({\it update\/}\ l_{i_n}\ \epsilon_n\ \sigma_n)))
\\
&&\lents \langle{{\it unspecified\/}, \ldots, {\it unspecified\/}} \rangle
\mbox{ \% {\it n\/}-times}\\
% \underbrace{{\it unspecified\/}, \ldots, {\it unspecified\/}}_{n}
&&\quad\mbox{where $i_1, \ldots, i_n$ is an arbitrary
permutation of $1, \ldots, n$}
\end{eqnarray*}
\section{Side-effects of our Changes}
The new definitions eliminate the connection between the report and
the programming environment of actual implementations, i.e., the
report no longer mentions the top-level read-eval-print loop. We
believe that this is desirable in face of the emerging stand-alone
compilers that are independent of user interactions.
\section{Implementation Effort}
The implementation effort should be minimal. We have implemented the
proposal in Chez Scheme. The fixes rely on non-RRRS features and are
not portable but we guess that a similar implementation should be
possible for other versions of Scheme.
\end{document}