End Sept
[haskell-report.git] / report / exps.verb
1 %
2 % $Header: /home/cvs/root/haskell-report/report/exps.verb,v 1.10 2001/09/24 14:40:47 simonpj Exp $
3 %
4 %*section 3
5 %**<title>The Haskell 98 Report: Expressions</title>
6 %**~header
7 \section{Expressions}\index{expression}
8 \label{expressions}
9
10 In this section, we describe the syntax and informal semantics of
11 \Haskell{} {\em expressions}, including their translations into the
12 \Haskell{} kernel, where appropriate.  Except in the case of @let@
13 expressions, these translations preserve both the static and dynamic
14 semantics.  Free variables and constructors used in these translations
15 always refer to entities defined by the @Prelude@.  For example,
16 ``@concatMap@'' used in the translation of list comprehensions
17 (Section~\ref{list-comprehensions}) means the @concatMap@ defined by
18 the @Prelude@, regardless of whether or not the identifier ``@concatMap@'' is in
19 scope where the list comprehension is used, and (if it is in scope)
20 what it is bound to.
21
22 In the syntax that follows, there are some families of nonterminals
23 indexed by precedence levels (written as a superscript).  Similarly, the
24 nonterminals "op", "varop", and "conop" may have a double index:
25 a letter "l", "r", or "n" for left-, right- or non-associativity and
26 a precedence level.  A precedence-level variable "i" ranges from 0 to 9;
27 an associativity variable "a" varies over "\{l, r, n\}".
28 For example
29 @@@
30 aexp    ->  @(@ exp^{i+1} qop^{(a,i)} @)@
31 @@@
32 actually stands for 30 productions, with 10 substitutions for "i"
33 and 3 for "a".
34
35 @@@
36 exp     ->  exp^0 @::@ [context @=>@] type      & (\tr{expression type signature})
37         |   exp^0
38 exp^i   ->  exp^{i+1} [qop^{({\rm{n}},i)} exp^{i+1}]
39         |   lexp^i
40         |   rexp^i
41 lexp^i  ->  (lexp^i | exp^{i+1}) qop^{({\rm{l}},i)} exp^{i+1}
42 lexp^6  ->  @-@ exp^7
43 rexp^i  ->  exp^{i+1} qop^{({\rm{r}},i)} (rexp^i | exp^{i+1})
44 exp^{10} ->  @\@ apat_1 ... apat_n @->@ exp     & (\tr{lambda abstraction}, n>=1)
45         |   @let@ decls @in@ exp                & ({\tr{let expression}})
46         |   @if@ exp @then@ exp @else@ exp      & (\tr{conditional})
47         |   @case@ exp @of@ @{@ alts  @}@       & (\tr{case expression})
48         |   @do@ @{@ stmts @}@                  & (\tr{do expression})
49         |   fexp
50 fexp    ->  [fexp] aexp                         & (\tr{function application})
51
52 aexp    ->  qvar                                & (\tr{variable})
53         |   gcon                                & (\tr{general constructor})
54         |   literal                             
55         |   @(@ exp @)@                       & (\tr{parenthesized expression})
56         |   @(@ exp_1 @,@ ... @,@ exp_k @)@     & (\tr{tuple}, k>=2)
57         |   @[@ exp_1 @,@ ... @,@ exp_k @]@     & (\tr{list}, k>=1)
58         |   @[@ exp_1 [@,@ exp_2] @..@ [exp_3] @]@ & (\tr{arithmetic sequence})
59         |   @[@ exp @|@ qual_1 @,@ ... @,@ qual_n @]@   & (\tr{list comprehension}, n>=1)
60         |   @(@ exp^{i+1} qop^{(a,i)} @)@        & (\tr{left section})
61         |   @(@ qop^{(a,i)} exp^{i+1} @)@        & (\tr{right section})
62         |   qcon @{@ fbind_1 @,@ ... @,@ fbind_n @}@ & (\tr{labeled construction}, n>=0)
63         |   aexp_{\{qcon\}} @{@ fbind_1 @,@ ... @,@ fbind_n @}@ & (\tr{labeled update}, n >= 1)
64
65 @@@
66 \indexsyn{exp}%
67 \index{exp@@"exp^i"}%
68 \index{lexp@@"lexp^i"}%
69 \index{rexp@@"rexp^i"}%
70 \indexsyn{aexp}%
71 \indexsyn{fexp}%
72
73 %       Removed Aug 2001: more misleading than helpful. SLPJ
74 % As an aid to understanding this grammar,
75 % Table~\ref{syntax-precedences} shows the relative precedence of
76 % expressions, patterns and definitions, plus an extended associativity.
77 % "-" indicates that the item is non-associative.
78
79 % \begin{table}[tb]
80 % \[
81 % \centerline{
82 % \begin{tabular}{|l|c|}\hline
83 % Item                                          &       Associativity \\ 
84 % \hline
85 %                                               &                       \\
86 % simple terms, parenthesized terms               &     --              \\
87 % irrefutable patterns (@~@)                      &       --            \\
88 % as-patterns ({\tt @@})                          &       right         \\
89 % function application                          &       left            \\
90 % @do@, @if@, @let@, lambda(@\@), @case@ (leftwards)&   right           \\
91 % @case@ (rightwards)                           &       right           \\
92 %                                               &                       \\
93 % infix operators, prec. 9                      &       as defined      \\
94 % \ldots                                                &       \ldots          \\
95 % infix operators, prec. 0                      &       as defined      \\
96 %                                               &                       \\
97 % function types (@->@)                         &       right           \\
98 % contexts (@=>@)                                       &       --              \\
99 % type constraints (@::@)                               &       --              \\
100 % @do@, @if@, @let@, lambda(@\@) (rightwards)   &       right           \\
101 % sequences (@..@)                              &       --              \\
102 % generators (@<-@)                             &       --              \\
103 % grouping (@,@)                                        &       n-ary           \\
104 % guards (@|@)                                  &       --              \\
105 % case alternatives (@->@)                      &       --              \\
106 % definitions (@=@)                             &       --              \\
107 % separation (@;@)                              &       n-ary           \\ 
108 % \hline
109 % \end{tabular}
110 % }
111 % \]
112 % %**<div align=center> <h4>Table 1</h4> </div>
113 % \ecaption{Precedence of expressions, patterns, definitions (highest to lowest)}
114 % \label{syntax-precedences}
115 % \end{table}
116
117 The grammar is ambiguous regarding the extent of lambda abstractions,
118 let expressions, and conditionals.  The ambiguity is resolved by the
119 meta-rule that each of these constructs extends as far to the right as
120 possible.  As a consequence, each of these constructs has two precedences,
121 one to its left, which is the precedence used in the grammar; and
122 one to its right, which is obtained via the meta-rule.  See the sample
123 parses below.
124
125 Expressions involving infix operators are disambiguated by the
126 operator's fixity (see Section~\ref{fixity}).  Consecutive
127 unparenthesized operators with the same precedence must both be either
128 left or right associative to avoid a syntax error.
129 Given an unparenthesized expression ``"x qop^{(a,i)} y qop^{(b,j)} z"'', parentheses
130 must be added around either ``"x qop^{(a,i)} y"'' or ``"y qop^{(b,j)}
131 z"'' when "i=j" unless "a=b={\rm l}" or "a=b={\rm r}".
132
133 Negation\index{negation} is the only prefix operator in
134 \Haskell{}; it has the same precedence as the infix @-@ operator
135 defined in the Prelude (see Figure~\ref{prelude-fixities}%
136 %*ignore
137 , page~\pageref{prelude-fixities}%
138 %*endignore
139 ).
140
141 %       I can't make head or tail of this para, so
142 %       I'm just deleting it.  SLPJ Dec 98
143 % The separation of function arrows from case alternatives solves
144 % the ambiguity that otherwise arises when an unparenthesized
145 % function type is used in an expression, such as the guard in a case
146 % expression.
147
148 Sample parses are shown below.
149 \[\bt{|l|l|}%%b
150 \hline
151 This                                & Parses as                             \\
152 \hline
153 @f x + g y@                         & @(f x) + (g y)@                       \\
154 @- f x + y@                         & @(- (f x)) + y@                       \\
155 @let { ... } in x + y@              & @let { ... } in (x + y)@              \\
156 @z + let { ... } in x + y@          & @z + (let { ... } in (x + y))@        \\
157 @f x y :: Int@                      & @(f x y) :: Int@                      \\
158 @\ x -> a+b :: Int@                 & @\ x -> ((a+b) :: Int@)               \\
159 \hline\et\]
160
161 For the sake of clarity, the rest of this section shows the syntax of
162 expressions without their precedences.
163
164 \subsection{Errors}
165 \label{basic-errors}\index{error}
166 Errors during expression evaluation, denoted by "\bot"\index{"\bot"},
167 are indistinguishable by a Haskell program from non-termination.  Since \Haskell{} is a
168 lazy language, all \Haskell{} types include "\bot".  That is, a value
169 of any type may be bound to a computation that, when demanded, results
170 in an error.  When evaluated, errors cause immediate program
171 termination and cannot be caught by the user.  The Prelude provides
172 two functions to directly 
173 cause such errors:
174 \bprog
175 @
176 error     :: String -> a
177 undefined :: a
178 @
179 \eprog
180 \indextt{error}
181 \indextt{undefined}
182 A call to @error@ terminates execution of
183 the program and returns an appropriate error indication to the
184 operating system.  It should also display the string in some
185 system-dependent manner.  When @undefined@ is used, the error message
186 is created by the compiler.
187
188 Translations of \Haskell{} expressions use @error@ and @undefined@ to
189 explicitly indicate where execution time errors may occur.  The actual
190 program behavior when an error occurs is up to the implementation.
191 The messages passed to the @error@ function in these translations are
192 only suggestions; implementations may choose to display more or less
193 information when an error occurs.
194
195 \subsection{Variables, Constructors, Operators, and Literals}
196 %
197 @@@
198 aexp    ->  qvar                                & (\tr{variable})
199         |   gcon                                & (\tr{general constructor})
200         |   literal                             
201 @@@
202 \indexsyn{var}%
203 \indexsyn{con}%
204 \indexsyn{varop}%
205 \indexsyn{conop}%
206 \indexsyn{op}%
207 @@@
208 gcon    ->  @()@
209         |   @[]@
210         |   @(,@\{@,@\}@)@
211         |   qcon
212
213 var     ->  varid | @(@ varsym @)@              & (\tr{variable})
214 qvar    ->  qvarid | @(@ qvarsym @)@            & (\tr{qualified variable})
215 con     ->  conid | @(@ consym @)@              & (\tr{constructor})
216 qcon    ->  qconid | @(@ gconsym @)@            & (\tr{qualified constructor})
217 varop   ->  varsym | \bkqB varid \bkqA          & (\tr{variable operator})
218 qvarop  ->  qvarsym | \bkqB qvarid \bkqA        & (\tr{qualified variable operator})
219 conop   ->  consym | \bkqB conid \bkqA          & (\tr{constructor operator})
220 qconop  ->  gconsym | \bkqB qconid \bkqA        & (\tr{qualified constructor operator})
221 op      ->  varop | conop                       & (\tr{operator})
222 qop     ->  qvarop | qconop                     & (\tr{qualified operator})
223 gconsym ->  @:@ | qconsym
224 @@@
225 \indexsyn{gcon}%
226 \indexsyn{var}%
227 \indexsyn{qvar}%
228 \indexsyn{con}%
229 \indexsyn{qcon}%
230 \indexsyn{varop}%
231 \indexsyn{qvarop}%
232 \indexsyn{conop}%
233 \indexsyn{qconop}%
234 \indexsyn{qop}%
235 \indexsyn{gconsym}%
236
237 \Haskell{} provides special syntax to support infix notation.
238 An {\em operator} is a function that can be applied using infix 
239 syntax (Section~\ref{operators}), or partially applied using a
240 {\em section} (Section~\ref{sections}).
241
242 An {\em operator} is either an {\em operator symbol}, such as @+@ or @$$@,
243 or is an ordinary identifier enclosed in grave accents (backquotes), such
244 as \bkqB@op@\bkqA.  For example, instead of writing the prefix application
245 @op x y@, one can write the infix application \mbox{@x@ \bkqB@op@\bkqA@ y@}.
246 If no fixity\index{fixity}
247 declaration is given for \bkqB@op@\bkqA{} then it defaults
248 to highest precedence and left associativity
249 (see Section~\ref{fixity}).
250
251 Dually, an operator symbol can be converted to an ordinary identifier
252 by enclosing it in parentheses.  For example, @(+) x y@ is equivalent
253 to @x + y@, and @foldr (*) 1 xs@ is equivalent to @foldr (\x y -> x*y) 1 xs@.
254
255 %       This para is covered by Section 2.4 and 5.5.1
256 % A qualified name may only be used to refer to a variable or
257 % constructor imported from another module (see Section~\ref{import}), or
258 % defined at the top level, 
259 % but not in the definition of a new variable or constructor.  Thus
260 % \bprog
261 % let F.x = 1 in F.x   -- invalid
262 % \eprog
263 % incorrectly uses a qualifier in the definition of @x@, regardless of
264 % the module containing this definition.  Qualification does not affect
265 % the nature of an operator: @F.+@ is an infix operator just as @+@ is.
266
267 Special syntax is used to name some constructors for some of the
268 built-in types, as found
269 in the production for "gcon" and "literal".  These are described
270 in Section~\ref{basic-types}.
271
272 \index{number!translation of literals}
273 An integer literal represents the
274 application of the function @fromInteger@\indextt{fromInteger} to the
275 appropriate value of type 
276 @Integer@.  Similarly, a floating point literal stands for an application of
277 @fromRational@\indextt{fromRational} to a value of type @Rational@ (that is, 
278 @Ratio Integer@).
279
280 \outline{
281 \paragraph*{Translation:}
282 The integer literal "i" is equivalent to @fromInteger@ "i",
283 where @fromInteger@ is a method in class @Num@ (see Section
284 \ref{numeric-literals}).\indexclass{Num}
285
286
287 The floating point literal "f" is equivalent to @fromRational@
288 ("n" @Ratio.%@ "d"), where @fromRational@ is a method in class @Fractional@
289 and @Ratio.%@ constructs a rational from two integers, as defined in
290 the @Ratio@ library.\indexclass{Fractional}
291 The integers "n" and "d" are chosen so that "n/d = f".
292 }
293
294
295 \subsection{Curried Applications and Lambda Abstractions}
296 \label{applications}
297 \label{lambda-abstractions}
298 \index{lambda abstraction}
299 \index{application}
300 %\index{function application|see{application}}
301 %
302 @@@
303 fexp    ->  [fexp] aexp                         & (\tr{function application})
304 exp     ->  @\@ apat_1 ... apat_n @->@ exp      & (\tr{lambda abstraction}, n>=1)
305 @@@
306 \indexsyn{exp}%
307 \indexsyn{fexp}%
308
309 \noindent
310 {\em Function application}\index{application} is written 
311 "e_1 e_2".  Application associates to the left, so the
312 parentheses may be omitted in @(f x) y@.  Because "e_1" could
313 be a data constructor, partial applications of data constructors are
314 allowed. 
315
316 {\em Lambda abstractions} are written 
317 "@\@ p_1 ... p_n @->@ e", where the "p_i" are {\em patterns}.
318 An expression such as @\x:xs->x@ is syntactically incorrect;
319 it may legally be written as @\(x:xs)->x@.
320
321 The set of patterns must be {\em linear}\index{linearity}%
322 \index{linear pattern}---no variable may appear more than once in the set.
323
324 \outline{
325 \paragraph*{Translation:}
326 The following identity holds:
327 \begin{center}
328 \bt{lcl}%
329 \struthack{17pt}%
330 "@\@ p_1 ... p_n @->@ e"
331          & "=" &
332         "@\@ x_1 ... x_n @-> case (@x_1@,@ ...@,@ x_n@) of (@p_1@,@ ...@,@ p_n@) ->@ e"
333 \et
334 \end{center}
335 where the "x_i" are new identifiers.
336 }
337 Given this translation combined with the semantics of case
338 expressions and pattern matching described in
339 Section~\ref{case-semantics}, if the
340 pattern fails to match, then the result is "\bot".
341
342              
343 \subsection{Operator Applications}
344 \index{operator application}
345 %\index{operator application|hseealso{application}}
346 \label{operators}
347 %
348 @@@
349 exp     ->  exp_1 qop exp_2
350         |   @-@ exp                             & (\tr{prefix negation})
351 qop     ->  qvarop | qconop                     & (\tr{qualified operator})
352 @@@
353 \indexsyn{exp}%
354 \indexsyn{qop}%
355
356 \noindent
357 The form "e_1 qop e_2" is the infix application of binary
358 operator\index{operator} "qop" to expressions "e_1" and "e_2".  
359
360 The special
361 form "@-@e" denotes prefix negation\index{negation}, the only
362 prefix operator in \Haskell{}, and is 
363 syntax for "@negate @(e)".\indextt{negate}  The binary @-@ operator
364 does not necessarily refer 
365 to the definition of @-@ in the Prelude; it may be rebound 
366 by the module system.  However, unary @-@ will always refer to the
367 @negate@ function defined in the Prelude.  There is no link between
368 the local meaning of the @-@ operator and unary negation.
369
370 Prefix negation has the same precedence as the infix operator @-@
371 defined in the Prelude (see
372 Table~\ref{prelude-fixities}%
373 %*ignore
374 , page~\pageref{prelude-fixities}%
375 %*endignore
376 ).  Because @e1-e2@ parses as an
377 infix application of the binary operator @-@, one must write @e1(-e2)@ for
378 the alternative parsing.  Similarly, @(-)@ is syntax for 
379 @(\ x y -> x-y)@, as with any infix operator, and does not denote 
380 @(\ x -> -x)@---one must use @negate@ for that.
381
382 \outline{
383 \paragraph*{Translation:}
384 The following identities hold:
385 \begin{center}
386 \bt{lcl}%
387 \struthack{17pt}%
388 "e_1 op e_2" & "=" & "@(@op@)@ e_1 e_2" \\
389 "@-@e" & "=" & "@negate@ (e)"
390 \et
391 \end{center}
392 }
393
394 \subsection{Sections}
395 \index{section}
396 %\index{section|hseealso{operator application}}
397 \label{sections}
398 %
399 @@@
400 aexp    ->  @(@ exp qop @)@ 
401         |   @(@ qop exp @)@
402 @@@
403 \indexsyn{aexp}%
404
405 \noindent
406 {\em Sections} are written as "@(@ op e @)@" or "@(@ e op @)@", where
407 "op" is a binary operator and "e" is an expression.  Sections are a
408 convenient syntax for partial application of binary operators.
409
410 Syntactic precedence rules apply to sections as follows.
411 "@(@op~e@)@" is legal if and only if "@(x@~op~e@)@" parses 
412 in the same way as "@(x@~op~@(@e@))@";
413 and similarly for  "@(@e~op@)@".
414 For example, @(*a+b)@ is syntactically invalid, but @(+a*b)@ and
415 @(*(a+b))@ are valid.  Because @(+)@ is left associative, @(a+b+)@ is syntactically correct,
416 but @(+a+b)@ is not; the latter may legally be written as @(+(a+b))@.
417
418 Because @-@ is treated specially in the grammar,
419 "@(-@ exp@)@" is not a section, but an application of prefix
420 negation,\index{negation} as
421 described in the preceding section.  However, there is a @subtract@
422 function defined in the Prelude such that
423 "@(subtract@ exp@)@" is equivalent to the disallowed section.
424 The expression "@(+ (-@ exp@))@" can serve the same purpose.
425
426 % Changed to allow postfix operators.  That is, in (op x), we no
427 % longer add a \x -> which would require op to be binary instead
428 % of unary.
429
430 \outline{
431 \paragraph*{Translation:}
432 The following identities hold:
433 \begin{center}
434 \bt{lcl}%
435 \struthack{17pt}%
436 "@(@op e@)@" & "=" & "@\@ x @->@ x op e" \\
437 "@(@e op@)@" & "=" & "@\@ x @->@ e op x"
438 \et
439 \end{center}
440 where "op" is a binary operator, "e" is an expression, and "x" is a variable
441 that does not occur free in "e".
442 }
443
444 \subsection{Conditionals}
445 \label{conditionals}\index{conditional expression}
446 %
447 @@@
448 exp     ->  @if@ exp_1 @then@ exp_2 @else@ exp_3
449 @@@
450 \indexsyn{exp}%
451
452 %\indextt{if ... then ... else ...}
453 A {\em conditional expression}
454 \index{conditional expression}
455 has the form 
456 "@if@ e_1 @then@ e_2 @else@ e_3" and returns the value of "e_2" if the
457 value of "e_1" is @True@, "e_3" if "e_1" is @False@, and "\bot"
458 otherwise.
459
460 \outline{
461 \paragraph*{Translation:}
462 The following identity holds:
463 \begin{center}
464 \bt{lcl}%
465 \struthack{17pt}%
466 "@if@ e_1 @then@ e_2 @else@ e_3"  & "=" & "@case@ e_1 @of { True ->@ e_2 @; False ->@ e_3 @}@"
467 \et
468 \end{center}
469 where @True@ and @False@ are the two nullary constructors from the 
470 type @Bool@, as defined in the Prelude.  The type of "e_1" must be @Bool@;
471 "e_2" and "e_3" must have the same type, which is also the type of the
472 entire conditional expression.
473 }
474
475 \subsection{Lists}
476 \label{lists}
477 %
478 @@@
479 exp     ->  exp_1 qop exp_2
480 aexp    ->  @[@ exp_1 @,@ ... @,@ exp_k @]@     & (k>=1)
481         |   gcon
482 gcon    -> @[]@
483         | qcon
484 qcon    -> @(@ gconsym @)@
485 qop     -> qconop
486 qconop  -> gconsym
487 gconsym -> @:@
488 @@@
489 \indexsyn{aexp}%
490
491 {\em Lists}\index{list} are written "@[@e_1@,@ ...@,@ e_k@]@", where
492 "k>=1".  The list constructor is @:@, and the empty list is denoted @[]@.
493 Standard operations on
494 lists are given in the Prelude (see Section~\ref{basic-lists}, and
495 Appendix~\ref{stdprelude} notably Section~\ref{preludelist}).
496
497 \outline{
498 \paragraph*{Translation:}  
499 The following identity holds:
500 \begin{center}
501 \bt{lcl}%
502 \struthack{17pt}%
503 "@[@e_1@,@ ...@,@ e_k@]@"  & "=" & "e_1 @: (@e_2 @: (@ ... @(@e_k @: [])))@"
504 \et
505 \end{center}
506 where @:@ and @[]@ are constructors for lists, as defined in
507 the Prelude (see Section~\ref{basic-lists}).  The types
508 of "e_1" through "e_k" must all be the same (call it "t\/"), and the
509 type of the overall expression is @[@"t"@]@ (see Section~\ref{type-syntax}).
510 }
511 The constructor ``@:@'' is reserved solely for list construction; like
512 @[]@, it is considered part of the language syntax, and cannot be hidden or redefined.
513
514 \subsection{Tuples}
515 \label{tuples}
516 %
517 @@@
518 aexp    ->  @(@ exp_1 @,@ ... @,@ exp_k @)@     & (k>=2)
519         | qcon
520 qcon -> @(,@\{@,@\}@)@
521
522 @@@
523 \indexsyn{aexp}%
524
525 {\em Tuples}\index{tuple} are written "@(@e_1@,@ ...@,@ e_k@)@", and may be
526 of arbitrary length "k>=2".  The constructor for an "n"-tuple is denoted by
527 @(,@\ldots@,)@, where there are "n-1" commas.  Thus @(a,b,c)@ and
528 @(,,) a b c@ denote the same value.
529 Standard operations on tuples are given
530 in the Prelude (see Section~\ref{basic-tuples} and Appendix~\ref{stdprelude}).
531
532 \outline{
533 \paragraph*{Translation:}  
534 "@(@e_1@,@ ...@,@ e_k@)@" for "k\geq2" is an instance of a "k"-tuple as
535 defined in the Prelude, and requires no translation.  If
536 "t_1" through "t_k" are the types of "e_1" through "e_k",
537 respectively, then the type of the resulting tuple is 
538 "@(@t_1@,@ ...@,@ t_k@)@" (see Section~\ref{type-syntax}).
539 }
540
541 \subsection{Unit Expressions and Parenthesized Expressions}
542 \label{unit-expression}
543 \index{unit expression}
544 %
545 @@@
546 aexp    ->  gcon
547         |   @(@ exp @)@
548 gcon    -> @()@
549 @@@
550 \indexsyn{aexp}%
551
552 \noindent
553 The form "@(@e@)@" is simply a {\em parenthesized expression}, and is
554 equivalent to "e".  The {\em unit expression} @()@ has type
555 @()@\index{trivial type} (see
556 Section~\ref{type-syntax}).  It is the only member of that type apart
557 from $\bot$, and can
558 be thought of as the ``nullary tuple'' (see Section~\ref{basic-trivial}).
559 \nopagebreak[4]
560
561 \outline{
562 \paragraph{Translation:}  
563 "@(@e@)@" is equivalent to "e".
564 }
565
566 \subsection{Arithmetic Sequences}
567 \label{arithmetic-sequences}
568 %
569 @@@
570 aexp    ->  @[@ exp_1 [@,@ exp_2] @..@ [exp_3] @]@      
571 @@@
572 \indexsyn{aexp}%
573
574 \noindent
575
576
577 The {\em arithmetic sequence}\index{arithmetic sequence}
578 "@[@e_1@,@ e_2 @..@ e_3@]@" denotes a list of values of
579 type "t", where each of the "e_i" has type "t", and "t" is an
580 instance of class @Enum@.
581
582 \outline{
583 \paragraph{Translation:}
584 Arithmetic sequences satisfy these identities:
585 \begin{center}
586 \begin{tabular}{lcl}%
587 \struthack{17pt}%
588 @[ @"e_1"@.. ]@         & "=" 
589                         & @enumFrom@ "e_1" \\
590 @[ @"e_1"@,@"e_2"@.. ]@ & "=" 
591                         & @enumFromThen@ "e_1" "e_2" \\
592 @[ @"e_1"@..@"e_3"@ ]@  & "=" 
593                         & @enumFromTo@ "e_1" "e_3" \\
594 @[ @"e_1"@,@"e_2"@..@"e_3"@ ]@ 
595                         & "=" 
596                         & @enumFromThenTo@ "e_1" "e_2" "e_3"
597 \end{tabular}
598 \end{center}
599 where @enumFrom@, @enumFromThen@, @enumFromTo@, and @enumFromThenTo@
600 are class methods in the class @Enum@ as defined in the Prelude
601 (see Figure~\ref{standard-classes}%
602 %*ignore
603 , page~\pageref{standard-classes}%
604 %*endignore
605 ).
606 }
607
608 The semantics of arithmetic sequences therefore depends entirely
609 on the instance declaration for the type "t".  We give here the
610 semantics for @Prelude@ types, and indications of the expected semantics
611 for other, user-defined, types.
612
613 For the types @Int@ and @Integer@, arithmetic sequences have the following
614 meaning:
615 \begin{itemize}
616 \item The sequence "@[@e_1@..]@" is the list "@[@e_1@,@e_1+1@,@e_1+2@,@...@]@".
617
618 \item The sequence "@[@e_1@,@e_2@..]@" is the list "@[@e_1@,@e_1+i@,@e_1+2i@,@...@]@",
619 where the increment, "i", is "e_2-e_1".  The increment may be zero or negative.
620 If the increment is zero, all the list elements are the same.
621
622 \item The sequence "@[@e_1@..@e_3@]@" is the list "@[@e_1@,@e_1+1@,@e_1+2@,@...e_3@]@".
623 The list is empty if "e_1 > e_3".
624
625 \item The sequence "@[@e_1@,@e_2@..@e_3@]@" 
626 is the list "@[@e_1@,@e_1+i@,@e_1+2i@,@...e_3@]@",
627 where the increment, "i", is "e_2-e_1".  If the increment 
628 is positive or zero, the list terminates when the next element would
629 be greater than "e_3"; the list is empty if "e_1 > e_3".
630 If the increment is negative, the list terminates when the next element would
631 be less than "e_3"; the list is empty if "e1 < e_3".
632 \end{itemize}
633 For other {\em discrete} @Prelude@ types "t" that 
634 are instances of @Enum@, namely @()@, @Bool@, @Char@ and @Ordering@,
635 the semantics is given by mapping the "e_i" to @Int@ using @fromEnum@,
636 using the above rules, and then mapping back to "t" with @toEnum@.
637
638 Where the type is also an instance of class @Bounded@ 
639 and "e_3" is omitted, an implied "e_3" is added
640 of @maxBound@ (if the increment is positive) or @minBound@ (resp. negative).
641 For example, @['a'..'z']@ denotes
642 the list of lowercase letters in alphabetical order, and @[LT..]@ is the
643 list @[LT,EQ,GT]@.
644
645 For {\em continuous} @Prelude@ types that are instances of @Enum@,
646 namely @Float@ and @Double@, the semantics is given by the rules for @Int@,
647 except that the list terminates when the elements become greater than
648 "e_3+i/2" for positive increment "i", or when they become less than 
649 "e_3+i/2" for negative "i".
650
651 See Figure~\ref{standard-classes}%
652 %*ignore
653 , page~\pageref{standard-classes}
654 %*endignore
655  and Section~\ref{derived-decls} for more details of which @Prelude@
656 type are in @Enum@.
657
658
659 \subsection{List Comprehensions}
660 \index{list comprehension}
661 \index{let expression!in list comprehensions}
662 \label{list-comprehensions}
663 %
664 @@@
665 aexp    -> @[@ exp @|@ qual_1 @,@ ... @,@ qual_n @]@    & (\tr{list comprehension}, n>=1)
666 qual    -> pat @<-@ exp         & (\tr{generator})
667          | @let@ decls          & (\tr{local declaration})
668          | exp                  & (\tr{guard})
669 @@@
670 \indexsyn{aexp}
671 \indexsyn{qual}
672
673 \noindent
674 A {\em list comprehension} has the form "@[@ e @|@ q_1@,@ ...@,@ q_n @]@,
675 n>=1," where the "q_i" qualifiers\index{qualifier} are either
676 \begin{itemize}
677 \item {\em generators}\index{generator} of the form "p @<-@ e", where
678 "p" is a 
679 pattern (see Section~\ref{pattern-matching}) of type "t" and "e" is an
680 expression of type "@[@t@]@"
681 \item {\em guards},\index{guard} which are arbitrary expressions of
682 type @Bool@ 
683 \item {\em local bindings} that provide new definitions for use in
684 the generated expression "e" or subsequent guards and generators.
685 \end{itemize}
686
687 Such a list comprehension returns the list of elements
688 produced by evaluating "e" in the successive environments
689 created by the nested, depth-first evaluation of the generators in the
690 qualifier list.  Binding of variables occurs according to the normal
691 pattern matching rules (see Section~\ref{pattern-matching}), and if a
692 match fails then that element of the list is simply skipped over.  Thus:\nopagebreak[4]
693 \bprog
694 @
695 [ x |  xs   <- [ [(1,2),(3,4)], [(5,4),(3,2)] ], 
696       (3,x) <- xs ]
697 @
698 \eprog
699 yields the list @[4,2]@.  If a qualifier is a guard, it must evaluate
700 to @True@ for the previous pattern match to succeed.  
701 As usual, bindings in list comprehensions can shadow those in outer
702 scopes; for example:
703 \[\ba{lll}
704 @[ x | x <- x, x <- x ]@ & = & @[ z | y <- x, z <- y]@ \\
705 \ea\]
706 \outline{
707 \paragraph{Translation:}
708 List comprehensions satisfy these identities, which may be
709 used as a translation into the kernel:
710 \begin{center}
711 \bt{lcl}%
712 \struthack{17pt}%
713 "@[ @ e@ | True ]@" & = & "@[@e@]@" \\
714 "@[ @ e@ | @q@ ]@" & = & "@[@~ e~@|@~q@, True ]@" \\
715 "@[ @ e@ | @b@,@~ Q ~@]@" & = &
716         "@if@~b~@then@~@[ @ e@ | @Q@ ]@~@else []@" \\
717 "@[ @ e@ | @p @<-@ l@,@~ Q@ ]@" & = &
718         "@let ok@~p~@=@~@[ @ e@ | @Q@ ]@" \\
719 &&       @    ok _ = []@ \\
720 &&      "@in concatMap ok@~ l" \\
721 "@[ @ e@ | let@~decls@,@~ Q@ ]@" & = &
722         "@let@~decls~@in@~@[ @ e@ | @Q@ ]@"
723 \et
724 \end{center}
725 where "e" ranges over expressions, "p" over
726 patterns, "l" over list-valued expressions, "b" over
727 boolean expressions, "decls" over declaration lists, 
728 "q" over qualifiers, and "Q" over sequences of qualifiers.  "@ok@" is a fresh variable.
729 The function @concatMap@, and boolean value @True@, are defined in the Prelude.
730 }
731
732 As indicated by the translation of list comprehensions, variables
733 bound by @let@ have fully polymorphic types while those defined by
734 @<-@ are lambda bound and are thus monomorphic (see Section
735 \ref{monomorphism}).
736
737 \subsection{Let Expressions}
738 \index{let expression}
739 \label{let-expressions}
740 %
741 % Including this syntax blurb does REALLY bad things to page breaking
742 % in the 1.[12] report (sigh); ToDo: hope it goes away.
743 @@@
744 exp     ->  @let@ decls @in@ exp
745 @@@
746 \indexsyn{exp}
747 \index{declaration!within a {\tt let} expression}
748
749 \noindent
750 {\em Let expressions} have the general form
751 "@let {@ d_1 @;@ ...  @;@ d_n @} in@ e",
752 and introduce a
753 nested, lexically-scoped, 
754 mutually-recursive list of declarations (@let@ is often called @letrec@ in
755 other languages).  The scope of the declarations is the expression "e"
756 and the right hand side of the declarations.  Declarations are
757 described in Section~\ref{declarations}.  Pattern bindings are matched
758 lazily; an implicit @~@ makes these patterns
759 irrefutable.\index{irrefutable pattern}
760 For example, 
761 \bprog
762 @
763 let (x,y) = undefined in @"e"@
764 @
765 \eprog
766 does not cause an execution-time error until @x@ or @y@ is evaluated.
767
768 \outline{
769 \paragraph*{Translation:} The dynamic semantics of the expression 
770 "@let {@ d_1 @;@ ...  @;@ d_n @} in@ e_0" are captured by this
771 translation: After removing all type signatures, each
772 declaration "d_i" is translated into an equation of the form 
773 "p_i @=@ e_i", where "p_i" and "e_i" are patterns and expressions
774 respectively, using the translation in
775 Section~\ref{function-bindings}.  Once done, these identities
776 hold, which may be used as a translation into the kernel:
777 \begin{center}
778 \bt{lcl}%
779 \struthack{17pt}%
780 @let {@"p_1"@ = @"e_1"@; @ ... @; @"p_n"@ = @"e_n"@} in@ "e_0"
781       &=& @let (~@"p_1"@,@ ... @,~@"p_n"@) = (@"e_1"@,@ ... @,@"e_n"@) in@ "e_0" \\
782 @let @"p"@ = @"e_1" @ in @ "e_0"
783         &=& @case @"e_1"@ of ~@"p"@ -> @"e_0"   \\
784         & & {\rm where no variable in "p" appears free in "e_1"} \\
785 @let @"p"@ = @"e_1" @ in @ "e_0"
786       &=& @let @"p"@ = fix ( \ ~@"p"@ -> @"e_1"@) in@ "e_0"
787 \et
788 \end{center}
789 where @fix@ is the least fixpoint operator.  Note the use of the
790 irrefutable patterns "@~@p".  This translation
791 does not preserve the static semantics because the use of @case@
792 precludes a fully polymorphic typing of the bound variables.
793 %\folks{Needs work -- KH}
794 % This same semantics applies to the top-level of
795 %a program that has been translated into a @let@ expression,
796 % as described at the beginning of Section~\ref{modules}.
797 The static semantics of the bindings in a @let@ expression
798 are described in 
799 Section~\ref{pattern-bindings}.
800 }
801
802 \subsection{Case Expressions}
803 \label{case}
804 %
805 @@@
806 exp     ->  @case@ exp @of@ @{@ alts @}@
807 alts    ->  alt_1 @;@ ... @;@ alt_n             & (n>=0)
808 alt     ->  pat @->@ exp [@where@ decls]
809         |   pat gdpat [@where@ decls]
810         |                                       & (empty alternative)
811
812 gdpat   ->  gd @->@ exp [ gdpat ]
813 gd      ->  @|@ exp^0 
814 @@@
815 \indexsyn{exp}%
816 \indexsyn{alts}%
817 \indexsyn{alt}%
818 \indexsyn{gdpat}%
819 \indexsyn{gd}%
820
821 A {\em case expression}\index{case expression} has the general form
822 \[
823 "@case@ e @of { @p_1 match_1 @;@ ... @;@ p_n  match_n @}@"
824 \]
825 where each "match_i" is of the general form
826 \[\ba{lll}
827  & "@|@ g_{i1}"   & "@->@ e_{i1}" \\
828  & "..." \\
829  & "@|@ g_{im_i}" & "@->@ e_{im_i}" \\
830  & \multicolumn{2}{l}{"@where@ decls_i"}
831 \ea\]
832 (Notice that in the syntax rule for "gd", the ``@|@'' is a 
833 terminal symbol, not the syntactic metasymbol for alternation.)
834 Each alternative "p_i match_i" consists of a 
835 pattern\index{pattern} "p_i" and its matches, "match_i".
836 Each match in turn
837 consists of a sequence of pairs of guards\index{guard}
838 "g_{ij}" and bodies "e_{ij}" (expressions), followed by
839 optional bindings ("decls_i") that scope over all of the guards and
840 expressions of the alternative.  An alternative of the form
841 \[
842 "pat @->@ exp @where@ decls"
843 \]
844 is treated as shorthand for:
845 \[\ba{lll}
846  & "pat @| True@"   & "@->@ exp" \\
847  & \multicolumn{2}{l}{"@where@ decls"}
848 \ea\]
849
850 A case expression must have at least one alternative and each alternative must
851 have at least one body.  Each body must have the same type, and the
852 type of the whole expression is that type.
853
854 A case expression is evaluated by pattern matching the expression "e"
855 against the individual alternatives.  The alternatives are tried
856 sequentially, from top to bottom.  If "e" matches the pattern in the
857 alternative, the guards for that alternative are tried sequentially
858 from top to bottom, in the environment of the case expression extended
859 by the bindings created during the matching of the pattern and by the
860 "decls_i" associated with that alternative.  If one of the guards
861 evaluates to @True@, the corresponding right-hand side is evaluated.
862 If all the guards evaluate to @False@, matching continues with the
863 next alternative.  If no match succeeds, the result is "\bot".
864 Pattern matching is described in Section~\ref{pattern-matching}, with
865 the formal semantics of case expressions in
866 Section~\ref{case-semantics}.
867
868 \subsection{Do Expressions}
869 \index{do expression}
870 \label{do-expressions}
871 \index{let expression!in do expressions}
872 \index{monad}
873 %
874 @@@
875 exp -> @do@ @{@ stmts @}@             & (\tr{do expression})
876 stmts -> stmt_1 ... stmt_n exp [@;@]  & \qquad (n>=0)
877 stmt -> exp @;@
878       | pat @<-@ exp @;@
879       | @let@ decls @;@
880       | @;@                     & (empty statement)
881 @@@
882 \indexsyn{exp}%
883 \indexsyn{stmt}%
884 \indexsyn{stmts}%
885
886 A {\em do expression} provides a more conventional syntax for monadic programming.
887 It allows an expression such as 
888 \bprog
889 @
890   putStr "x: "    >> 
891   getLine         >>= \l ->
892   return (words l)
893 @
894 \eprog
895 to be written in a more traditional way as:
896 \bprog
897 @
898   do putStr "x: "
899      l <- getLine
900      return (words l)
901 @
902 \eprog
903 \outline{
904 \paragraph*{Translation:} 
905 Do expressions satisfy these identities, which may be
906 used as a translation into the kernel, after eliminating empty "stmts":
907 \begin{center}
908 \bt{lcl}%
909 \struthack{17pt}%
910 @do {@"e"@}@                       &=& "e"\\
911 @do {@"e"@;@"stmts"@}@             &=& "e" @>> do {@"stmts"@}@ \\
912 @do {@"p"@ <- @"e"@; @"stmts"@}@   &=& @let ok @"p"@ = do {@"stmts"@}@\\
913                                    & & @    ok _ = fail "..."@\\
914                                    & & @  in @"e"@ >>= ok@ \\
915 @do {let@ "decls"@; @"stmts"@}@  &=& @let@ "decls" @in do {@"stmts"@}@\\
916 \et
917 \end{center}
918 The ellipsis @"..."@ stands for a compiler-generated error message,
919 passed to @fail@, preferably giving some indication of the location
920 of the pattern-match failure;
921 the functions @>>@, @>>=@, and @fail@ are operations in the class @Monad@,
922 as defined in the Prelude\indexclass{Monad}; and @ok@ is a fresh
923 identifier. 
924 }
925 As indicated by the translation of @do@, variables bound by @let@ have
926 fully polymorphic types while those defined by @<-@ are lambda bound
927 and are thus monomorphic.
928
929 \subsection{Datatypes with Field Labels}
930 \label{field-ops}
931 \index{data declaration@@{\tt data} declaration}
932 \index{label}
933 \index{field label|see{label}}
934 A datatype declaration may optionally include field labels for some or
935 all of the components of the type (see Section~\ref{datatype-decls}).
936 Readers unfamiliar with datatype declarations in \Haskell{} may wish
937 to read Section \ref{datatype-decls} first.
938 These field labels can be used to 
939 construct, select from, and update fields in a manner
940 that is independent of the overall structure of the datatype.
941
942 Different datatypes cannot share common field labels in the same scope.
943 A field label can be used at most once in a constructor.
944 Within a datatype, however, a field label can be used in more
945 than one constructor provided the field has the same typing in all
946 constructors. To illustrate the last point, consider:
947 @
948   data S = S1 { x :: Int } | S2 { x :: Int }   -- OK
949   data T = T1 { y :: Int } | T2 { y :: Bool }  -- BAD
950 @
951 Here @S@ is legal but @T@ is not, because @y@ is given 
952 inconsistent typings in the latter.
953
954 \subsubsection{Field Selection}
955 @@@
956 aexp ->     qvar
957 @@@
958 \index{field label!selection}
959
960 Field labels are used as selector functions.  When used as a variable,
961 a field label serves as a function that extracts the field from an
962 object.  Selectors are top level bindings and so they
963 may be shadowed by local variables but cannot conflict with 
964 other top level bindings of the same name.  This shadowing only
965 affects selector functions; in record construction (Section~\ref{record-construction}) 
966 and update (Section~\ref{record-update}), field labels
967 cannot be confused with ordinary variables. 
968
969 \outline{
970 \paragraph*{Translation:} 
971 A field label "f" introduces a selector function defined as:
972 \begin{center}
973 \bt{lcl}
974 \struthack{17pt}%
975 "f"@ x@ &=&@case x of {@ "C_1 p_{11} \ldots p_{1k}" @ -> @ "e_1" @;@ 
976  "\ldots" @;@ "C_n p_{n1} \ldots p_{nk}" @ -> @ "e_n" @}@\\
977 \et
978 \end{center}
979 where "C_1 \ldots C_n" are all the constructors of the datatype containing a
980 field labeled with "f", "p_{ij}" is @y@ when "f" labels the "j"th
981 component of "C_i" or @_@ otherwise, and "e_i" is @y@ when some field in
982 "C_i" has a label of "f" or @undefined@ otherwise.
983 }
984 \subsubsection{Construction Using Field Labels}
985 \label{record-construction}
986 \index{field label!construction}
987 @@@
988 aexp ->  qcon @{@ fbind_1 @,@ ... @,@ fbind_n @}@ & (\tr{labeled construction}, n>=0)
989 fbind   ->  qvar @=@ exp
990 @@@
991 \indexsyn{fbind}%
992
993 A constructor with labeled fields may be used to construct a value 
994 in which the components are specified by name rather than by position.
995 Unlike the braces used in declaration lists, these are not subject to
996 layout; the @{@ and @}@ characters must be explicit.  (This is also
997 true of field updates and field patterns.)
998 Construction using field labels is subject to the following constraints:
999 \begin{itemize}
1000 \item Only field labels declared with the specified constructor may be
1001 mentioned. 
1002 \item A field label may not be mentioned more than once.
1003 \item Fields not mentioned are initialized to $\bot$.
1004 \item A compile-time error occurs when any strict fields (fields
1005 whose declared types are prefixed by @!@) are omitted during
1006 construction.  Strict fields are discussed in Section~\ref{strictness-flags}.
1007 \end{itemize}
1008
1009 \outline{
1010 \paragraph*{Translation:} 
1011 In the binding "f" @=@ "v", the field "f" labels "v".
1012 \begin{center}
1013 \bt{lcl}
1014 \struthack{17pt}%
1015 "C" @{@ "bs" @}@ &=& "C (pick^C_1 bs @undefined@) \ldots (pick^C_k bs @undefined@)"\\
1016 \et
1017 \end{center}
1018 where "k" is the arity of "C".
1019
1020 The auxiliary function "pick^C_i bs d" is defined as follows:
1021 \begin{quote}
1022     If the "i"th component of a constructor "C" has the
1023     field label "f", and if "f=v" appears in the binding list
1024     "bs", then "pick^C_i bs d" is "v".  Otherwise, "pick^C_i bs d" is
1025     the default value "d".
1026 \end{quote}
1027 }
1028 \subsubsection{Updates Using Field Labels}
1029 \label{record-update}
1030 \index{field label!update}
1031 @@@
1032 aexp ->  aexp_{\langle{}qcon\rangle{}} @{@ fbind_1 @,@ ... @,@ fbind_n @}@ & (\tr{labeled update}, n>=1)
1033 @@@
1034
1035 Values belonging to a datatype with field labels may be
1036 non-destructively updated.  This creates a new value in which the
1037 specified field values replace those in the existing value.  
1038 Updates are restricted in the following ways:
1039 \begin{itemize}
1040 \item All labels must be taken from the same datatype.
1041 \item At least one constructor must define all of the labels
1042 mentioned in the update.
1043 \item No label may be mentioned more than once.
1044 \item An execution error occurs when the value being updated does
1045 not contain all of the specified labels.
1046 \end{itemize}
1047 \outline{
1048 \paragraph*{Translation:} 
1049 Using the prior definition of "pick",
1050 \begin{center}
1051 \bt{lcl}
1052 \struthack{17pt}%
1053 "e" @{@ "bs" @}@ &=& @case@ "e" @of@\\
1054 &&@        @"C_1 v_1 ... v_{k_1}" @->@ "C_1 (pick^{C_1}_1 bs v_1) ... (pick^{C_1}_{k_1} bs v_{k_1})"\\
1055 &&@            @ ... \\
1056 &&@        @"C_j v_1 ... v_{k_j}" @->@ "C_j (pick^{C_j}_1 bs v_1) ... (pick^{C_j}_{k_j} bs v_{k_j})"\\
1057 &&@        _ -> error "Update error"@\\
1058 \et
1059 \end{center}
1060 where "\{C_1,...,C_j\}" is the set of constructors containing all labels
1061 in "bs", and "k_i" is the arity of "C_i".
1062 }
1063 Here are some examples using labeled fields:
1064 \bprog
1065 @
1066 data T    = C1 {f1,f2 :: Int}
1067           | C2 {f1 :: Int,
1068                 f3,f4 :: Char}
1069 @
1070 \eprog
1071 \[\bt{|l|l|}%%b
1072 \hline
1073 Expression                                  & Translation                       \\
1074 \hline
1075 @C1 {f1 = 3}@                       & @C1 3 undefined@          \\
1076 @C2 {f1 = 1, f4 = 'A', f3 = 'B'}@   & @C2 1 'B' 'A'@            \\
1077 @x {f1 = 1}@                 & @case x of C1 _ f2    -> C1 1 f2@ \\
1078                              & @          C2 _ f3 f4 -> C2 1 f3 f4@   \\
1079 \hline\et\]
1080 The field @f1@ is common to both constructors in T.  This
1081 example translates expressions using constructors in field-label
1082 notation into equivalent expressions using the same constructors
1083 without field labels. 
1084 A compile-time error will result if no single constructor
1085 defines the set of field labels used in an update, such as
1086 @x {f2 = 1, f3 = 'x'}@. 
1087
1088 \subsection{Expression Type-Signatures}
1089 \index{expression type-signature}
1090 \label{expression-type-sigs}
1091 %
1092 @@@
1093 exp ->  exp @::@ [context @=>@] type
1094 @@@
1095 \indexsyn{exp}
1096 \indextt{::}
1097
1098 \nopagebreak[4]
1099 {\em Expression type-signatures} have the form "e @::@ t", where "e"
1100 is an expression and "t" is a type (Section~\ref{type-syntax}); they
1101 are used to type an expression explicitly
1102 and may be used to resolve ambiguous typings due to overloading (see
1103 Section~\ref{default-decls}).  The value of the expression is just that of
1104 "exp".  As with normal type signatures (see
1105 Section~\ref{type-signatures}), the declared type may be more specific than 
1106 the principal type derivable from "exp", but it is an error to give
1107 a type that is more general than, or not comparable to, the
1108 principal type.
1109 \outline{
1110 \paragraph*{Translation:} 
1111 \begin{center}
1112 \bt{lcl}
1113 \struthack{17pt}%
1114 "e @::@ t" & = & "@let {@ v @::@ t@; @ v @=@ e @} in @v"
1115 \et
1116 \end{center}
1117 }
1118
1119
1120 \subsection{Pattern Matching}
1121 \index{pattern-matching}
1122 \label{pattern-matching}
1123 \label{patterns}
1124
1125 {\em Patterns} appear in lambda abstractions, function definitions, pattern
1126 bindings, list comprehensions, do expressions, and case expressions.
1127 However, the 
1128 first five of these ultimately translate into case expressions, so
1129 defining the semantics of pattern matching for case expressions is sufficient.
1130 %it suffices to restrict the definition of the semantics of
1131 %pattern-matching to case expressions.
1132
1133 \subsubsection{Patterns}
1134 \label{pattern-definitions}
1135
1136 Patterns\index{pattern} have this syntax:
1137 @@@
1138 pat     ->  var @+@ integer            & (\tr{successor pattern})
1139         |   pat^0
1140 pat^i   ->  pat^{i+1} [qconop^{({\rm{n}},i)} pat^{i+1}]
1141         |   lpat^i
1142         |   rpat^i
1143 lpat^i  ->  (lpat^i | pat^{i+1}) qconop^{({\rm{l}},i)} pat^{i+1}
1144 lpat^6  ->  @-@ (integer | float)               & (\tr{negative literal})
1145 rpat^i  ->  pat^{i+1} qconop^{({\rm{r}},i)} (rpat^i | pat^{i+1})
1146 pat^{10}->  apat
1147         |   gcon apat_1 ... apat_k              & (\tr{arity} gcon = k, k>=1)
1148
1149 apat    ->  var [{\tt @@} apat]                 & (\tr{as pattern})
1150         |   gcon                                & (\tr{arity} gcon = 0) 
1151         |   qcon @{@ fpat_1 @,@ ... @,@ fpat_k @}@ & (\tr{labeled pattern}, k>=0)
1152         |   literal
1153         |   @_@                                 & (\tr{wildcard})
1154         |   @(@ pat @)@                         & (\tr{parenthesized pattern})
1155         |   @(@ pat_1 @,@ ... @,@ pat_k @)@     & (\tr{tuple pattern}, k>=2)
1156         |   @[@ pat_1 @,@ ... @,@ pat_k @]@     & (\tr{list pattern}, k>=1) 
1157         |   @~@ apat                            & (\tr{irrefutable pattern})
1158
1159 fpat    ->  qvar @=@ pat
1160 @@@
1161 \indexsyn{pat}%
1162 \index{pat@@"pat^i"}%
1163 \index{lpat@@"lpat^i"}%
1164 \index{rpat@@"rpat^i"}%
1165 \indexsyn{apat}%
1166 \indexsyn{fpats}%
1167 \indexsyn{fpat}%
1168
1169 The arity of a constructor must match the number of
1170 sub-patterns associated with it; one cannot match against a
1171 partially-applied constructor.
1172
1173 All patterns must be {\em linear}\index{linearity}
1174 \index{linear pattern}---no variable may appear more than once.  For
1175 example, this definition is illegal:
1176 @
1177   f (x,x) = x   -- ILLEGAL; x used twice in pattern
1178 @
1179
1180 Patterns of the form "var"{\tt @@}"pat" are called {\em as-patterns},
1181 \index{as-pattern ({\tt {\char'100}})}
1182 and allow one to use "var"
1183 as a name for the value being matched by "pat".  For example,\nopagebreak[4]
1184 \bprog
1185 @
1186 case e of { xs@@(x:rest) -> if x==0 then rest else xs }
1187 @
1188 \eprog
1189 is equivalent to:
1190 \bprog
1191 @
1192 let { xs = e } in
1193   case xs of { (x:rest) -> if x==0 then rest else xs }
1194 @
1195 \eprog
1196
1197 Patterns of the form @_@ are {\em
1198 wildcards}\index{wildcard pattern ({\tt {\char'137}})} and are useful when some part of a pattern
1199 is not referenced on the right-hand-side.  It is as if an
1200 identifier not used elsewhere were put in its place.  For example,
1201 \bprog
1202 @
1203 case e of { [x,_,_]  ->  if x==0 then True else False }
1204 @
1205 \eprog
1206 is equivalent to:
1207 \bprog
1208 @
1209 case e of { [x,y,z]  ->  if x==0 then True else False }
1210 @
1211 \eprog
1212 % where @y@ and @z@ are identifiers not used elsewhere.
1213
1214 %old:
1215 %This translation is also 
1216 %assumed prior to the semantics given below.
1217
1218 In the pattern matching rules given below we distinguish two kinds of
1219 patterns: an {\em irrefutable pattern}
1220 \index{irrefutable pattern}
1221 is: a variable, a wildcard, "N apat" where "N" is a constructor
1222 defined by @newtype@ and "apat" is irrefutable (see
1223 Section~\ref{datatype-renaming}), 
1224 \index{newtype declaration@@{\tt newtype} declaration} 
1225 "var"{\tt @@}"apat" where "apat" is irrefutable,
1226 or of the form "@~@apat" (whether or not "apat" is irrefutable).
1227 All other patterns are {\em refutable}.
1228 \index{refutable pattern}
1229
1230 \subsubsection{Informal Semantics of Pattern Matching}
1231
1232 Patterns are matched against values.  Attempting to match a pattern
1233 can have one of three results: it may {\em fail\/}; it may {\em
1234 succeed}, returning a binding for each variable in the pattern; or it
1235 may {\em diverge} (i.e.~return "\bot").  Pattern matching proceeds
1236 from left to right, and outside to inside, according to the following rules:
1237 \begin{enumerate}
1238 \item Matching a value "v" against the irrefutable pattern
1239 \index{irrefutable pattern}
1240 "var" always succeeds and binds "var" to "v".  
1241 Similarly, matching "v" against the irrefutable pattern "@~@apat" always succeeds.  
1242 The free
1243 variables in "apat" are bound to the appropriate values if matching
1244 "v" against "apat" would otherwise succeed, and to "\bot" if matching
1245 "v" against "apat" fails or diverges.  (Binding does {\em
1246 not} imply evaluation.)
1247
1248 Matching any value against the wildcard pattern @_@ always succeeds
1249 and no binding is done.
1250
1251 % Matching a value "con v" against the pattern "con apat" where "con" is an
1252 % abstract datatype constructor and "apat" is irrefutable always succeeds
1253 % and binds "var" to "v".  Matching "\bot" against the pattern "con apat" where
1254 % "con" is an abstract datatype constructor and "apat" is irrefutable always
1255 % succeeds and matches "\bot" to "apat".  
1256
1257 Operationally, this means that no matching is done on an
1258 irrefutable pattern until one of the variables in the pattern is used.
1259 At that point the entire pattern is matched against the value, and if
1260 the match fails or diverges, so does the overall computation.
1261
1262 \item
1263 Matching a value "con v" against the pattern "con pat", where "con" is a
1264 constructor defined by @newtype@, is equivalent to matching "v"
1265 against the pattern "pat".   That is, constructors associated with
1266 @newtype@ serve only to change the type of a value.\index{newtype declaration@@{\tt newtype} declaration}
1267
1268 \item Matching "\bot" against a refutable pattern always diverges.
1269 \index{refutable pattern}
1270
1271 \item Matching a non-"\bot" value can occur against three kinds of
1272 refutable patterns:
1273 \begin{enumerate}
1274 \item Matching a non-"\bot" value against a pattern whose outermost
1275 component is a constructor defined by @data@ 
1276 \index{constructed pattern}
1277 fails if the value being matched was created by a 
1278 different constructor.  If the constructors are
1279 the same, the result of the match is the result of matching the
1280 sub-patterns left-to-right against the components of the data value:
1281 if all matches succeed, the overall match
1282 succeeds; the first to fail or diverge causes the overall match to
1283 fail or diverge, respectively.  
1284
1285 %Also, literals (characters, positive and
1286 %negative integers, and the unit value @()@) are treated as nullary
1287 %constructors.
1288 \item Numeric literals are matched using the overloaded @==@ function.  
1289 The behavior of numeric patterns depends entirely on the definition of
1290 @==@ and @fromInteger@ (integer literals) or @fromRational@ (floating point literals)
1291 for the type of object being matched.
1292
1293 \item Matching a non-"\bot" value "x" against a pattern of the form
1294 "n@+@k"
1295 \index{n+k pattern@@"n@+@k" pattern}
1296 (where "n" is a variable and "k" is a positive integer
1297 literal) succeeds if "x>=k", resulting in the binding of "n" to "x-k",
1298 and fails if "x<k".  The behavior of "n@+@k" patterns depends entirely
1299 on the underlying definitions of @>=@, @fromInteger@, and @-@ for the
1300 type of the object being matched.
1301 \end{enumerate}
1302
1303 \item
1304 Matching against a constructor using labeled fields is the same as
1305 matching ordinary constructor patterns except that the fields are
1306 matched in the order they are named in the field list.  All fields
1307 listed must be declared by the constructor; fields may not be named
1308 more than once.  Fields not named by the pattern are ignored (matched
1309 against @_@).
1310
1311 \item
1312 The result of matching a value "v" against an as-pattern "var"{\tt @@}"apat" is
1313 \index{as-pattern ({\tt {\char'100}})}
1314 the result of matching "v" against "apat" augmented with the binding of
1315 "var" to "v".  If the match of "v" against "apat" fails or diverges,
1316 then so does the overall match.
1317 \end{enumerate}
1318
1319 Aside from the obvious static type constraints (for
1320 example, it is a static error to match a character against a
1321 boolean), the following static class constraints hold: an integer
1322 literal pattern
1323 \index{integer literal pattern}
1324 can only be matched against a value in the class
1325 @Num@ and a floating literal pattern
1326 \index{floating literal pattern}
1327 can only be matched against a value
1328 in the class @Fractional@.
1329 A "n@+@k" pattern
1330 \index{n+k pattern@@"n@+@k" pattern}
1331 can only be matched
1332 against a value in the class @Integral@.
1333
1334 Many people feel that "n@+@k" patterns should not be used.  These
1335 patterns may be removed or changed in future versions of \Haskell{}. 
1336
1337 Here are some examples:
1338 \begin{enumerate}
1339 \item If the pattern @['a','b']@ is matched against "@['x',@\bot@]@", then @'a'@
1340 "fails" to match against @'x'@, and the result is a failed match.  But
1341 if @['a','b']@ is matched against "@[@\bot@,'x']@", then attempting to match
1342 @'a'@ against "\bot" causes the match to "diverge".
1343
1344 \item These examples demonstrate refutable vs.~irrefutable
1345 matching:
1346 \bprog
1347 @
1348 (\ ~(x,y) -> 0) @"\bot"@    @"\Rightarrow"@    0
1349 (\  (x,y) -> 0) @"\bot"@    @"\Rightarrow"@    @"\bot"@
1350 @
1351 \eprog
1352 \bprog
1353 @
1354 (\ ~[x] -> 0) []    @"\Rightarrow"@    0
1355 (\ ~[x] -> x) []    @"\Rightarrow"@    @"\bot"@
1356 @
1357 \eprog
1358 \bprog
1359 @
1360 (\ ~[x,~(a,b)] -> x) [(0,1),@"\bot"@]    @"\Rightarrow"@    (0,1)
1361 (\ ~[x, (a,b)] -> x) [(0,1),@"\bot"@]    @"\Rightarrow"@    @"\bot"@
1362 @
1363 \eprog
1364 \bprog
1365 @
1366 (\  (x:xs) -> x:x:xs) @"\bot"@   @"\Rightarrow"@   @"\bot"@
1367 (\ ~(x:xs) -> x:x:xs) @"\bot"@   @"\Rightarrow"@   @"\bot"@:@"\bot"@:@"\bot"@
1368 @
1369 \eprogNoSkip
1370 \end{enumerate}
1371 \nopagebreak[4]
1372 % \bprog
1373 % @@
1374 % (\ t -> let (x,y) = t in 0) @@"\bot"@@    @@"\Rightarrow"@@    0
1375 % (\ (x,y) -> 0) @@"\bot"@@    @@"\Rightarrow"@@    @@"\bot"@@
1376 % @@
1377 % \eprog
1378 % \bprog
1379 % @@
1380 % (\ l -> let [x] = l in 0) []    @@"\Rightarrow"@@    0
1381 % (\ l -> let [x] = l in x) []    @@"\Rightarrow"@@    @@"\bot"@@
1382 % @@
1383 % \eprog
1384 % \bprog
1385 % @@
1386 % (\ l -> let [x,t] = l; (a,b) = t in x) [(0,1),@@"\bot"@@]    @@"\Rightarrow"@@    (0,1)
1387 % (\ l -> let [x, (a,b)] = l in x) [(0,1),@@"\bot"@@]    @@"\Rightarrow"@@    @@"\bot"@@
1388 % @@
1389 % \eprog
1390 % \bprog
1391 % @@
1392 % (\  (x:xs) -> x:x:xs) @@"\bot"@@   @@"\Rightarrow"@@   @@"\bot"@@
1393 % (\ l -> let (x:xs) = l in x:x:xs) @@"\bot"@@   @@"\Rightarrow"@@   @@"\bot"@@:@@"\bot"@@:@@"\bot"@@
1394 % @@
1395 % \eprogNoSkip
1396 % \end{enumerate}
1397 Additional examples illustrating some of the subtleties of pattern matching
1398 may be found in Section~\ref{datatype-renaming}.
1399
1400 Top level patterns in case
1401 expressions and the set of top level patterns in function or pattern
1402 bindings may have zero or more associated {\em guards}\index{guard}.
1403 A guard is 
1404 a boolean expression that is evaluated only after all of the
1405 arguments have been successfully matched, and it must be true for the
1406 overall pattern match to succeed.  The environment of the guard is the same
1407 as the right-hand-side of the case-expression
1408 alternative, function definition, or pattern binding to which it is attached.
1409
1410 The guard semantics have an obvious influence on the
1411 strictness characteristics of a function or case expression.  In
1412 particular, an otherwise irrefutable pattern
1413 \index{irrefutable pattern}
1414 may be evaluated because of a guard.  For example, in
1415 \bprog
1416 @
1417 f :: (Int,Int,Int) -> [Int] -> Int
1418 f ~(x,y,z) [a] | (a == y) = 1
1419 @
1420 \eprog
1421 % \bprog
1422 % @@
1423 % f t [a] | a==y = 1 
1424 %           where (x,y,z) = t
1425 % @@
1426 % \eprog
1427 both @a@ and @y@ will be evaluated by @&&@ in the guard.
1428
1429
1430 \subsubsection{Formal Semantics of Pattern Matching}
1431 \label{case-semantics}
1432
1433 The semantics of all pattern matching constructs other than @case@
1434 expressions are defined by giving identities that relate those
1435 constructs to @case@ expressions.  The semantics of
1436 @case@ expressions themselves are in turn given as a series of
1437 identities, in Figures~\ref{simple-case-expr-1}--\ref{simple-case-expr-2}. 
1438 Any implementation should behave so that these identities hold; it is 
1439 not expected that it will use them directly, since that 
1440 would generate rather inefficient code.
1441   
1442 \begin{figure}[tb]
1443 \outlinec{
1444 \begin{tabular}{@@{}cl}
1445 (a)&@case @$e$@ of { @$alts$@ } @$=$@ (\@$v$@ -> case @$v$@ of { @$alts$@ }) @"e"\\
1446 &{\rm where $v$ is a new variable}\\
1447 (b)&@case @$v$@ of { @$p_1\ \ match_1$@;  @$\ldots{}$@ ; @$p_n\ \ match_n$@ }@\\
1448    &$=$@  case @$v$@ of { @$p_1\ \ match_1$@ ;@\\
1449    &@                _  -> @$\ldots{}$@ case @$v$@ of {@\\
1450    &@                           @$p_n\ \ match_n$\ @;@\\
1451    &@                           _  -> error "No match" }@$\ldots$@}@\\
1452    &@ @{\rm where each $match_i$ has the form:}\\
1453    &@  | @$g_{i,1}$  @ -> @$e_{i,1}$@ ; @$\ldots{}$@ ; | @$g_{i,m_i}$@ -> @$e_{i,m_i}$@ where { @$decls_i$@ }@\\[4pt]
1454 %\\
1455 (c)&@case @$v$@ of { @$p$@ | @$g_1$@ -> @$e_1$@ ; @$\ldots{}$\\
1456    &\hspace*{4pt}@             | @$g_n$@ -> @$e_n$@ where { @$decls$@ }@\\
1457    &\hspace*{2pt}@            _     -> @$e'$@ }@\\
1458    &$=$@ case @$e'$@ of@\\
1459    &   @  {@$y$@ -> @     {\rm (where "y" is a new variable)}\\
1460  &@   case @$v$@ of {@\\
1461    &@         @$p$@ -> let { @$decls$@ } in@\\
1462    &@                if @$g_1$@ then @$e_1$@ @$\ldots{}$@ else if @$g_n$@ then @$e_n$@ else @$y$ \ @;@\\
1463    &@         _ -> @$y$@ }}@\\[4pt]
1464 %\\
1465 (d)&@case @$v$@ of { ~@$p$@ -> @$e$@; _ -> @$e'$@ }@\\
1466 &$=$@ (\@$x'_1$ $\ldots$ $x'_n$ @->@ $e_1$ @) (case @$v$@ of { @$p$@->@ 
1467 $x_1$@ })@ $\ldots$ @(case @$v$@ of { @$p$@ -> @$x_n$@})@\\
1468 &{\rm where $e_1$ = $e\,[x'_1/x_1, \ldots, x'_n/x_n]$}\\[2pt]
1469 &{\rm $x_1, \ldots, x_n$ are all the variables in $p\/$; $x'_1, \ldots, x'_n$ are new variables}\\[4pt]
1470 %\\
1471 (e)&@case @$v$@ of { @$x${\tt @@}$p$@ -> @$e$@; _ -> @$e'$@ }@\\
1472 &$=$@  case @$v$@ of { @$p$@ -> ( \ @$x$@ -> @$e$@ ) @$v$@ ; _ -> @$e'$@ }@\\[4pt]
1473 %\\
1474 (f)&@case @$v$@ of { _ -> @$e$@; _ -> @$e'$@ } @$=$@ @$e$\\[4pt]
1475 \end{tabular}
1476 }
1477 %**<div align=center> <h4>Figure 3</h4> </div>
1478 \ecaption{Semantics of Case Expressions, Part 1}
1479 \label{simple-case-expr-1}
1480 \end{figure}
1481
1482 \begin{figure}[tb]
1483 \outlinec{
1484 \begin{tabular}{@@{}cl}
1485 (g)&@case @$v$@ of { @$K\ p_1 \ldots p_n$@ -> @$e$@; _ -> @$e'$@ }@\\
1486 &$=$@ case @$v$@ of {@\\
1487 &@     @$K\ x_1 \ldots x_n$@ -> case @$x_1$@ of {@\\
1488 &@                    @$p_1$@ -> @$\ldots$@ case @$x_n$@ of { @$p_n$@ -> @$e$@ ; _ -> @$e'$@ } @$\ldots$\\
1489 &@                    _  -> @$e'$@ }@\\
1490 &@     _ -> @$e'$@ }@\\[2pt]
1491 &{\rm at least one of $p_1, \ldots, p_n$ is not a variable; $x_1, \ldots, x_n$ are new variables}\\[4pt]
1492 %\\
1493 (h)&@case @$v$@ of { @$k$@ -> @$e$@; _ -> @$e'$@ } @$=$@ if (@$v$@==@$k$@) then @$e$@ else @$e'$\\[4pt]
1494 %\\
1495 (i)&@case @$v$@ of { @$x$@ -> @$e$@; _ -> @$e'$@ } @$=$@ case @$v$@ of { @$x$@ -> @$e$@ }@\\[4pt]
1496 %\\
1497 (j)&@case @$v$@ of { @$x$@ -> @$e$@ } @$=$@ ( \ @$x$@ -> @$e$@ ) @$v$\\[4pt]
1498 %\\
1499 (k)&@case @$N$ $v$@ of { @$N$@ @$p$@ -> @$e$@; _ -> @$e'$@ }@\\
1500 &$=$@ case @$v$@ of { @$p$@ -> @$e$@; _ -> @$e'$@ }@\\
1501 &{\rm where $N$ is a @newtype@ constructor}\\[4pt]
1502 (l)&@case @$\bot$@ of { @$N$@ @$p$@ -> @$e$@; _ -> @$e'$@ } @$=$@ case @$\bot$@ of { @$p$@ -> @$e$@ }@\\
1503 &{\rm where $N$ is a @newtype@ constructor}\\[4pt]
1504 (m)& @case @ $v$ @ of { @ $K$ @ {@ $f_1$ @ = @ $p_1$ @ , @ $f_2$ @ = @
1505 $p_2$ @ , @ $\ldots$ @} -> @ $e$ @; _ -> @ $e'$ @ }@\\
1506 &$=$ @ case @$e'$@ of {@\\
1507 &@   @$y$@ ->@\\
1508 &@    case @ $v$ @ of { @\\
1509 &@     @ $K$ @ { @ $f_1$ @ = @ $p_1$ @ } ->@\\
1510 &@            case @ $v$ @ of {@ $K$ @ {@ $f_2$ @ = @ $p_2$ @ , @
1511 $\ldots$ @ } -> @ $e$ @; _ -> @ $y$ @ };@\\
1512 &@            _ -> @ $y$ @ }}@\\
1513 &{\rm where $f_1$, $f_2$, $\ldots$ are fields of constructor $K$; $y$
1514 is a new variable}\\[4pt]
1515 (n)&@case @ $v$ @ of { @ $K$ @ {@ $f$ @ = @ $p$ @} -> @ $e$ @; _ -> @
1516 $e'$ @ }@ \\
1517 &$=$@ case @ $v$ @ of {@\\
1518 &   @    @ $K$ $p_1\ \ldots \  p_n$ @ -> @ $e$ @; _ -> @ $e'$ @ }@\\
1519 &{\rm where $p_i$ is $p$ if $f$ labels the $i$th component of $K$,
1520 @_@ otherwise}\\
1521 (o)&@case @ $v$ @ of { @ $K$ @ {} -> @ $e$ @; _ -> @
1522 $e'$ @ }@ \\
1523 &$=$@ case @ $v$ @ of {@\\
1524 &   @    @ $K$ @_@ $\ldots$ @_ -> @ $e$ @; _ -> @ $e'$ @ }@\\
1525 (p)&@case (@$K'$@ @$e_1$@ @$\ldots$@ @$e_m$@) of { @$K$@ @$x_1$@ @$\ldots$@ @$x_n$@ -> @$e$@; _ -> @$e'$@ } @$=$@ @$e'$\\
1526 &{\rm where $K$ and $K'$ are distinct @data@ constructors of arity $n$ and $m$, respectively}\\[4pt]
1527 %\\
1528 (q)&@case (@$K$@ @$e_1$@ @$\ldots$@ @$e_n$@) of { @$K$@ @$x_1$@ @$\ldots$@ @$x_n$@ -> @$e$@; _ -> @$e'$@ }@\\
1529 &$=$@  case @$e_1$@ of { @$x'_1$@ -> @$\ldots$@  case @$e_n$@ of { @$x'_n$@ -> @$e[x'_1/x_1 \ldots x'_n/x_n]$@ }@$\ldots$@}@\\
1530 &{\rm where $K$ is a constructor of arity $n$; $x'_1 \ldots x'_n$ are new variables}\\[4pt]
1531 %(l)&@case (@$A$@ @$ e_1$@) of {@$A$@ @$ x_1$@ -> @$e$@; _ -> @$e'$@ }@\\
1532 %&$=$@ case @$e1$@ of { @$x_1$@ -> @$e$@ }@\\
1533 %&{\rm where $A$ is constructor defined by @newtype@}\\
1534 (r)&@case @$v$@ of { @$x$@+@$k$@ -> @$e$@; _ -> @$e'$@ }@\\
1535 &$=$@ if @$v$@ >= @$k$@ then let {@$x'$@ = @$v$@-@$k$@} in @$e[x'/x]$@ else @$e'$@ @($x'$ is a new variable)\\
1536 \end{tabular}
1537 }
1538 %**<div align=center> <h4>Figure 4</h4> </div>
1539 \ecaption{Semantics of Case Expressions, Part 2}
1540 \label{simple-case-expr-2}
1541 \end{figure}
1542
1543 In Figures~\ref{simple-case-expr-1}--\ref{simple-case-expr-2}:
1544 "e", "e'" and "e_i" are expressions; 
1545 "g" and "g_i" are boolean-valued expressions; 
1546 "p" and "p_i" are patterns; 
1547 "v", "x", and "x_i" are variables; 
1548 "K" and "K'" are algebraic datatype (@data@) constructors (including
1549 tuple constructors);  "N" is a @newtype@ constructor; \index{newtype declaration@@{\tt newtype} declaration}
1550 and "k" is a character, string, or numeric literal.
1551
1552 % For clarity, several rules are expressed using
1553 % @let@ (used only in a non-recursive way); their usual purpose is to
1554 % prevent name capture
1555 % (e.g., in rule~(c)).  The rules may be re-expressed entirely with
1556 % @cases@ by applying this identity:
1557 % \[
1558 % "@let @x@ = @y@ in @e@ @ =@  case @y@ of { @x@ -> @e@ }@"
1559 % \]
1560
1561 %Using all but the last two identities (rules~(n) and~(o)) in Figure~\ref{simple-case-expr-2}
1562 %in a left-to-right manner yields a translation into a
1563 %subset of general @case@ expressions called {\em simple case expressions}.%
1564 %\index{simple case expression}
1565 Rule~(b) matches a general source-language
1566 @case@ expression, regardless of whether it actually includes
1567 guards---if no guards are written, then @True@ is substituted for the guards "g_{i,j}"
1568 in the "match_i" forms.
1569 Subsequent identities manipulate the resulting @case@ expression into simpler
1570 and simpler forms.
1571 %The semantics of simple @case@ expressions is 
1572 %given by the last two identities ((n) and~(o)).
1573
1574 Rule~(h) in Figure~\ref{simple-case-expr-2} involves the
1575 overloaded operator @==@; it is this rule that defines the
1576 meaning of pattern matching against overloaded constants.
1577 \index{pattern-matching!overloaded constant}
1578
1579 %% When used as a translation, the identities in
1580 %% Figure~\ref{simple-case-expr} will generate a very inefficient
1581 %% program.  This can be fixed by using further @case@ or @let@ 
1582 %% expressions, but doing so 
1583 %% would clutter the identities, which are intended only to convey the semantics.
1584
1585 These identities all preserve the static semantics.  Rules~(d),~(e), and~(j)
1586 use a lambda rather than a @let@; this indicates that variables bound
1587 by @case@ are monomorphically typed (Section~\ref{type-semantics}).
1588 \index{monomorphic type variable}
1589
1590 %**~footer
1591
1592 % Local Variables: 
1593 % mode: latex
1594 % End: