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