[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

*To*: rrrs-authors@mc.lcs.mit.edu*Subject*: Declarative LETREC and DEFINE*From*: Matthias Felleisen <matthias@rice.edu>*Date*: Fri, 11 Jan 91 13:45:18 CST

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}

- Next by Date:
**Re: Declarative LETREC and DEFINE** - Next by thread:
**Re: Declarative LETREC and DEFINE** - Index(es):