source: report/report/exps.verb @ 6a0f5a2

h2010
Last change on this file since 6a0f5a2 was 6a0f5a2, checked in by Iavor S. Diatchki <iavor.diatchki@…>, 11 years ago

fixed rule (g) of pattern semantics to avoid duplicating the evaluation of e'

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