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