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