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