Done while away at c-- workshop
[haskell-report.git] / report / exps.verb
1 %
2 % $Header: /home/cvs/root/haskell-report/report/exps.verb,v 1.5 2001/08/20 07:57:53 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 \Haskell{}
11 {\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.
15 Free variables and constructors used in these translations refer to
16 entities 
17 defined by the Prelude.  To avoid clutter,
18 \index{Prelude}
19 we use @True@ instead of
20 @Prelude.True@ or @map@ instead of @Prelude.map@. (@Prelude.True@ is a
21 "qualified name" as described in Section~\ref{import}.)
22
23 Free variables and constructors used in these translations
24 always refer to entities defined by the @Prelude@.
25 For example, ``@concatMap@'' used in the translation of list comprehensions 
26 (Section~\ref{list-comprehensions})
27 means the @concatMap@ defined by the @Prelude@, regardless of what is in scope
28 where the list comprehension is used.
29
30 In the syntax that follows, there are some families of nonterminals
31 indexed by precedence levels (written as a superscript).  Similarly, the
32 nonterminals "op", "varop", and "conop" may have a double index:
33 a letter "l", "r", or "n" for left-, right- or non-associativity and
34 a precedence level.  A precedence-level variable "i" ranges from 0 to 9;
35 an associativity variable "a" varies over "\{l, r, n\}".
36 For example
37 @@@
38 aexp    ->  @(@ exp^{i+1} qop^{(a,i)} @)@
39 @@@
40 actually stands for 30 productions, with 10 substitutions for "i"
41 and 3 for "a".
42
43 @@@
44 exp     ->  exp^0 @::@ [context @=>@] type      & (\tr{expression type signature})
45         |   exp^0
46 exp^i   ->  exp^{i+1} [qop^{({\rm{n}},i)} exp^{i+1}]
47         |   lexp^i
48         |   rexp^i
49 lexp^i  ->  (lexp^i | exp^{i+1}) qop^{({\rm{l}},i)} exp^{i+1}
50 lexp^6  ->  @-@ exp^7
51 rexp^i  ->  exp^{i+1} qop^{({\rm{r}},i)} (rexp^i | exp^{i+1})
52 exp^{10} ->  @\@ apat_1 ... apat_n @->@ exp     & (\tr{lambda abstraction}, n>=1)
53         |   @let@ decls @in@ exp                & ({\tr{let expression}})
54         |   @if@ exp @then@ exp @else@ exp      & (\tr{conditional})
55         |   @case@ exp @of@ @{@ alts  @}@       & (\tr{case expression})
56         |   @do@ @{@ stmts @}@                  & (\tr{do expression})
57         |   fexp
58 fexp    ->  [fexp] aexp                         & (\tr{function application})
59
60 aexp    ->  qvar                                & (\tr{variable})
61         |   gcon                                & (\tr{general constructor})
62         |   literal                             
63         |   @(@ exp @)@                       & (\tr{parenthesized expression})
64         |   @(@ exp_1 @,@ ... @,@ exp_k @)@     & (\tr{tuple}, k>=2)
65         |   @[@ exp_1 @,@ ... @,@ exp_k @]@     & (\tr{list}, k>=1)
66         |   @[@ exp_1 [@,@ exp_2] @..@ [exp_3] @]@ & (\tr{arithmetic sequence})
67         |   @[@ exp @|@ qual_1 @,@ ... @,@ qual_n @]@   & (\tr{list comprehension}, n>=1)
68         |   @(@ exp^{i+1} qop^{(a,i)} @)@        & (\tr{left section})
69         |   @(@ qop^{(a,i)} exp^{i+1} @)@        & (\tr{right section})
70         |   qcon @{@ fbind_1 @,@ ... @,@ fbind_n @}@ & (\tr{labeled construction}, n>=0)
71         |   aexp_{\{qcon\}} @{@ fbind_1 @,@ ... @,@ fbind_n @}@ & (\tr{labeled update}, n >= 1)
72
73 @@@
74 \indexsyn{exp}%
75 \index{exp@@"exp^i"}%
76 \index{lexp@@"lexp^i"}%
77 \index{rexp@@"rexp^i"}%
78 \indexsyn{aexp}%
79 \indexsyn{fexp}%
80
81 % As an aid to understanding this grammar,
82 % Table~\ref{syntax-precedences} shows the relative precedence of
83 % expressions, patterns and definitions, plus an extended associativity.
84 % "-" indicates that the item is non-associative.
85
86 % \begin{table}[tb]
87 % \[
88 % \centerline{
89 % \begin{tabular}{|l|c|}\hline
90 % Item                                          &       Associativity \\ 
91 % \hline
92 %                                               &                       \\
93 % simple terms, parenthesized terms               &     --              \\
94 % irrefutable patterns (@~@)                      &       --            \\
95 % as-patterns ({\tt @@})                          &       right         \\
96 % function application                          &       left            \\
97 % @do@, @if@, @let@, lambda(@\@), @case@ (leftwards)&   right           \\
98 % @case@ (rightwards)                           &       right           \\
99 %                                               &                       \\
100 % infix operators, prec. 9                      &       as defined      \\
101 % \ldots                                                &       \ldots          \\
102 % infix operators, prec. 0                      &       as defined      \\
103 %                                               &                       \\
104 % function types (@->@)                         &       right           \\
105 % contexts (@=>@)                                       &       --              \\
106 % type constraints (@::@)                               &       --              \\
107 % @do@, @if@, @let@, lambda(@\@) (rightwards)   &       right           \\
108 % sequences (@..@)                              &       --              \\
109 % generators (@<-@)                             &       --              \\
110 % grouping (@,@)                                        &       n-ary           \\
111 % guards (@|@)                                  &       --              \\
112 % case alternatives (@->@)                      &       --              \\
113 % definitions (@=@)                             &       --              \\
114 % separation (@;@)                              &       n-ary           \\ 
115 % \hline
116 % \end{tabular}
117 % }
118 % \]
119 % %**<div align=center> <h4>Table 1</h4> </div>
120 % \ecaption{Precedence of expressions, patterns, definitions (highest to lowest)}
121 % \label{syntax-precedences}
122 % \end{table}
123
124 The grammar is ambiguous regarding the extent of lambda abstractions,
125 let expressions, and conditionals.  The ambiguity is resolved by the
126 meta-rule that each of these constructs extends as far to the right as
127 possible.  As a consequence, each of these constructs has two precedences,
128 one to its left, which is the precedence used in the grammar; and
129 one to its right, which is obtained via the meta-rule.  See the sample
130 parses below.
131
132 Expressions involving infix operators are disambiguated by the
133 operator's fixity (see Section~\ref{fixity}).  Consecutive
134 unparenthesized operators with the same precedence must both be either
135 left or right associative to avoid a syntax error.
136 Given an unparenthesized expression ``"x qop^{(a,i)} y qop^{(b,j)} z"'', parentheses
137 must be added around either ``"x qop^{(a,i)} y"'' or ``"y qop^{(b,j)}
138 z"'' when "i=j" unless "a=b={\rm l}" or "a=b={\rm r}".
139
140 Negation\index{negation} is the only prefix operator in
141 \Haskell{}; it has the same precedence as the infix @-@ operator
142 defined in the Prelude (see Figure~\ref{prelude-fixities}%
143 %*ignore
144 , page~\pageref{prelude-fixities}%
145 %*endignore
146 ).
147
148 %       I can't make head or tail of this para, so
149 %       I'm just deleting it.  SLPJ Dec 98
150 % The separation of function arrows from case alternatives solves
151 % the ambiguity that otherwise arises when an unparenthesized
152 % function type is used in an expression, such as the guard in a case
153 % expression.
154
155 Sample parses are shown below.
156 \[\bt{|l|l|}%%b
157 \hline
158 This                                & Parses as                             \\
159 \hline
160 @f x + g y@                         & @(f x) + (g y)@                       \\
161 @- f x + y@                         & @(- (f x)) + y@                       \\
162 @let { ... } in x + y@              & @let { ... } in (x + y)@              \\
163 @z + let { ... } in x + y@          & @z + (let { ... } in (x + y))@        \\
164 @f x y :: Int@                      & @(f x y) :: Int@                      \\
165 @\ x -> a+b :: Int@                 & @\ x -> ((a+b) :: Int@)               \\
166 \hline\et\]
167
168 For the sake of clarity, the rest of this section shows the syntax of
169 expressions without their precedences.
170
171 \subsection{Errors}
172 \label{basic-errors}\index{error}
173 Errors during expression evaluation, denoted by "\bot"\index{"\bot"},
174 are indistinguishable by a Haskell program from non-termination.  Since \Haskell{} is a
175 lazy language, all \Haskell{} types include "\bot".  That is, a value
176 of any type may be bound to a computation that, when demanded, results
177 in an error.  When evaluated, errors cause immediate program
178 termination and cannot be caught by the user.  The Prelude provides
179 two functions to directly 
180 cause such errors:
181 \bprog
182 @
183 error     :: String -> a
184 undefined :: a
185 @
186 \eprog
187 \indextt{error}
188 \indextt{undefined}
189 A call to @error@ terminates execution of
190 the program and returns an appropriate error indication to the
191 operating system.  It should also display the string in some
192 system-dependent manner.  When @undefined@ is used, the error message
193 is created by the compiler.
194
195 Translations of \Haskell{} expressions use @error@ and @undefined@ to
196 explicitly indicate where execution time errors may occur.  The actual
197 program behavior when an error occurs is up to the implementation.
198 The messages passed to the @error@ function in these translations are
199 only suggestions; implementations may choose to display more or less
200 information when an error occurs.
201
202 \subsection{Variables, Constructors, Operators, and Literals}
203 %
204 @@@
205 aexp    ->  qvar                                & (\tr{variable})
206         |   gcon                                & (\tr{general constructor})
207         |   literal                             
208 @@@
209 \indexsyn{var}%
210 \indexsyn{con}%
211 \indexsyn{varop}%
212 \indexsyn{conop}%
213 \indexsyn{op}%
214 @@@
215 gcon    ->  @()@
216         |   @[]@
217         |   @(,@\{@,@\}@)@
218         |   qcon
219
220 var     ->  varid | @(@ varsym @)@              & (\tr{variable})
221 qvar    ->  qvarid | @(@ qvarsym @)@            & (\tr{qualified variable})
222 con     ->  conid | @(@ consym @)@              & (\tr{constructor})
223 qcon    ->  qconid | @(@ gconsym @)@            & (\tr{qualified constructor})
224 varop   ->  varsym | \bkqB varid \bkqA          & (\tr{variable operator})
225 qvarop  ->  qvarsym | \bkqB qvarid \bkqA        & (\tr{qualified variable operator})
226 conop   ->  consym | \bkqB conid \bkqA          & (\tr{constructor operator})
227 qconop  ->  gconsym | \bkqB qconid \bkqA        & (\tr{qualified constructor operator})
228 op      ->  varop | conop                       & (\tr{operator})
229 qop     ->  qvarop | qconop                     & (\tr{qualified operator})
230 gconsym ->  @:@ | qconsym
231 @@@
232 \indexsyn{gcon}%
233 \indexsyn{var}%
234 \indexsyn{qvar}%
235 \indexsyn{con}%
236 \indexsyn{qcon}%
237 \indexsyn{varop}%
238 \indexsyn{qvarop}%
239 \indexsyn{conop}%
240 \indexsyn{qconop}%
241 \indexsyn{qop}%
242 \indexsyn{gconsym}%
243
244 Alphanumeric operators are formed by enclosing an identifier between
245 grave accents (backquotes).  Any variable or constructor may be used as
246 an operator in this way.  If "fun" is an identifier (either variable
247 or constructor), then an expression of the form "fun x y" is
248 equivalent to "x \bkqB{fun}\bkqA y".  If no fixity\index{fixity}
249 declaration is given for "\bkqB{fun}\bkqA" then it defaults
250 to highest precedence and left associativity
251 (see Section~\ref{fixity}).
252
253 Similarly, any symbolic operator may be used as a (curried) variable
254 or constructor by enclosing it in parentheses.  If "op" is an infix
255 operator, then an expression or pattern of the form \mbox{"x op y"} is
256 equivalent to {"@(@op@)@ x y"}.
257
258 Qualified names may only be used to reference an imported variable or
259 constructor (see Section~\ref{import})
260 but not in the definition of a new variable or constructor.  Thus
261 \bprog
262 @
263 let F.x = 1 in F.x   -- invalid
264 @
265 \eprog
266 incorrectly uses a qualifier in the definition of @x@, regardless of
267 the module containing this definition.  Qualification does not affect
268 the nature of an operator: @F.+@ is an infix operator just as @+@ is.
269
270 Special syntax is used to name some constructors for some of the
271 built-in types, as found
272 in the production for "gcon" and "literal".  These are described
273 in Section~\ref{basic-types}.
274
275 \index{number!translation of literals}
276 An integer literal represents the
277 application of the function @fromInteger@\indextt{fromInteger} to the
278 appropriate value of type 
279 @Integer@.  Similarly, a floating point literal stands for an application of
280 @fromRational@\indextt{fromRational} to a value of type @Rational@ (that is, 
281 @Ratio Integer@).
282
283 \outline{
284 \paragraph*{Translation:}
285 The integer literal "i" is equivalent to @fromInteger@ "i",
286 where @fromInteger@ is a method in class @Num@ (see Section
287 \ref{numeric-literals}).\indexclass{Num}
288
289
290 The floating point literal "f" is equivalent to @fromRational@
291 ("n" @Ratio.%@ "d"), where @fromRational@ is a method in class @Fractional@
292 and @Ratio.%@ constructs a rational from two integers, as defined in
293 the @Ratio@ library.\indexclass{Fractional}
294 The integers "n" and "d" are chosen so that "n/d = f".
295 }
296
297
298 \subsection{Curried Applications and Lambda Abstractions}
299 \label{applications}
300 \label{lambda-abstractions}
301 \index{lambda abstraction}
302 \index{application}
303 %\index{function application|see{application}}
304 %
305 @@@
306 fexp    ->  [fexp] aexp                         & (\tr{function application})
307 exp     ->  @\@ apat_1 ... apat_n @->@ exp      & (\tr{lambda abstraction}, n>=1)
308 @@@
309 \indexsyn{exp}%
310 \indexsyn{fexp}%
311
312 \noindent
313 {\em Function application}\index{application} is written 
314 "e_1 e_2".  Application associates to the left, so the
315 parentheses may be omitted in @(f x) y@.  Because "e_1" could
316 be a data constructor, partial applications of data constructors are
317 allowed. 
318
319 {\em Lambda abstractions} are written 
320 "@\@ p_1 ... p_n @->@ e", where the "p_i" are {\em patterns}.
321 An expression such as @\x:xs->x@ is syntactically incorrect;
322 it may legally be written as @\(x:xs)->x@.
323
324 The set of patterns must be {\em linear}\index{linearity}%
325 \index{linear pattern}---no variable may appear more than once in the set.
326
327 \outline{
328 \paragraph*{Translation:}
329 The following identity holds:
330 \begin{center}
331 \bt{lcl}%
332 \struthack{17pt}%
333 "@\@ p_1 ... p_n @->@ e"
334          & "=" &
335         "@\@ x_1 ... x_n @-> case (@x_1@,@ ...@,@ x_n@) of (@p_1@,@ ...@,@ p_n@) ->@ e"
336 \et
337 \end{center}
338 where the "x_i" are new identifiers.
339 }
340 Given this translation combined with the semantics of case
341 expressions and pattern matching described in
342 Section~\ref{case-semantics}, if the
343 pattern fails to match, then the result is "\bot".
344
345              
346 \subsection{Operator Applications}
347 \index{operator application}
348 %\index{operator application|seealso{application}}
349 \label{operators}
350 %
351 @@@
352 exp     ->  exp_1 qop exp_2
353         |   @-@ exp                             & (\tr{prefix negation})
354 qop     ->  qvarop | qconop                     & (\tr{qualified operator})
355 @@@
356 \indexsyn{exp}%
357 \indexsyn{qop}%
358
359 \noindent
360 The form "e_1 qop e_2" is the infix application of binary
361 operator\index{operator} "qop" to expressions "e_1" and "e_2".  
362
363 The special
364 form "@-@e" denotes prefix negation\index{negation}, the only
365 prefix operator in \Haskell{}, and is 
366 syntax for "@negate @(e)".\indextt{negate}  The binary @-@ operator
367 does not necessarily refer 
368 to the definition of @-@ in the Prelude; it may be rebound 
369 by the module system.  However, unary @-@ will always refer to the
370 @negate@ function defined in the Prelude.  There is no link between
371 the local meaning of the @-@ operator and unary negation.
372
373 Prefix negation has the same precedence as the infix operator @-@
374 defined in the Prelude (see
375 Table~\ref{prelude-fixities}%
376 %*ignore
377 , page~\pageref{prelude-fixities}%
378 %*endignore
379 ).  Because @e1-e2@ parses as an
380 infix application of the binary operator @-@, one must write @e1(-e2)@ for
381 the alternative parsing.  Similarly, @(-)@ is syntax for 
382 @(\ x y -> x-y)@, as with any infix operator, and does not denote 
383 @(\ x -> -x)@---one must use @negate@ for that.
384
385 \outline{
386 \paragraph*{Translation:}
387 The following identities hold:
388 \begin{center}
389 \bt{lcl}%
390 \struthack{17pt}%
391 "e_1 op e_2" & "=" & "@(@op@)@ e_1 e_2" \\
392 "@-@e" & "=" & "@negate@ (e)"
393 \et
394 \end{center}
395 }
396
397 \subsection{Sections}
398 \index{section}
399 %\index{section|seealso{operator application}}
400 \label{sections}
401 %
402 @@@
403 aexp    ->  @(@ exp qop @)@ 
404         |   @(@ qop exp @)@
405 @@@
406 \indexsyn{aexp}%
407
408 \noindent
409 {\em Sections} are written as "@(@ op e @)@" or "@(@ e op @)@", where
410 "op" is a binary operator and "e" is an expression.  Sections are a
411 convenient syntax for partial application of binary operators.
412
413 Syntactic precedence rules apply to sections as follows.
414 "@(@op~e@)@" is legal if and only if "@(x@~op~e@)@" parses 
415 in the same way as "@(x@~op~@(@e@))@";
416 and similarly for  "@(@e~op@)@".
417 For example, @(*a+b)@ is syntactically invalid, but @(+a*b)@ and
418 @(*(a+b))@ are valid.  Because @(+)@ is left associative, @(a+b+)@ is syntactically correct,
419 but @(+a+b)@ is not; the latter may legally be written as @(+(a+b))@.
420
421 Because @-@ is treated specially in the grammar,
422 "@(-@ exp@)@" is not a section, but an application of prefix
423 negation,\index{negation} as
424 described in the preceding section.  However, there is a @subtract@
425 function defined in the Prelude such that
426 "@(subtract@ exp@)@" is equivalent to the disallowed section.
427 The expression "@(+ (-@ exp@))@" can serve the same purpose.
428
429 % Changed to allow postfix operators.  That is, in (op x), we no
430 % longer add a \x -> which would require op to be binary instead
431 % of unary.
432
433 \outline{
434 \paragraph*{Translation:}
435 The following identities hold:
436 \begin{center}
437 \bt{lcl}%
438 \struthack{17pt}%
439 "@(@op e@)@" & "=" & "@\@ x @->@ x op e" \\
440 "@(@e op@)@" & "=" & "@\@ x @->@ e op x"
441 \et
442 \end{center}
443 where "op" is a binary operator, "e" is an expression, and "x" is a variable
444 that does not occur free in "e".
445 }
446
447 \subsection{Conditionals}
448 \label{conditionals}\index{conditional expression}
449 %
450 @@@
451 exp     ->  @if@ exp_1 @then@ exp_2 @else@ exp_3
452 @@@
453 \indexsyn{exp}%
454
455 %\indextt{if ... then ... else ...}
456 A {\em conditional expression}
457 \index{conditional expression}
458 has the form 
459 "@if@ e_1 @then@ e_2 @else@ e_3" and returns the value of "e_2" if the
460 value of "e_1" is @True@, "e_3" if "e_1" is @False@, and "\bot"
461 otherwise.
462
463 \outline{
464 \paragraph*{Translation:}
465 The following identity holds:
466 \begin{center}
467 \bt{lcl}%
468 \struthack{17pt}%
469 "@if@ e_1 @then@ e_2 @else@ e_3"  & "=" & "@case@ e_1 @of { True ->@ e_2 @; False ->@ e_3 @}@"
470 \et
471 \end{center}
472 where @True@ and @False@ are the two nullary constructors from the 
473 type @Bool@, as defined in the Prelude.  The type of "e_1" must be @Bool@;
474 "e_2" and "e_3" must have the same type, which is also the type of the
475 entire conditional expression.
476 }
477
478 \subsection{Lists}
479 \label{lists}
480 %
481 @@@
482 exp     ->  exp_1 qop exp_2
483 aexp    ->  @[@ exp_1 @,@ ... @,@ exp_k @]@     & (k>=1)
484         |   gcon
485 gcon    -> @[]@
486         | qcon
487 qcon    -> @(@ gconsym @)@
488 qop     -> qconop
489 qconop  -> gconsym
490 gconsym -> @:@
491 @@@
492 \indexsyn{aexp}%
493
494 {\em Lists}\index{list} are written "@[@e_1@,@ ...@,@ e_k@]@", where
495 "k>=1".  The list constructor is @:@, and the empty list is denoted @[]@.
496 Standard operations on
497 lists are given in the Prelude (see Section~\ref{basic-lists}, and
498 Appendix~\ref{stdprelude} notably Section~\ref{preludelist}).
499
500 \outline{
501 \paragraph*{Translation:}  
502 The following identity holds:
503 \begin{center}
504 \bt{lcl}%
505 \struthack{17pt}%
506 "@[@e_1@,@ ...@,@ e_k@]@"  & "=" & "e_1 @: (@e_2 @: (@ ... @(@e_k @: [])))@"
507 \et
508 \end{center}
509 where @:@ and @[]@ are constructors for lists, as defined in
510 the Prelude (see Section~\ref{basic-lists}).  The types
511 of "e_1" through "e_k" must all be the same (call it "t\/"), and the
512 type of the overall expression is @[@"t"@]@ (see Section~\ref{type-syntax}).
513 }
514 The constructor ``@:@'' is reserved solely for list construction; like
515 @[]@, it is considered part of the language syntax, and cannot be hidden or redefined.
516
517 \subsection{Tuples}
518 \label{tuples}
519 %
520 @@@
521 aexp    ->  @(@ exp_1 @,@ ... @,@ exp_k @)@     & (k>=2)
522         | qcon
523 qcon -> @(,@\{@,@\}@)@
524
525 @@@
526 \indexsyn{aexp}%
527
528 {\em Tuples}\index{tuple} are written "@(@e_1@,@ ...@,@ e_k@)@", and may be
529 of arbitrary length "k>=2".  The constructor for an "n"-tuple is denoted by
530 @(,@\ldots@,)@, where there are "n-1" commas.  Thus @(a,b,c)@ and
531 @(,,) a b c@ denote the same value.
532 Standard operations on tuples are given
533 in the Prelude (see Section~\ref{basic-tuples} and Appendix~\ref{stdprelude}).
534
535 \outline{
536 \paragraph*{Translation:}  
537 "@(@e_1@,@ ...@,@ e_k@)@" for "k\geq2" is an instance of a "k"-tuple as
538 defined in the Prelude, and requires no translation.  If
539 "t_1" through "t_k" are the types of "e_1" through "e_k",
540 respectively, then the type of the resulting tuple is 
541 "@(@t_1@,@ ...@,@ t_k@)@" (see Section~\ref{type-syntax}).
542 }
543
544 \subsection{Unit Expressions and Parenthesized Expressions}
545 \label{unit-expression}
546 \index{unit expression}
547 %
548 @@@
549 aexp    ->  gcon
550         |   @(@ exp @)@
551 gcon    -> @()@
552 @@@
553 \indexsyn{aexp}%
554
555 \noindent
556 The form "@(@e@)@" is simply a {\em parenthesized expression}, and is
557 equivalent to "e".  The {\em unit expression} @()@ has type
558 @()@\index{trivial type} (see
559 Section~\ref{type-syntax}).  It is the only member of that type apart
560 from $\bot$, and can
561 be thought of as the ``nullary tuple'' (see Section~\ref{basic-trivial}).
562 \nopagebreak[4]
563
564 \outline{
565 \paragraph{Translation:}  
566 "@(@e@)@" is equivalent to "e".
567 }
568
569 \subsection{Arithmetic Sequences}
570 \label{arithmetic-sequences}
571 %
572 @@@
573 aexp    ->  @[@ exp_1 [@,@ exp_2] @..@ [exp_3] @]@      
574 @@@
575 \indexsyn{aexp}%
576
577 \noindent
578
579
580 The {\em arithmetic sequence}\index{arithmetic sequence}
581 "@[@e_1@,@ e_2 @..@ e_3@]@" denotes a list of values of
582 type "t", where each of the "e_i" has type "t", and "t" is an
583 instance of class @Enum@.
584
585 \outline{
586 \paragraph{Translation:}
587 Arithmetic sequences satisfy these identities:
588 \begin{center}
589 \begin{tabular}{lcl}%
590 \struthack{17pt}%
591 @[ @"e_1"@.. ]@         & "=" 
592                         & @enumFrom@ "e_1" \\
593 @[ @"e_1"@,@"e_2"@.. ]@ & "=" 
594                         & @enumFromThen@ "e_1" "e_2" \\
595 @[ @"e_1"@..@"e_3"@ ]@  & "=" 
596                         & @enumFromTo@ "e_1" "e_3" \\
597 @[ @"e_1"@,@"e_2"@..@"e_3"@ ]@ 
598                         & "=" 
599                         & @enumFromThenTo@ "e_1" "e_2" "e_3"
600 \end{tabular}
601 \end{center}
602 where @enumFrom@, @enumFromThen@, @enumFromTo@, and @enumFromThenTo@
603 are class methods in the class @Enum@ as defined in the Prelude
604 (see Figure~\ref{standard-classes}%
605 %*ignore
606 , page~\pageref{standard-classes}%
607 %*endignore
608 ).
609 }
610
611 The semantics of arithmetic sequences therefore depends entirely
612 on the instance declaration for the type "t".  We give here the
613 semantics for @Prelude@ types, and indications of the expected semantics
614 for other, user-defined, types.
615
616 For the types @Int@ and @Integer@, arithmetic sequences have the following
617 meaning:
618 \begin{itemize}
619 \item The sequence "@[@e_1@..]@" is the list "@[@e_1@,@e_1+1@,@e_1+2@,@...@]@".
620
621 \item The sequence "@[@e_1@,@e_2@..]@" is the list "@[@e_1@,@e_1+i@,@e_1+2i@,@...@]@",
622 where the increment, "i", is "e_2-e_1".  The increment may be zero or negative.
623 If the increment is zero, all the list elements are the same.
624
625 \item The sequence "@[@e_1@..@e_3@]@" is the list "@[@e_1@,@e_1+1@,@e_1+2@,@...e_3@]@".
626 The list is empty if "e_1 > e_3".
627
628 \item The sequence "@[@e_1@,@e_2@..@e_3@]@" 
629 is the list "@[@e_1@,@e_1+i@,@e_1+2i@,@...e_3@]@",
630 where the increment, "i", is "e_2-e_1".  If the increment 
631 is positive or zero, the list terminates when the next element would
632 be greater than "e_3"; the list is empty if "e_1 > e_3".
633 If the increment is negative, the list terminates when the next element would
634 be less than "e_3"; the list is empty if "e1 < e_3".
635 \end{itemize}
636 For other {\em discrete} @Prelude@ types "t" that 
637 are instances of @Enum@, namely @()@, @Bool@, @Char@ and @Ordering@,
638 the semantics is given by mapping the "e_i" to @Int@ using @fromEnum@,
639 using the above rules, and then mapping back to "t" with @toEnum@.
640
641 Where the type is also an instance of class @Bounded@ 
642 and "e_3" is omitted, an implied "e_3" is added
643 of @maxBound@ (if the increment is positive) or @minBound@ (resp. negative).
644 For example, @['a'..'z']@ denotes
645 the list of lowercase letters in alphabetical order, and @[LT..]@ is the
646 list @[LT,EQ,GT]@.
647
648 For {\em continuous} @Prelude@ types that are instances of @Enum@,
649 namely @Float@ and @Double@, the semantics is given by the rules for @Int@,
650 except that the list terminates when the elements become greater than
651 "e_3+i/2" for positive increment "i", or when they become less than 
652 "e_3+i/2" for negative "i".
653
654 See Figure~\ref{standard-classes}%
655 %*ignore
656 , page~\pageref{standard-classes}
657 %*endignore
658  and Section~\ref{derived-decls} for more details of which @Prelude@
659 type are in @Enum@.
660
661
662 \subsection{List Comprehensions}
663 \index{list comprehension}
664 \index{let expression!in list comprehensions}
665 \label{list-comprehensions}
666 %
667 @@@
668 aexp    -> @[@ exp @|@ qual_1 @,@ ... @,@ qual_n @]@    & (\tr{list comprehension}, n>=1)
669 qual    -> pat @<-@ exp         & (\tr{generator})
670          | @let@ decls          & (\tr{local declaration})
671          | exp                  & (\tr{guard})
672 @@@
673 \indexsyn{aexp}
674 \indexsyn{qual}
675
676 \noindent
677 A {\em list comprehension} has the form "@[@ e @|@ q_1@,@ ...@,@ q_n @]@,
678 n>=1," where the "q_i" qualifiers\index{qualifier} are either
679 \begin{itemize}
680 \item {\em generators}\index{generator} of the form "p @<-@ e", where
681 "p" is a 
682 pattern (see Section~\ref{pattern-matching}) of type "t" and "e" is an
683 expression of type "@[@t@]@"
684 \item {\em guards},\index{guard} which are arbitrary expressions of
685 type @Bool@ 
686 \item {\em local bindings} that provide new definitions for use in
687 the generated expression "e" or subsequent guards and generators.
688 \end{itemize}
689
690 Such a list comprehension returns the list of elements
691 produced by evaluating "e" in the successive environments
692 created by the nested, depth-first evaluation of the generators in the
693 qualifier list.  Binding of variables occurs according to the normal
694 pattern matching rules (see Section~\ref{pattern-matching}), and if a
695 match fails then that element of the list is simply skipped over.  Thus:\nopagebreak[4]
696 \bprog
697 @
698 [ x |  xs   <- [ [(1,2),(3,4)], [(5,4),(3,2)] ], 
699       (3,x) <- xs ]
700 @
701 \eprog
702 yields the list @[4,2]@.  If a qualifier is a guard, it must evaluate
703 to @True@ for the previous pattern match to succeed.  
704 As usual, bindings in list comprehensions can shadow those in outer
705 scopes; for example:
706 \[\ba{lll}
707 @[ x | x <- x, x <- x ]@ & = & @[ z | y <- x, z <- y]@ \\
708 \ea\]
709 \outline{
710 \paragraph{Translation:}
711 List comprehensions satisfy these identities, which may be
712 used as a translation into the kernel:
713 \begin{center}
714 \bt{lcl}%
715 \struthack{17pt}%
716 "@[ @ e@ | True ]@" & = & "@[@e@]@" \\
717 "@[ @ e@ | @q@ ]@" & = & "@[@~ e~@|@~q@, True ]@" \\
718 "@[ @ e@ | @b@,@~ Q ~@]@" & = &
719         "@if@~b~@then@~@[ @ e@ | @Q@ ]@~@else []@" \\
720 "@[ @ e@ | @p @<-@ l@,@~ Q@ ]@" & = &
721         "@let ok@~p~@=@~@[ @ e@ | @Q@ ]@" \\
722 &&       @    ok _ = []@ \\
723 &&      "@in concatMap ok@~ l" \\
724 "@[ @ e@ | let@~decls@,@~ Q@ ]@" & = &
725         "@let@~decls~@in@~@[ @ e@ | @Q@ ]@"
726 \et
727 \end{center}
728 where "e" ranges over expressions, "p" over
729 patterns, "l" over list-valued expressions, "b" over
730 boolean expressions, "decls" over declaration lists, 
731 "q" over qualifiers, and "Q" over sequences of qualifiers.  "@ok@" is a fresh variable.
732 The function @concatMap@, and boolean value @True@, are defined in the Prelude.
733 }
734
735 As indicated by the translation of list comprehensions, variables
736 bound by @let@ have fully polymorphic types while those defined by
737 @<-@ are lambda bound and are thus monomorphic (see Section
738 \ref{monomorphism}).
739
740 \subsection{Let Expressions}
741 \index{let expression}
742 \label{let-expressions}
743 %
744 % Including this syntax blurb does REALLY bad things to page breaking
745 % in the 1.[12] report (sigh); ToDo: hope it goes away.
746 @@@
747 exp     ->  @let@ decls @in@ exp
748 @@@
749 \indexsyn{exp}
750 \index{declaration!within a {\tt let} expression}
751
752 \noindent
753 {\em Let expressions} have the general form
754 "@let {@ d_1 @;@ ...  @;@ d_n @} in@ e",
755 and introduce a
756 nested, lexically-scoped, 
757 mutually-recursive list of declarations (@let@ is often called @letrec@ in
758 other languages).  The scope of the declarations is the expression "e"
759 and the right hand side of the declarations.  Declarations are
760 described in Section~\ref{declarations}.  Pattern bindings are matched
761 lazily; an implicit @~@ makes these patterns
762 irrefutable.\index{irrefutable pattern}
763 For example, 
764 \bprog
765 @
766 let (x,y) = undefined in @"e"@
767 @
768 \eprog
769 does not cause an execution-time error until @x@ or @y@ is evaluated.
770
771 \outline{
772 \paragraph*{Translation:} The dynamic semantics of the expression 
773 "@let {@ d_1 @;@ ...  @;@ d_n @} in@ e_0" are captured by this
774 translation: After removing all type signatures, each
775 declaration "d_i" is translated into an equation of the form 
776 "p_i @=@ e_i", where "p_i" and "e_i" are patterns and expressions
777 respectively, using the translation in
778 Section~\ref{function-bindings}.  Once done, these identities
779 hold, which may be used as a translation into the kernel:
780 \begin{center}
781 \bt{lcl}%
782 \struthack{17pt}%
783 @let {@"p_1"@ = @"e_1"@; @ ... @; @"p_n"@ = @"e_n"@} in@ "e_0"
784       &=& @let (~@"p_1"@,@ ... @,~@"p_n"@) = (@"e_1"@,@ ... @,@"e_n"@) in@ "e_0" \\
785 @let @"p"@ = @"e_1" @ in @ "e_0"
786         &=& @case @"e_1"@ of ~@"p"@ -> @"e_0"   \\
787         & & {\rm where no variable in "p" appears free in "e_1"} \\
788 @let @"p"@ = @"e_1" @ in @ "e_0"
789       &=& @let @"p"@ = fix ( \ ~@"p"@ -> @"e_1"@) in@ "e_0"
790 \et
791 \end{center}
792 where @fix@ is the least fixpoint operator.  Note the use of the
793 irrefutable patterns "@~@p".  This translation
794 does not preserve the static semantics because the use of @case@
795 precludes a fully polymorphic typing of the bound variables.
796 %\folks{Needs work -- KH}
797 % This same semantics applies to the top-level of
798 %a program that has been translated into a @let@ expression,
799 % as described at the beginning of Section~\ref{modules}.
800 The static semantics of the bindings in a @let@ expression
801 are described in 
802 Section~\ref{pattern-bindings}.
803 }
804
805 \subsection{Case Expressions}
806 \label{case}
807 %
808 @@@
809 exp     ->  @case@ exp @of@ @{@ alts @}@
810 alts    ->  alt_1 @;@ ... @;@ alt_n             & (n>=0)
811 alt     ->  pat @->@ exp [@where@ decls]
812         |   pat gdpat [@where@ decls]
813         |                                       & (empty alternative)
814
815 gdpat   ->  gd @->@ exp [ gdpat ]
816 gd      ->  @|@ exp^0 
817 @@@
818 \indexsyn{exp}%
819 \indexsyn{alts}%
820 \indexsyn{alt}%
821 \indexsyn{gdpat}%
822 \indexsyn{gd}%
823
824 A {\em case expression}\index{case expression} has the general form
825 \[
826 "@case@ e @of { @p_1 match_1 @;@ ... @;@ p_n  match_n @}@"
827 \]
828 where each "match_i" is of the general form
829 \[\ba{lll}
830  & "@|@ g_{i1}"   & "@->@ e_{i1}" \\
831  & "..." \\
832  & "@|@ g_{im_i}" & "@->@ e_{im_i}" \\
833  & \multicolumn{2}{l}{"@where@ decls_i"}
834 \ea\]
835 (Notice that in the syntax rule for "gd", the ``@|@'' is a 
836 terminal symbol, not the syntactic metasymbol for alternation.)
837 Each alternative "p_i match_i" consists of a 
838 pattern\index{pattern} "p_i" and its matches, "match_i".
839 Each match in turn
840 consists of a sequence of pairs of guards\index{guard}
841 "g_{ij}" and bodies "e_{ij}" (expressions), followed by
842 optional bindings ("decls_i") that scope over all of the guards and
843 expressions of the alternative.  An alternative of the form
844 \[
845 "pat @->@ exp @where@ decls"
846 \]
847 is treated as shorthand for:
848 \[\ba{lll}
849  & "pat @| True@"   & "@->@ exp" \\
850  & \multicolumn{2}{l}{"@where@ decls"}
851 \ea\]
852
853 A case expression must have at least one alternative and each alternative must
854 have at least one body.  Each body must have the same type, and the
855 type of the whole expression is that type.
856
857 A case expression is evaluated by pattern matching the expression "e"
858 against the individual alternatives.  The matches are tried sequentially,
859 from top to bottom.  The first successful match causes evaluation of
860 the corresponding alternative body, in the environment of the case
861 expression extended by the bindings created during the matching of
862 that alternative and by the "decls_i" associated with that
863 alternative.  If no
864 match succeeds, the result is "\bot".  Pattern matching is described
865 in Section~\ref{pattern-matching}, with the formal semantics of case
866 expressions in 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 (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 (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 "b", 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 ~(x,y,z) [a] | a && y = 1
1418 @
1419 \eprog
1420 % \bprog
1421 % @@
1422 % f t [a] | a==y = 1 
1423 %           where (x,y,z) = t
1424 % @@
1425 % \eprog
1426 both @a@ and @y@ will be evaluated by @&&@ in the guard.
1427
1428
1429 \subsubsection{Formal Semantics of Pattern Matching}
1430 \label{case-semantics}
1431
1432 The semantics of all pattern matching constructs other than @case@
1433 expressions are defined by giving identities that relate those
1434 constructs to @case@ expressions.  The semantics of
1435 @case@ expressions themselves are in turn given as a series of
1436 identities, in Figures~\ref{simple-case-expr-1}--\ref{simple-case-expr-2}. 
1437 Any implementation should behave so that these identities hold; it is 
1438 not expected that it will use them directly, since that 
1439 would generate rather inefficient code.
1440   
1441 \begin{figure}[tb]
1442 \outlinec{
1443 \begin{tabular}{@@{}cl}
1444 (a)&@case @$e$@ of { @$alts$@ } @$=$@ (\@$v$@ -> case @$v$@ of { @$alts$@ }) @"e"\\
1445 &{\rm where $v$ is a new variable}\\
1446 (b)&@case @$v$@ of { @$p_1\ \ match_1$@;  @$\ldots{}$@ ; @$p_n\ \ match_n$@ }@\\
1447    &$=$@  case @$v$@ of { @$p_1\ \ match_1$@ ;@\\
1448    &@                _  -> @$\ldots{}$@ case @$v$@ of {@\\
1449    &@                           @$p_n\ \ match_n$\ @;@\\
1450    &@                           _  -> error "No match" }@$\ldots$@}@\\
1451    &@ @{\rm where each $match_i$ has the form:}\\
1452    &@  | @$g_{i,1}$  @ -> @$e_{i,1}$@ ; @$\ldots{}$@ ; | @$g_{i,m_i}$@ -> @$e_{i,m_i}$@ where { @$decls_i$@ }@\\[4pt]
1453 %\\
1454 (c)&@case @$v$@ of { @$p$@ | @$g_1$@ -> @$e_1$@ ; @$\ldots{}$\\
1455    &\hspace*{4pt}@             | @$g_n$@ -> @$e_n$@ where { @$decls$@ }@\\
1456    &\hspace*{2pt}@            _     -> @$e'$@ }@\\
1457    &$=$@ case @$e'$@ of@\\
1458    &   @  {@$y$@ -> @     {\rm (where "y" is a new variable)}\\
1459  &@   case @$v$@ of {@\\
1460    &@         @$p$@ -> let { @$decls$@ } in@\\
1461    &@                if @$g_1$@ then @$e_1$@ @$\ldots{}$@ else if @$g_n$@ then @$e_n$@ else @$y$ \ @;@\\
1462    &@         _ -> @$y$@ }}@\\[4pt]
1463 %\\
1464 (d)&@case @$v$@ of { ~@$p$@ -> @$e$@; _ -> @$e'$@ }@\\
1465 &$=$@ (\@$x'_1$ $\ldots$ $x'_n$ @->@ $e_1$ @) (case @$v$@ of { @$p$@->@ 
1466 $x_1$@ })@ $\ldots$ @(case @$v$@ of { @$p$@ -> @$x_n$@})@\\
1467 &{\rm where $e_1$ = $e\,[x'_1/x_1, \ldots, x'_n/x_n]$}\\[2pt]
1468 &{\rm $x_1, \ldots, x_n$ are all the variables in $p\/$; $x'_1, \ldots, x'_n$ are new variables}\\[4pt]
1469 %\\
1470 (e)&@case @$v$@ of { @$x${\tt @@}$p$@ -> @$e$@; _ -> @$e'$@ }@\\
1471 &$=$@  case @$v$@ of { @$p$@ -> ( \ @$x$@ -> @$e$@ ) @$v$@ ; _ -> @$e'$@ }@\\[4pt]
1472 %\\
1473 (f)&@case @$v$@ of { _ -> @$e$@; _ -> @$e'$@ } @$=$@ @$e$\\[4pt]
1474 \end{tabular}
1475 }
1476 %**<div align=center> <h4>Figure 3</h4> </div>
1477 \ecaption{Semantics of Case Expressions, Part 1}
1478 \label{simple-case-expr-1}
1479 \end{figure}
1480
1481 \begin{figure}[tb]
1482 \outlinec{
1483 \begin{tabular}{@@{}cl}
1484 (g)&@case @$v$@ of { @$K\ p_1 \ldots p_n$@ -> @$e$@; _ -> @$e'$@ }@\\
1485 &$=$@ case @$v$@ of {@\\
1486 &@     @$K\ x_1 \ldots x_n$@ -> case @$x_1$@ of {@\\
1487 &@                    @$p_1$@ -> @$\ldots$@ case @$x_n$@ of { @$p_n$@ -> @$e$@ ; _ -> @$e'$@ } @$\ldots$\\
1488 &@                    _  -> @$e'$@ }@\\
1489 &@     _ -> @$e'$@ }@\\[2pt]
1490 &{\rm at least one of $p_1, \ldots, p_n$ is not a variable; $x_1, \ldots, x_n$ are new variables}\\[4pt]
1491 %\\
1492 (h)&@case @$v$@ of { @$k$@ -> @$e$@; _ -> @$e'$@ } @$=$@ if (@$v$@==@$k$@) then @$e$@ else @$e'$\\[4pt]
1493 %\\
1494 (i)&@case @$v$@ of { @$x$@ -> @$e$@; _ -> @$e'$@ } @$=$@ case @$v$@ of { @$x$@ -> @$e$@ }@\\[4pt]
1495 %\\
1496 (j)&@case @$v$@ of { @$x$@ -> @$e$@ } @$=$@ ( \ @$x$@ -> @$e$@ ) @$v$\\[4pt]
1497 %\\
1498 (k)&@case @$N$ $v$@ of { @$N$@ @$p$@ -> @$e$@; _ -> @$e'$@ }@\\
1499 &$=$@ case @$v$@ of { @$p$@ -> @$e$@; _ -> @$e'$@ }@\\
1500 &{\rm where $N$ is a @newtype@ constructor}\\[4pt]
1501 (l)&@case @$\bot$@ of { @$N$@ @$p$@ -> @$e$@; _ -> @$e'$@ } @$=$@ case @$\bot$@ of { @$p$@ -> @$e$@ }@\\
1502 &{\rm where $N$ is a @newtype@ constructor}\\[4pt]
1503 (m)& @case @ $v$ @ of { @ $K$ @ {@ $f_1$ @ = @ $p_1$ @ , @ $f_2$ @ = @
1504 $p_2$ @ , @ $\ldots$ @} -> @ $e$ @; _ -> @ $e'$ @ }@\\
1505 &$=$ @ case @$e'$@ of {@\\
1506 &@   @$y$@ ->@\\
1507 &@    case @ $v$ @ of { @\\
1508 &@     @ $K$ @ { @ $f_1$ @ = @ $p_1$ @ } ->@\\
1509 &@            case @ $v$ @ of {@ $K$ @ {@ $f_2$ @ = @ $p_2$ @ , @
1510 $\ldots$ @ } -> @ $e$ @; _ -> @ $y$ @ };@\\
1511 &@            _ -> @ $y$ @ }}@\\
1512 &{\rm where $f_1$, $f_2$, $\ldots$ are fields of constructor $K$; $y$
1513 is a new variable}\\[4pt]
1514 (n)&@case @ $v$ @ of { @ $K$ @ {@ $f$ @ = @ $p$ @} -> @ $e$ @; _ -> @
1515 $e'$ @ }@ \\
1516 &$=$@ case @ $v$ @ of {@\\
1517 &   @    @ $K$ $p_1\ \ldots \  p_n$ @ -> @ $e$ @; _ -> @ $e'$ @ }@\\
1518 &{\rm where $p_i$ is $p$ if $f$ labels the $i$th component of $K$,
1519 @_@ otherwise}\\
1520 (o)&@case @ $v$ @ of { @ $K$ @ {} -> @ $e$ @; _ -> @
1521 $e'$ @ }@ \\
1522 &$=$@ case @ $v$ @ of {@\\
1523 &   @    @ $K$ @_@ $\ldots$ @_ -> @ $e$ @; _ -> @ $e'$ @ }@\\
1524 (p)&@case (@$K'$@ @$e_1$@ @$\ldots$@ @$e_m$@) of { @$K$@ @$x_1$@ @$\ldots$@ @$x_n$@ -> @$e$@; _ -> @$e'$@ } @$=$@ @$e'$\\
1525 &{\rm where $K$ and $K'$ are distinct @data@ constructors of arity $n$ and $m$, respectively}\\[4pt]
1526 %\\
1527 (q)&@case (@$K$@ @$e_1$@ @$\ldots$@ @$e_n$@) of { @$K$@ @$x_1$@ @$\ldots$@ @$x_n$@ -> @$e$@; _ -> @$e'$@ }@\\
1528 &$=$@  case @$e_1$@ of { @$x'_1$@ -> @$\ldots$@  case @$e_n$@ of { @$x'_n$@ -> @$e[x'_1/x_1 \ldots x'_n/x_n]$@ }@$\ldots$@}@\\
1529 &{\rm where $K$ is a constructor of arity $n$; $x'_1 \ldots x'_n$ are new variables}\\[4pt]
1530 %(l)&@case (@$A$@ @$ e_1$@) of {@$A$@ @$ x_1$@ -> @$e$@; _ -> @$e'$@ }@\\
1531 %&$=$@ case @$e1$@ of { @$x_1$@ -> @$e$@ }@\\
1532 %&{\rm where $A$ is constructor defined by @newtype@}\\
1533 (r)&@case @$v$@ of { @$x$@+@$k$@ -> @$e$@; _ -> @$e'$@ }@\\
1534 &$=$@ if @$v$@ >= @$k$@ then let {@$x'$@ = @$v$@-@$k$@} in @$e[x'/x]$@ else @$e'$@ @($x'$ is a new variable)\\
1535 \end{tabular}
1536 }
1537 %**<div align=center> <h4>Figure 4</h4> </div>
1538 \ecaption{Semantics of Case Expressions, Part 2}
1539 \label{simple-case-expr-2}
1540 \end{figure}
1541
1542 In Figures~\ref{simple-case-expr-1}--\ref{simple-case-expr-2}:
1543 "e", "e'" and "e_i" are expressions; 
1544 "g" and "g_i" are boolean-valued expressions; 
1545 "p" and "p_i" are patterns; 
1546 "v", "x", and "x_i" are variables; 
1547 "K" and "K'" are algebraic datatype (@data@) constructors (including
1548 tuple constructors);  "N" is a @newtype@ constructor; \index{newtype declaration@@{\tt newtype} declaration}
1549 and "k" is a character, string, or numeric literal.
1550
1551 % For clarity, several rules are expressed using
1552 % @let@ (used only in a non-recursive way); their usual purpose is to
1553 % prevent name capture
1554 % (e.g., in rule~(c)).  The rules may be re-expressed entirely with
1555 % @cases@ by applying this identity:
1556 % \[
1557 % "@let @x@ = @y@ in @e@ @ =@  case @y@ of { @x@ -> @e@ }@"
1558 % \]
1559
1560 %Using all but the last two identities (rules~(n) and~(o)) in Figure~\ref{simple-case-expr-2}
1561 %in a left-to-right manner yields a translation into a
1562 %subset of general @case@ expressions called {\em simple case expressions}.%
1563 %\index{simple case expression}
1564 Rule~(b) matches a general source-language
1565 @case@ expression, regardless of whether it actually includes
1566 guards---if no guards are written, then @True@ is substituted for the guards "g_{i,j}"
1567 in the "match_i" forms.
1568 Subsequent identities manipulate the resulting @case@ expression into simpler
1569 and simpler forms.
1570 %The semantics of simple @case@ expressions is 
1571 %given by the last two identities ((n) and~(o)).
1572
1573 Rule~(h) in Figure~\ref{simple-case-expr-2} involves the
1574 overloaded operator @==@; it is this rule that defines the
1575 meaning of pattern matching against overloaded constants.
1576 \index{pattern-matching!overloaded constant}
1577
1578 %% When used as a translation, the identities in
1579 %% Figure~\ref{simple-case-expr} will generate a very inefficient
1580 %% program.  This can be fixed by using further @case@ or @let@ 
1581 %% expressions, but doing so 
1582 %% would clutter the identities, which are intended only to convey the semantics.
1583
1584 These identities all preserve the static semantics.  Rules~(d),~(e), and~(j)
1585 use a lambda rather than a @let@; this indicates that variables bound
1586 by @case@ are monomorphically typed (Section~\ref{type-semantics}).
1587 \index{monomorphic type variable}
1588
1589 %**~footer
1590
1591 % Local Variables: 
1592 % mode: latex
1593 % End: