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