Commit 2ab78c20 authored by Michael Hanus 's avatar Michael Hanus
Browse files

Version 0.6 of the Curry Report

parent ac978a9d
% $Id: report.tex,v 1.3 1999/08/26 12:48:40 hanus Exp hanus $
% $Id: report.tex,v 1.4 1999/08/30 10:14:20 hanus Exp hanus $
% $Log: report.tex,v $
% Revision 1.4 1999/08/30 10:14:20 hanus
% Description of module system modified (for conformity with Haskell)
%
% Revision 1.3 1999/08/26 12:48:40 hanus
% Section about lambda lifting updated
%
......@@ -95,7 +98,7 @@
\begin{center}\vspace{10ex}
{\Huge\bf Curry}\\[4ex]
{\LARGE\bf An Integrated Functional Logic Language}\\[5ex]
{\large\bf Version 0.5.2}\\[1ex]
{\large\bf Version 0.6}\\[1ex]
{\large \today}\\[8ex]
\Large
Michael Hanus$^1$ [editor] \\[3ex]
......@@ -103,15 +106,17 @@ Michael Hanus$^1$ [editor] \\[3ex]
Sergio Antoy$^2$ \\
Herbert Kuchen$^3$ \\
Francisco J. L\'opez-Fraguas$^4$ \\
Juan Jos\'e Moreno Navarro$^5$ \\
Frank Steiner$^6$ \\[20ex]
Wolfgang Lux$^5$ \\
Juan Jos\'e Moreno Navarro$^6$ \\
Frank Steiner$^7$ \\[15ex]
\normalsize
(1) RWTH Aachen, Germany, {\tt hanus@informatik.rwth-aachen.de} \\
(2) Portland State University, USA, {\tt antoy@cs.pdx.edu} \\
(3) University of M\"unster, Germany, {\tt kuchen@uni-muenster.de} \\
(4) Universidad Complutense de Madrid, Spain, {\tt fraguas@dia.ucm.es} \\
(5) Universidad Polit\'ecnica de Madrid, Spain, {\tt jjmoreno@fi.upm.es} \\
(6) RWTH Aachen, Germany, {\tt steiner@i2.informatik.rwth-aachen.de} \\[5ex]~
(5) University of M\"unster, Germany, {\tt wlux@uni-muenster.de} \\
(6) Universidad Polit\'ecnica de Madrid, Spain, {\tt jjmoreno@fi.upm.es} \\
(7) RWTH Aachen, Germany, {\tt steiner@i2.informatik.rwth-aachen.de} \\[5ex]~
\end{center}
\end{minipage}}
\end{center}
......@@ -386,7 +391,13 @@ to an expression \pr{double$\,t$}, we obtain the new expression
\pr{$t$+$t$} but both occurrences of $t$ denote the identical
expression, i.e., these subterms will be simultaneously evaluated.
Thus, \emph{several occurrences of the same variable are
always shared.} This is necessary not only for efficiency reasons
always shared},\index{sharing}
i.e., if one occurrence of an argument variable,
which might bound to an evaluable expression when the function
is applied, is evaluated to some value, all other occurrences
of this variable are replaced by the same value (without
evaluating these other occurrences again).
This sharing is necessary not only for efficiency reasons
but it has also an influence on the soundness of the operational semantics
in the presence of non-deterministic functions
(see also \cite{GonzalesEtAl96ESOP}). For instance,
......@@ -775,7 +786,18 @@ unification to \emph{higher-order unification}
\cite{HanusPrehofer96RTA,NadathurMiller88,Prehofer95Diss}.
Since higher-order unification is a computationally expensive
operation, Curry delays the application of unknown functions
until the function becomes known \cite{Ait-KaciLincolnNasr87,Smolka95}.
until the function becomes known
\cite{Ait-KaciLincolnNasr87,Smolka95}.\footnote{Note that
an unbound functional variable can never be instantiated
if all program rules are constructor-based and the equational constraint
\pr{=:=} denotes equality between data terms.
However, extensions of Curry might overcome this weakness
by instantiating unbound functional variables to
(type-conform) functions occurring in the program in order
to evaluate an application (as in \cite{Gonzalez-MorenoEtAl97ICLP}),
or by considering partial applications
(i.e., functions calls with less than the required number of arguments)
as data terms (as in \cite{Warren82}).}
Thus, the application operation can be considered as a function
(``\pr{@}'' is a left-associative infix operator)
\startprog
......@@ -2668,7 +2690,7 @@ infixr 9 .
infixl 7 *, /, `div`, `mod`
infixl 6 +, -
infixr 5 ++, :
infix 4 =:=, ==, <, >, <=, >=
infix 4 =:=, ==, /=, <, >, <=, >=
infixr 3 \&\&
infixr 2 ||
infixr 1 >>, >>=
......@@ -2685,12 +2707,19 @@ f . g = \ttbs{}x -> f (g x)
id :: a -> a \pindex{id}
id x = x
~
-- Constant function
const :: a -> b -> a \pindex{const}
const x _ = x
~
-- Convert an uncurried function to a curried function
curry :: ((a,b) -> c) -> a -> b -> c \pindex{curry}
curry f a b = f (a,b)
~
-- Convert an curried function to a function on pairs
uncurry :: (a -> b -> c) -> (a,b) -> c \pindex{uncurry}
uncurry f (a,b) = f a b
~
-- (flip f) is identical to f but with the order of arguments reversed
flip :: (a -> b -> c) -> b -> a -> c \pindex{flip}
flip f x y = f y x
~
......@@ -2714,8 +2743,12 @@ not :: Bool -> Bool \pindex{not}
not True = False
not False = True
~
otherwise :: Bool \pindex{otherwise}
otherwise = True
otherwise :: Bool \pindex{otherwise}
otherwise = True
~
-- Disequality
(/=) :: a -> a -> Bool \pindex{/=}
x /= y = not (x==y)
~
~
-- Pairs
......@@ -2780,6 +2813,11 @@ zip :: [a] -> [b] -> [(a,b)] \pindex{zip}
zip [] [] = []
zip (x:xs) (y:ys) = (x,y) : zip xs ys
~
-- Join three list to one list of triples
zip3 :: [a] -> [b] -> [c] -> [(a,b,c)]
zip3 [] [] [] = []
zip3 (x:xs) (y:ys) (z:zs) = (x,y,z) : zip3 xs ys zs
~
-- Concatenate a list of lists into one list
concat :: [[a]] -> [a] \pindex{concat}
concat l = foldr (++) [] l
......@@ -2806,6 +2844,20 @@ dropWhile :: (a -> Bool) -> [a] -> [a] \pindex{dropWhile}
dropWhile _ [] = []
dropWhile p (x:xs) = if p x then dropWhile p xs else x:xs
~
-- break a string into list of lines where a line is terminated at a
-- newline character. The resulting lines do not contain newline characters.
lines :: String -> [String] \pindex{lines}
lines [] = []
lines (c:cs) = let (l,restcs) = breakline (c:cs) in l : lines restcs
where breakline [] = ([],[])
breakline (c:cs) = if c=='\ttbs{}n'
then ([],cs)
else let (ds,es) = breakline cs in ((c:ds),es)
~
-- concatenate a list of strings with terminating newlines
unlines :: [String] -> String \pindex{unlines}
unlines ls = concat (map (++"\ttbs{}n") ls)
~
~
-- Conversion functions between characters and their ASCII values
~
......@@ -2847,6 +2899,24 @@ success :: Constraint \pindex{success}
c1 \&> c2 | c1 = c2
~
~
-- Maybe type
~
data Maybe a = Nothing | Just a \pindex{Maybe}\pindex{Nothing}\pindex{Just}
~
maybe :: b -> (a -> b) -> Maybe a -> b \pindex{maybe}
maybe n _ Nothing = n
maybe _ f (Just x) = f x
~
~
-- Either type
~
data Either a b = Left a | Right b \pindex{Either}\pindex{Left}\pindex{Right}
~
either :: (a -> c) -> (b -> c) -> Either a b -> c \pindex{either}
either f _ (Left x) = f x
either _ g (Right x) = g x
~
~
-- Monadic IO
~
data IO a -- conceptually: \mbox{\it{}World} -> (a,\mbox{\it{}World}) \pindex{IO}
......@@ -2859,6 +2929,7 @@ done :: IO () \pindex{done}
return :: a -> IO a \pindex{return}
readFile :: String -> IO String \pindex{readFile}
writeFile :: String -> String -> IO () \pindex{writeFile}
appendFile :: String -> String -> IO () \pindex{appendFile}
~
putStr :: String -> IO () \pindex{putStr}
putStr [] = done
......@@ -3413,7 +3484,7 @@ as $\varphi(e_1,\ldots,e_n)$
which is equivalent to Curry's notation $\varphi~e_1\ldots e_n$.}
The set of all expressions and data terms are denoted
by $\Tc(\Cc \cup \Fc,\Xc)$ and $\Tc(\Cc,\Xc)$, respectively.
A \emph{function pattern}\index{function pattern}\index{pattern!function}
A \emph{call pattern}\index{call pattern}\index{pattern!call}
is an expression of the form
$f(t_1,\ldots,t_n)$ where each variable occurs only once,
$f \in \Fc$ is an $n$-ary function, and $t_1,\ldots,t_n \in \Tc(\Cc,\Xc)$.
......@@ -3448,7 +3519,7 @@ for every expression $f(e_1,\ldots,e_n)$.
A Curry program is a set of rules \pr{$l$\,=\,$r$} satisfying
some restrictions (see Section~\ref{sec-funcdecl}).
In particular, the left-hand side $l$ must be a function pattern.
In particular, the left-hand side $l$ must be a call pattern.
A rewrite rule is called a \emph{variant}\index{variant} of another rule
if it is obtained by a unique replacement of variables
by other variables.
......@@ -3476,7 +3547,7 @@ of definitional trees.}
A definitional tree is a hierarchical structure containing
all rules of a defined function.
$\Tc$ is a
\emph{definitional tree with function pattern}\index{definitional tree} $\pi$
\emph{definitional tree with call pattern}\index{definitional tree} $\pi$
iff the depth of $\Tc$ is finite and
one of the following cases holds:
\begin{description}
......@@ -3488,21 +3559,21 @@ $r \in \{rigid,flex\}$,
$c_1,\ldots,c_k$ are different constructors of the sort
of $\pi|_o$, for some $k > 0$,
and, for all $i = 1,\ldots,k$, $\Tc_i$ is a definitional tree with
function pattern $\pi[c_i(x_1,\ldots,x_n)]_o$,
call pattern $\pi[c_i(x_1,\ldots,x_n)]_o$,
where $n$ is the arity of $c_i$ and
$x_1,\ldots,x_n$ are new variables.
\item [$\Tc=or(\Tc_1,\Tc_2),$] where $\Tc_1$ and $\Tc_2$ are
definitional trees with function pattern $\pi$.\footnote{For the sake of
definitional trees with call pattern $\pi$.\footnote{For the sake of
simplicity, we consider only binary $or$ nodes. The extension
to such nodes with more than two subtrees is straightforward.}
\end{description}
A \emph{definitional tree of an $n$-ary function} $f$
is a definitional tree $\Tc$ with function pattern $f(x_1,\ldots,x_n)$,
is a definitional tree $\Tc$ with call pattern $f(x_1,\ldots,x_n)$,
where $x_1,\ldots,x_n$ are distinct variables, such that for each rule
$l \pr{\,=\,} r$ with $l = f(t_1,\ldots,t_n)$ there is a node
$rule(l' \pr{\,=\,} r')$
in $\Tc$ with $l$ variant of $l'$.
In the following, we write $pat(\Tc)$ for the function pattern
In the following, we write $pat(\Tc)$ for the call pattern
of a definitional tree $\Tc$.
It is always possible to construct a definitional tree
......@@ -3740,8 +3811,24 @@ this description of the operational semantics is based on term rewriting
and does not take into account that common subterms are shared
(see Section~\ref{sec-variable-sharing}). We only note here that
\emph{several occurrences of the same variable are always shared},
i.e., subterms obtained by the instantiation
of the same variable are always simultaneously evaluated.
\index{sharing}
i.e., if an argument of a function is instantiated during a call
to this function to an expression and this expression is evaluated
to some value (head normal form), then all other expressions
resulting from instantiating occurrences of the same argument
are replaced by the same value (head normal form).\footnote{
It should be noted that values are constructor terms
like \pr{23}, \pr{True}, or \pr{[2,4,5]}.
This means that the evaluation of constraints and I/O actions
are not shared since they are not replaced by a value after
evaluation but constraints are solved in order to apply a conditional rule
(in case of constraints) and I/O actions are applied to the outside
world when they appear at the top-level in a program.
This is the intended behavior since the expressions
``\pr{putChar 'a' >> putChar 'a'}'' and
``\pr{let ca = putChar 'a' in ca >> ca}'' should have
an identical behvarior, namely printing the character \pr{'a'}
twice.}
This is necessary not only for efficiency reasons
but also for the soundness of the operational semantics
in the presence of non-deterministic functions, as discussed
......@@ -3944,12 +4031,12 @@ To specify the construction algorithm, we define by
DP(\pi,R) = \{ o \mbox{ position of a variable in } \pi \mid
root(l|_o) \in \Cc \mbox{ for some } l \pr{\,=\,} r \in R \}
\]
the set of \emph{demanded positions} of a function pattern $\pi$ w.r.t.\ a
set of rules $R$. For instance, the demanded positions of the function pattern
the set of \emph{demanded positions} of a call pattern $\pi$ w.r.t.\ a
set of rules $R$. For instance, the demanded positions of the call pattern
\pr{leq(x,y)} w.r.t.\ the rules for the predicate \pr{leq}
(see Section~\ref{example-leq}, page~\pageref{example-leq})
are $\{1,2\}$ referring to the pattern variables \pr{x} and \pr{y}.
The \emph{g}eneration of a definitional \emph{t}ree for a function pattern
The \emph{g}eneration of a definitional \emph{t}ree for a call pattern
$\pi$ and a set of rules $R$ (where $l$ is an instance of $\pi$ for each
$l \pr{\,=\,} r \in R$) is described by the function $gt(\pi,m,R)$
($m \in \{flex,rigid\}$ determines the mode annotation in the generated
......@@ -3980,7 +4067,7 @@ $R' = \{ l \pr{\,=\,} r \in R \mid root(l|_o) \in \Cc \} \neq R$, then
gt(\pi,m,R) = or(gt(\pi,m,R'),gt(\pi,m,R-R'))
\]
I.e., we generate an $or$ node if the leftmost demanded position
of the function pattern is not demanded by the left-hand sides of all rules.
of the call pattern is not demanded by the left-hand sides of all rules.
\item
If $DP(\pi,R) = \emptyset$ and $l \pr{\,=\,} r$ variant of some rule in $R$
with $l = \pi$, then
......@@ -4006,7 +4093,7 @@ It is easy to see that this algorithm
computes a definitional tree for each
function since the number of rules is reduced in each recursive call
and it keeps the invariant that the left-hand sides of the current set
of rules are always instances of the current function pattern.
of rules are always instances of the current call pattern.
The algorithm $gt$ conforms to the evaluation strategy
of functional languages like Haskell or Miranda, since it generates
......@@ -4195,7 +4282,7 @@ one or both of these definitions.
In the description of the operational semantics above,
we assumed that a Curry program is a set of rules \pr{$l$\,=\,$r$}
where the left-hand side $l$ is a function pattern and the
where the left-hand side $l$ is a call pattern and the
right-hand side $r$ is an expression containing variables,
constructors, and defined functions.
However, a Curry program can also contain local declarations
......@@ -4289,14 +4376,17 @@ $l$ = let $decls$ in $r$ .
\stopprog
Each conditional rule of the form
\startprog
$l$ | $c$ = $r$ where $decls$
$l$ | $c$ = $r$ $[\,$where $decls\,]$
\stopprog
is transformed into
\startprog
$l$ = let $decls$ in ($c$|$r$)
$l$ = $[\,$let $decls$ in$\,]$ ($c$|$r$)
\stopprog
where the meaning of the guarded expression \pr{($c$|$r$)}
is explained in Figure~\ref{figure-condrules}.
Thus, we assume in the subsequent transformations that
all program rules are of the form ``\pr{$l$\,\,=\,$r$}''
(where $r$ might be a let-expression).
Note that this transformation is not really necessary
but provides for a unified treatment of the elimination
......@@ -4330,7 +4420,8 @@ $l$ = let $decls_1$
\stopprog
with $free(e) \subseteq free(l)$
(it is a programming error if no pattern declaration has this property,
i.e., cyclic pattern definitions are not allowed).
i.e., cyclic pattern definitions or pattern definitions
depending on locally free variables are not allowed).
Then transform this rule into the rules
\startprog
$l$ = $f'~x_1\ldots{}x_k~e$
......@@ -4368,7 +4459,8 @@ f x = let y free
If the definitions of all locally declared functions are completed,
i.e., the definitions only refer to variables in the argument
patterns, delete the locally declared functions and
define them at the top-level. For instance, the previous
define them at the top-level (and rename them if there are already
top-level functions with the same name). For instance, the previous
rule is transformed into the definitions
\startprog
g y z = c y z
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment