ffb2e357c47a37e7de11ec660d3c296e6157d0df
[haskell-report.git] / report / decls.verb
1 %
2 % $Header: /home/cvs/root/haskell-report/report/decls.verb,v 1.18 2002/12/10 11:51:10 simonpj Exp $
3 %
4 %**<title>The Haskell 98 Report: Declarations</title>
5 %*section 4
6 %**~header
7 \section{Declarations and Bindings}
8 \index{declaration}
9 \index{binding}
10 \label{declarations}
11
12 In this chapter, we describe the syntax and informal semantics of \Haskell{}
13 {\em declarations}.
14 % including their translations into
15 % the \Haskell{} kernel where appropriate.
16 % (see Appendix~\ref{formal-semantics} for a complete formal semantics).
17
18 @@@
19 module -> @module@ modid [exports] @where@ body 
20        |  body
21 body   -> @{@ impdecls @;@ topdecls @}@
22         | @{@ impdecls  @}@
23         | @{@ topdecls  @}@
24
25 topdecls -> topdecl_1 @;@ ... @;@ topdecl_n     & (n>=1)
26 topdecl -> @type@ simpletype @=@ type
27         |  @data@ [context @=>@] simpletype @=@ constrs [deriving]
28         |  @newtype@ [context @=>@] simpletype @=@ newconstr [deriving]
29         |  @class@ [scontext @=>@] tycls tyvar [@where@ cdecls]
30         |  @instance@ [scontext @=>@] qtycls inst [@where@ idecls]
31         |  @default@ @(@type_1 @,@ ... @,@ type_n@)@ & \qquad (n>=0)
32         |  decl
33
34 decls   -> @{@ decl_1 @;@ ... @;@ decl_n @}@            & (n>=0)
35 decl    -> gendecl
36         |  (funlhs | pat^0) rhs
37
38 cdecls  -> @{@ cdecl_1 @;@ ... @;@ cdecl_n @}@          & (n>=0)
39 cdecl   -> gendecl
40         |  (funlhs | var) rhs
41
42 idecls  -> @{@ idecl_1 @;@ ... @;@ idecl_n @}@          & (n>=0)
43 idecl   -> (funlhs | var) rhs
44         |                                               & (\tr{empty})
45
46 gendecl -> vars @::@ [context @=>@] type        & (\tr{type signature})
47         |  fixity [integer] ops                 & (\tr{fixity declaration})
48         |                                       & (\tr{empty declaration})
49
50 ops     -> op_1 @,@ ... @,@ op_n                & (n>=1)
51 vars    -> var_1 @,@ ... @,@ var_n              & (n>=1)
52 fixity  -> @infixl@ | @infixr@ | @infix@
53 @@@
54 \indexsyn{vars}%
55 \indexsyn{fixity}%
56 \indexsyn{ops}%
57 \indexsyn{topdecls}%
58 \indexsyn{topdecl}%
59 \indexsyn{gendecl}%
60 \indexsyn{decls}%
61 \indexsyn{decl}%
62 \indexsyn{cdecls}%
63 \indexsyn{cdecl}%
64 \indexsyn{idecls}%
65 \indexsyn{idecl}%
66
67 The declarations in the syntactic category "topdecls" are only allowed
68 at the top level of a \Haskell{} module (see
69 Chapter~\ref{modules}), whereas "decls" may be used either at the top level or
70 in nested scopes (i.e.~those within a @let@ or @where@ construct).
71
72 For exposition, we divide the declarations into
73 three groups: user-defined datatypes, consisting of @type@, @newtype@,
74 and @data@ 
75 declarations (Section~\ref{user-defined-datatypes}); type classes and
76 overloading, consisting of @class@, @instance@, and @default@
77 declarations (Section~\ref{overloading}); and nested declarations,
78 consisting of value bindings, type signatures, and fixity declarations
79 (Section~\ref{nested}).
80
81 %The @module@ declaration, along with @import@ and
82 %infix declarations, is described in Section~\ref{modules}.
83
84 \Haskell{} has several primitive datatypes that are ``hard-wired''
85 (such as integers and floating-point numbers), but most ``built-in''
86 datatypes are defined with normal \Haskell{} code, using normal @type@
87 and @data@ declarations. % (see Section~\ref{user-defined-datatypes}).
88 These ``built-in'' datatypes are described in detail in
89 Section~\ref{basic-types}.
90
91 \subsection{Overview of Types and Classes}
92 \label{types-overview}
93
94 \Haskell{} uses a traditional
95 Hindley-Milner\index{Hindley-Milner type system}
96 polymorphic type system to provide a static type semantics
97 \cite{damas-milner82,hindley69}, but the type system has been extended with
98 {\em type classes} (or just {\em
99 classes}\index{class}) that provide 
100 a structured way to introduce {\em overloaded} functions.\index{type
101 class} \index{constructor class} \index{overloaded functions}
102
103 A @class@ declaration (Section~\ref{class-decls}) introduces a new
104 {\em type class} and the overloaded operations that must be
105 supported by any type that is an instance of that class.  An
106 @instance@ declaration (Section~\ref{instance-decls}) declares that a
107 type is an {\em instance} of a class and includes
108 the definitions of the overloaded operations---called {\em
109 class methods}---instantiated on the named type.
110 \index{class method}
111
112 For example, suppose we wish to overload the operations @(+)@ and
113 @negate@ on types @Int@ and @Float@.  We introduce a new
114 type class called @Num@:\nopagebreak[4]
115 \par
116 {\small
117 \bprog
118 @
119   class Num a  where          -- simplified class declaration for Num
120     (+)    :: a -> a -> a     -- (Num is defined in the Prelude)
121     negate :: a -> a
122 @
123 \eprog
124 }
125 This declaration may be read ``a type @a@ is an instance of the class
126 @Num@ if there are class methods @(+)@ and @negate@, of the
127 given types, defined on it.''
128
129 We may then declare @Int@ and @Float@ to be instances of this class:
130 \bprog
131 @
132   instance Num Int  where     -- simplified instance of Num Int
133     x + y       =  addInt x y
134     negate x    =  negateInt x
135   
136   instance Num Float  where   -- simplified instance of Num Float
137     x + y       =  addFloat x y
138     negate x    =  negateFloat x
139 @
140 \eprog
141 where @addInt@, @negateInt@, @addFloat@, and @negateFloat@ are assumed
142 in this case to be primitive functions, but in general could be any
143 user-defined function.  The first declaration above may be read
144 ``@Int@ is an instance of the class @Num@ as witnessed by these
145 definitions (i.e.~class methods)\index{class method} for @(+)@ and @negate@.''
146
147 More examples of type classes can be found in
148 the papers by Jones \cite{jones:cclasses} or Wadler and Blott
149 \cite{wadler:classes}. 
150 The term `type class' was used to describe the original \Haskell{} 1.0
151 type system; `constructor class' was used to describe an extension to
152 the original type classes.  There is no longer any reason to use two
153 different terms: in this report, `type class' includes both the
154 original \Haskell{} type classes and the constructor classes
155 introduced by Jones.
156
157 \subsubsection{Kinds}
158
159 To ensure that they are valid, type expressions are classified
160 into different {\em kinds}, \index{kind} which take one of two possible
161 forms:\nopagebreak[4]
162 \begin{itemize}
163
164 \item The symbol $\ast$ represents the kind of all nullary type
165 constructors.
166
167 \item If $\kappa_1$ and $\kappa_2$ are kinds, then $\kappa_1\rightarrow\kappa_2$
168 is the kind of types that take a type of kind $\kappa_1$ and return
169 a type of kind $\kappa_2$.
170 \end{itemize}
171 Kind inference checks the validity of type expressions 
172 in a similar way that type inference checks the validity of value expressions.  
173 However, unlike types, kinds are entirely
174 implicit and are not a visible part of the language.  Kind inference is discussed
175 in Section~\ref{kindinference}.
176
177 \subsubsection{Syntax of Types}
178 \label{type-syntax}
179 \index{type}
180 \label{types}
181
182 @@@
183 type      -> btype [@->@ type]                    & (\tr{function type})
184
185 btype    ->  [btype] atype                        & (\tr{type application})
186
187 atype    ->  gtycon
188           |  tyvar
189           |  @(@ type_1 @,@ ... @,@ type_k @)@ & (\tr{tuple type}, k>=2)
190           |  @[@ type @]@                      & (\tr{list type})
191           |  @(@ type @)@                      & (\tr{parenthesised constructor})
192
193 gtycon    -> qtycon
194           |  @()@                              & (\tr{unit type})
195           |  @[]@                              & (\tr{list constructor})
196           |  @(->)@                            & (\tr{function constructor})
197           |  @(,@\{@,@\}@)@                    & (\tr{tupling constructors})
198 @@@
199 \indexsyn{type}%
200 \indexsyn{atype}%
201 \indexsyn{btype}%
202 \indexsyn{gtycon}%
203
204 \noindent
205 The syntax for \Haskell{} type expressions
206 \index{type expression}
207 \index{constructor expression}
208 is given above.  Just as data values are built using data
209 constructors, type values are built from "type constructors".  As with
210 data constructors, the names of type constructors start with uppercase
211 letters.
212 Unlike data constructors, infix type constructors are not allowed (other than @(->)@).
213
214 The main forms of type expression are as follows:\nopagebreak[4]
215 \begin{enumerate}
216
217 \item Type variables, written as identifiers beginning with
218       a lowercase letter.  The kind of a variable is determined implicitly
219       by the context in which it appears.
220
221 \item Type constructors.  Most type constructors are written as an identifier
222       beginning with an uppercase letter.  For example:\nopagebreak[4]
223       \begin{itemize}
224       \item @Char@, @Int@, @Integer@, @Float@, @Double@ and @Bool@ are
225             type constants with kind $\ast$.
226       \item @Maybe@ and @IO@ are unary type
227             constructors, and treated as types with
228             kind $\ast\rightarrow\ast$.
229       \item The declarations @data T ...@ or @newtype T ...@ add the type
230             constructor @T@ to
231             the type vocabulary.  The kind of @T@ is determined by
232             kind inference.
233       \end{itemize}
234       Special syntax is provided for certain built-in type constructors:\nopagebreak[4]
235       \begin{itemize}
236       \item The {\em trivial type}\index{trivial type} is written as @()@ and
237             has kind $\ast$.
238             It denotes the ``nullary tuple'' type, and has exactly one value,
239             also written @()@ (see Sections~\ref{unit-expression}
240             and~\ref{basic-trivial}).
241       \item The {\em function type} is written as @(->)@ and has\index{function type}
242             kind $\ast\rightarrow\ast\rightarrow\ast$.
243       \item The {\em list type}  is written as @[]@ and has kind
244             $\ast\rightarrow\ast$.\index{list}
245       \item The {\em tuple types} are written as @(,)@,\index{tuple}
246             @(,,)@, and so on.  Their kinds are
247             $\ast\rightarrow\ast\rightarrow\ast$,
248             $\ast\rightarrow\ast\rightarrow\ast\rightarrow\ast$,  and
249             so on.
250       \end{itemize}
251       Use of the @(->)@ and @[]@ constants is described in more detail below.
252
253 \item Type application.  If $t_1$ is a type of kind
254       $\kappa_1\rightarrow\kappa_2$ and $t_2$ is a type of kind $\kappa_1$,
255       then $t_1~t_2$ is a type expression of kind $\kappa_2$.
256
257 \item A {\em parenthesized type}, having form "@(@t@)@", is identical
258       to the type "t".
259
260 \end{enumerate}
261 For example, the type expression @IO a@ can be understood as the application
262 of a constant, @IO@, to the variable @a@.  Since the @IO@ type
263 constructor has kind 
264 $\ast\rightarrow\ast$, it follows that both the variable @a@ and the whole
265 expression, @IO a@, must have kind $\ast$.
266 In general, a process of {\em kind inference}\index{kind}\index{kind inference}
267 (see Section~\ref{kindinference})
268 is needed to determine appropriate kinds for user-defined datatypes, type
269 synonyms, and classes.
270
271 Special syntax is provided to allow certain type expressions to be written
272 in a more traditional style:\nopagebreak[4]
273 \begin{enumerate}
274
275 \item A {\em function type}\index{function type} has the form
276 "t_1 @->@ t_2", which is equivalent to the type
277 "@(->)@ t_1 t_2".  Function arrows associate to the right.
278 For example, @Int -> Int -> Float@ means @Int -> (Int -> Float)@.
279
280 \item A {\em tuple type}\index{tuple type} has the form 
281 "@(@t_1@,@ ... @,@ t_k@)@" where "k>=2", which is equivalent to
282 the type "@(,@$\ldots$@,)@ t_1 ... t_k" where there are
283 $k-1$ commas between the parenthesis.  It denotes the
284 type of "k"-tuples with the first component of type "t_1", the second
285 component of type "t_2", and so on (see Sections~\ref{tuples}
286 and \ref{basic-tuples}).
287
288 \item A {\em list type}\index{list type} has the form "@[@t@]@",
289 which is equivalent to the type "@[]@ t".
290 It denotes the type of lists with elements of type "t" (see
291 Sections~\ref{lists} and \ref{basic-lists}).
292
293 \end{enumerate}
294 These special syntactic forms always denote the built-in type constructors
295 for functions, tuples, and lists, regardless of what is in scope.
296 In a similar way, the prefix type constructors @(->)@, @[]@, @()@, @(,)@, 
297 and so on, always denote the built-in type constructors; they 
298 cannot be qualified, nor mentioned in import or export lists (Chapter~\ref{modules}).
299 (Hence the special production, ``gtycon'', above.)
300
301 Although the list and tuple types have special syntax, their semantics 
302 is the same as the equivalent user-defined algebraic data types.
303
304 Notice that expressions and types have a consistent syntax.
305 If "t_i" is the type of
306 expression or pattern "e_i", then the expressions "@(\@ e_1 @->@ e_2@)@",
307 "@[@e_1@]@", and "@(@e_1,e_2@)@" have the types "@(@t_1 @->@ t_2@)@",
308 "@[@t_1@]@", and "@(@t_1,t_2@)@", respectively.
309
310 \index{quantification}
311 With one exception (that of the distinguished type variable
312 in a class declaration (Section~\ref{class-decls})), the
313 type variables in a \Haskell{} type expression
314 are all assumed to be universally quantified; there is no explicit
315 syntax for universal quantification~\cite{damas-milner82}.
316 % \cite{damas-milner82,reynolds90}.
317 For example, the type expression
318 @a -> a@ denotes the type "\forall a.~a \rightarrow a".
319 For clarity, however, we often write quantification explicitly
320 when discussing the types of \Haskell{} programs.  When we write an
321 explicitly quantified type, the scope of the "\forall" extends as far
322 to the right as possible; for example, "\forall a.~a \rightarrow a" means
323 "\forall a.~(a \rightarrow a)".
324
325 %Every type variable appearing in a signature
326 %is universally quantified over that signature.  This last
327 %constraint implies that signatures such as:
328 %\bprog
329 %@@
330 %       \ x -> ([x] :: [a])
331 %@@
332 %\eprog
333 %are not valid, because this declares @[x]@ to be of type 
334 %"\forall a.@[@a@]@".  In contrast, this {\em is} a valid signature:
335 %@(\ x -> [x]) :: a -> [a]@; it declares that @(\ x -> [x])@ has type
336 %"\forall a.a @->@ @[@a@]@".
337
338 \subsubsection{Syntax of Class Assertions and Contexts}
339 \index{class assertion}
340 \index{context}
341 \label{classes&contexts}
342
343 @@@
344 context -> class
345         |  @(@ class_1 @,@ ... @,@ class_n @)@          & (n>=0)
346 class   -> qtycls tyvar
347         |  qtycls @(@ tyvar atype_1 ...  atype_n @)@ & (n>=1)
348 qtycls  -> [ modid @.@ ] tycls
349 tycls   -> conid
350 tyvar   -> varid
351 @@@
352 \indexsyn{context}%
353 \indexsyn{class}%
354 \indexsyn{simpleclass}%
355 \indexsyn{tycls}%
356 \indexsyn{tyvar}%
357
358 A {\em class assertion} has form "qtycls tyvar", and
359 indicates the membership of the type "tyvar" in the class
360 "qtycls".  A class identifier begins with an uppercase
361 letter.
362 A {\em context} consists of zero or more class assertions,
363 and has the general form
364 \[
365 "@(@ C_1 u_1, ..., C_n u_n @)@"
366 \]
367 where "C_1, ..., C_n" are class identifiers, and each of the "u_1, ..., u_n" is
368 either a type variable, or the application of type variable to one or more types.
369 The outer parentheses may be omitted when "n=1".  In
370 general, we use "cx" to denote a context and we write "cx @=>@ t" to
371 indicate the type "t" restricted by the context "cx".
372 The context "cx" must only contain type variables referenced in "t".
373 For convenience,
374 we write "cx @=>@ t" even if the context "cx" is empty, although in this
375 case the concrete syntax contains no @=>@.
376
377 \subsubsection{Semantics of Types and Classes}
378 \label{type-semantics}
379
380 In this section, we provide informal details of the type system.
381 % the formal semantics is described in Appendix~\ref{static-semantics}
382 (Wadler and Blott \cite{wadler:classes} and Jones
383 \cite{jones:cclasses} discuss type
384 and constructor classes, respectively, in more detail.)
385
386 %A type is a {\em monotype\/}\index{monotype} if it contains no type
387 %variables, and is {\em monomorphic\/}
388 %\index{monomorphic type}
389 %if it contains type variables
390 %but is not polymorphic (in Milner's original terminology,
391 %it is monomorphic if it contains no generic type variables).
392
393 The \Haskell{} type system attributes a {\em type} to each
394 \index{type}
395 expression in the program.  In general, a type is of the form
396 "\forall \overline{u}.~cx \Rightarrow t",
397 where "\overline{u}" is a set of type variables "u_1, ..., u_n".
398 In any such type, any of the universally-quantified type variables "u_i"
399 that are free in "cx" must also be free in "t".
400 Furthermore, the context "cx" must be of the form given above in
401 Section~\ref{classes&contexts}.  For example, here are some
402 valid types:
403 \bprog
404 @
405   Eq a => a -> a
406   (Eq a, Show a, Eq b) => [a] -> [b] -> String
407   (Eq (f a), Functor f) => (a -> b) -> f a -> f b -> Bool
408 @
409 \eprog
410 In the third type, the constraint @Eq (f a)@ cannot be made
411 simpler because @f@ is universally quantified.
412
413 The type of an expression "e" depends 
414 on a {\em type environment}\index{type environment} that gives types 
415 for the free variables in "e", and a
416 {\em class environment}\index{class environment} that 
417 declares which types are instances of which classes (a type becomes
418 an instance of a class only via the presence of an
419 @instance@ declaration or a @deriving@ clause).
420
421 Types are related by a generalization preorder
422 \index{generalization preorder}
423 (specified below);
424 the most general type, up to the equivalence induced by the generalization preorder,
425 that can be assigned to a particular
426 expression (in a given environment) is called its {\em
427 principal type}.
428 \index{principal type}
429 \Haskell{}'s extended Hindley-Milner type system can infer the principal
430 type of all expressions, including the proper use of overloaded
431 class methods (although certain ambiguous overloadings could arise, as
432 described in Section~\ref{default-decls}).  Therefore, explicit typings (called
433 {\em type signatures})
434 \index{type signature}
435 are usually optional (see
436 Sections~\ref{expression-type-sigs} and~\ref{type-signatures}).
437
438 The type "\forall \overline{u}.~cx_1 \Rightarrow t_1" is
439 {\em more general than} the 
440 type "\forall \overline{w}.~cx_2 \Rightarrow t_2" if and only if there is 
441 a substitution "S" whose domain is "\overline{u}" such that:
442 \begin{itemize}
443 \item "t_2" is identical to "S(t_1)".
444 \item Whenever "cx_2" holds in the class environment, "S(cx_1)" also holds.
445 \end{itemize}
446
447 A value of type
448 "\forall \overline{u}.~cx \Rightarrow t",
449 may be instantiated at types "\overline{s}" if and only if
450 the context "cx[\overline{s}/\overline{u}]" holds.
451 For example, consider the function @double@:
452 \bprog
453 @
454   double x = x + x
455 @
456 \eprog
457 The most general type of @double@ is
458 "\forall a.~@Num@~a \Rightarrow a \rightarrow a".
459 @double@ may be applied to values of type @Int@ (instantiating "a" to
460 @Int@), since @Num Int@ holds, because @Int@ is an instance of the class @Num@.
461 However, @double@ may not normally be applied to values
462 of type @Char@, because @Char@ is not normally an instance of class @Num@.  The
463 user may choose to declare such an instance, in which case @double@ may
464 indeed be applied to a @Char@.
465
466
467 \subsection{User-Defined Datatypes}
468 \index{datatype}
469 \label{user-defined-datatypes}
470
471 In this section, we describe algebraic datatypes (@data@
472 declarations), renamed datatypes (@newtype@ declarations), and type
473 synonyms (@type@ declarations).  These declarations may only appear at
474 the top level of a module.
475
476 \subsubsection{Algebraic Datatype Declarations}
477 \index{algebraic datatype}
478 \label{datatype-decls}
479
480 @@@
481 topdecl    -> @data@ [context @=>@] simpletype @=@ constrs [deriving]
482
483 simpletype -> tycon tyvar_1 ... tyvar_k  & (k>=0) 
484
485 constrs    -> constr_1 @|@ ... @|@ constr_n     & (n>=1)
486 constr     -> con [@!@] atype_1 ... [@!@] atype_k       & (\tr{arity} con = k, k>=0)
487            |  (btype | @!@ atype) conop (btype | @!@ atype) & (\tr{infix} conop)
488            |  con @{@ fielddecl_1 @,@ ... @,@ fielddecl_n @}@ & (n>=0)
489 fielddecl  -> vars @::@ (type | @!@ atype)
490
491 deriving   -> @deriving@ (dclass | @(@dclass_1@,@ ... @,@ dclass_n@)@)& (n>=0)
492 dclass     -> qtycls
493 @@@
494 \index{topdecl@@{\em topdecl} (@data@)}%
495 \indexsyn{simpletype}%
496 \indexsyn{constrs}%
497 \indexsyn{constr}%
498 \indexsyn{fielddecl}%
499 \indexsyn{deriving}%
500 \indexsyn{dclass}%
501 \index{data declaration@@{\tt data} declaration}
502 The precedence\index{precedence} for "constr" is the same as that for
503 expressions---normal constructor application has higher precedence
504 than infix constructor application (thus @a : Foo a@ parses as 
505 @a : (Foo a)@).
506
507 An algebraic datatype declaration has the form:
508 \[
509 "@data@ cx @=>@ T u_1 ... u_k @=@ K_1 t_{11} ... t_{1k_1} @|@ \cdots @|@ \
510                                 K_n t_{n1} ... t_{nk_n}"
511 \]
512 where "cx" is a context.
513 %\index{context!in data declaration@@in {\tt data} declaration}
514 This declaration
515 introduces a new {\em type constructor} "T" with one or more constituent {\em data
516 constructors} "K_1, ..., K_n".
517 \index{data constructor}\index{type constructor}
518 In this Report, the unqualified term ``constructor'' always means ``data constructor''.
519
520 The types of the data constructors are given by:
521 \[
522 "K_i :: \forall u_1 ... u_k.~ cx_i \Rightarrow t_{i1} \rightarrow \cdots \rightarrow t_{ik_i} \rightarrow (T u_1 ... u_k)"
523 \]
524 where "cx_i" is the largest subset of "cx" that constrains only those type
525 variables free in the types "t_{i1}, ..., t_{ik_i}".
526 The type variables "u_1" through "u_k" must be distinct and may appear
527 in "cx" and the "t_{ij}"; it is a static error
528 for any other type variable to appear in "cx" or on the right-hand-side.
529 The new type constant "T" has a kind of the form
530 $\kappa_1\rightarrow\ldots\rightarrow\kappa_k\rightarrow\ast$
531 where the kinds "\kappa_i" of the argument variables "u_i" are
532 determined by kind inference
533 as described in Section~\ref{kindinference}\index{kind}\index{kind inference}.
534 This means that "T" may be used in type expressions with anywhere
535 between "0" and "k" arguments.
536
537 For example, the declaration
538 \bprog
539 @
540   data Eq a => Set a = NilSet | ConsSet a (Set a)
541 @
542 \eprog
543 introduces a type constructor @Set@ of kind $\ast\rightarrow\ast$, and constructors @NilSet@ and
544 @ConsSet@ with types
545 \[\ba{ll}
546 @NilSet@  & ":: \forall a.~ @Set@~ a" \\
547 @ConsSet@ & ":: \forall a.~ @Eq@~ a \Rightarrow a \rightarrow @Set@~ a \rightarrow @Set@~ a"
548 \ea\]
549 In the example given, the overloaded
550 type for @ConsSet@ ensures that @ConsSet@ can only be applied to values whose
551 type is an instance of the class @Eq@.  
552 Pattern matching against @ConsSet@ also gives rise to an @Eq a@ constraint. 
553 For example: 
554 \bprog
555 @
556   f (ConsSet a s) = a
557 @
558 \eprog
559 the function @f@ has inferred type @Eq a => Set a -> a@.
560 The context in the @data@ declaration has no other effect whatsoever.
561
562 The visibility of a datatype's constructors (i.e.~the ``abstractness''
563 \index{abstract datatype}
564 of the datatype) outside of the module in which the datatype is
565 defined is controlled by the form of the datatype's name in the export
566 list as described in Section~\ref{abstract-types}.
567
568 The optional "@deriving@" part of a @data@ declaration has to do
569 with {\em derived instances}, and is described in
570 Section~\ref{derived-decls}.
571
572 \paragraph{Labelled Fields}
573 \label{field-labels}
574 \index{field label}
575 A data constructor of arity "k" creates an object with "k" components.
576 These components are normally accessed positionally as arguments to the
577 constructor in expressions or patterns.  For large datatypes it is
578 useful to assign "field labels" to the components of a data object.
579 This allows a specific field to be referenced independently of its
580 location within the constructor.
581
582 A constructor definition in a @data@ declaration may assign labels to the
583 fields of the constructor, using the record syntax (@C { ... }@).
584 Constructors using field labels may be freely mixed with constructors
585 without them. 
586 A constructor with associated field labels may still be used as an
587 ordinary constructor; features using labels are
588 simply a shorthand for operations using an underlying positional
589 constructor.  The arguments to the positional constructor occur in the
590 same order as the labeled fields.  For example, the declaration
591 \bprog
592 @
593   data C = F { f1,f2 :: Int, f3 :: Bool}
594 @
595 \eprog
596 defines a type and constructor identical to the one produced by
597 \bprog
598 @
599   data C = F Int Int Bool
600 @
601 \eprog
602 Operations using field labels are described in Section~\ref{field-ops}.
603 A @data@ declaration may use the same field label in multiple
604 constructors as long as the typing of the field is the same in all
605 cases after type synonym expansion.  A label cannot be shared by
606 more than one type in scope.  Field names share the top level namespace
607 with ordinary variables and class methods and must not conflict with
608 other top level names in scope.
609
610 The pattern @F {}@ matches any value built with constructor @F@, 
611 {\em whether or not @F@ was declared with record syntax}. 
612
613 \paragraph{Strictness Flags}
614 \label{strictness-flags}
615 \index{strictness flag}
616 Whenever a data constructor is applied, each argument to the
617 constructor is evaluated if and only if the corresponding type in the
618 algebraic datatype declaration has a strictness flag, denoted by
619 an exclamation point, ``@!@''.
620 \index{""!@@{\tt  {\char'041}}}
621 Lexically, ``@!@'' is an ordinary varsym not a "reservedop"; 
622 it has special significance only in the context of the argument types of 
623 a data declaration.
624
625
626 \outline{
627 \paragraph*{Translation:}
628 A declaration of the form
629 \[
630 "@data@ cx @=>@ T u_1 ... u_k @=@ ... @|@ K s_{1} ... s_{n} @|@ ... "
631 \]
632 where each "s_i" is either of the form @!@" t_i" or "t_i", replaces
633 every occurrence of "K" in an expression by 
634 \[
635 "@(\ @x_1 ... x_n @->@ ( ((K op_1 x_1) op_2 x_2) ... ) op_n x_n)"
636 \]
637 where "op_i" is the non-strict apply function @$@ if "s_i" is of the form "t_i",
638 and "op_i" is the strict apply function @$!@ (see
639 Section~\ref{strict-eval}) if "s_i" is of the form "@!@ t_i".  Pattern
640 matching on "K" is not affected by strictness flags.
641 }
642
643
644 \subsubsection{Type Synonym Declarations}
645 \index{type synonym}
646 \label{type-synonym-decls}
647
648 @@@
649 topdecl    -> @type@ simpletype @=@ type
650 simpletype ->  tycon tyvar_1 ... tyvar_k & (k>=0) 
651 @@@
652 \index{topdecl@@{\em topdecl} (@type@)}%
653 \indexsyn{simpletype}%
654 A type synonym declaration introduces a new type that
655 is equivalent to an old type.  It has the form
656 \[
657 "@type@ T u_1 ... u_k @=@ t"
658 \]
659 which introduces a new type constructor, "T".  The type "(T t_1 ...
660 t_k)" is equivalent to the type "t[t_1/u_1, ..., t_k/u_k]".  The type
661 variables "u_1" through "u_k" must be distinct and are scoped only
662 over "t"; it is a static error for any other type variable to appear
663 in "t".  The kind of the new type constructor "T" is of the form
664 $\kappa_1\rightarrow\ldots\rightarrow\kappa_k\rightarrow\kappa$ where
665 the kinds "\kappa_i" of the arguments "u_i" and "\kappa" of the right hand
666 side "t" are determined by kind inference as described in
667 Section~\ref{kindinference}\index{kind}\index{kind inference}.
668 For example, the following definition can be used to provide an alternative
669 way of writing the list type constructor: 
670 \bprog
671 @
672   type List = []
673 @
674 \eprog
675 Type constructor symbols "T" introduced by type synonym declarations cannot
676 be partially applied; it is a static error to use "T" without the full number
677 of arguments.
678
679 Although recursive and mutually recursive datatypes are allowed,
680 \index{recursive datatype}
681 \index{type synonym!recursive}
682 this is not so for type synonyms, {\em unless an algebraic datatype
683 intervenes}.  For example,
684 \bprog
685 @
686   type Rec a   =  [Circ a]
687   data Circ a  =  Tag [Rec a]
688 @
689 \eprog
690 is allowed, whereas
691 \bprog
692 @
693   type Rec a   =  [Circ a]        -- invalid
694   type Circ a  =  [Rec a]         -- invalid
695 @
696 \eprog
697 is not. Similarly, @type Rec a = [Rec a]@ is not allowed.
698
699 Type synonyms are a convenient, but strictly syntactic, mechanism to make type
700 signatures more readable.  A synonym and its definition are completely
701 interchangeable, except in the instance type of an @instance@ declaration (Section~\ref{instance-decls}).
702
703 \subsubsection{Datatype Renamings}
704 \index{newtype declaration@@{\tt newtype} declaration}
705 \label{datatype-renaming}
706
707 @@@
708 topdecl    -> @newtype@ [context @=>@] simpletype @=@ newconstr [deriving]
709 newconstr  -> con atype
710            |  con @{@ var @::@ type @}@ 
711 simpletype ->  tycon tyvar_1 ... tyvar_k                & (k>=0)
712 @@@
713 \index{topdecl@@{\em topdecl} (@newtype@)}%
714 \indexsyn{simpletype}%
715 \indexsyn{newconstr}%
716
717 \noindent \noindent A declaration of the form
718 \[
719 "@newtype@ cx @=>@ T u_1 ... u_k @=@ N t"
720 \]
721 introduces a new type whose
722 representation is the same as an existing type.  The type "@(@T u_1
723 ... u_k@)@" renames the datatype "t".
724 It differs from a type synonym in
725 that it creates a distinct type that must be explicitly coerced to or
726 from the original type.  Also, unlike type synonyms, @newtype@ may be
727 used to define recursive types.
728 The constructor "N" in an expression 
729 coerces a value from type "t" to type "@(@T u_1 ... u_k@)@".
730 Using "N" in a pattern coerces a value from type "@(@T u_1 ... u_k@)@"
731 to type "t".  These coercions may be implemented without
732 execution time overhead; @newtype@ does not change the underlying
733 representation of an object.
734
735 New instances (see Section \ref{instance-decls}) can be defined for a
736 type defined by @newtype@ but may not be defined for a type synonym.  A type
737 created by @newtype@ differs from an algebraic datatype in that the
738 representation of an
739 algebraic datatype has an extra level of indirection.  This difference
740 may make access to the representation less efficient.  The difference is
741 reflected in different rules for pattern matching (see
742 Section~\ref{pattern-matching}).  Unlike algebraic datatypes, the
743 newtype constructor "N" is {\em unlifted}, so that "N \bot"
744 is the same as "\bot".
745
746 The following examples clarify the differences between @data@ (algebraic
747 datatypes), @type@ (type synonyms), and @newtype@ (renaming types.)
748 Given the declarations 
749 \bprog
750 @
751   data D1 = D1 Int
752   data D2 = D2 !Int
753   type S = Int
754   newtype N = N Int
755   d1 (D1 i) = 42
756   d2 (D2 i) = 42
757   s i = 42
758   n (N i) = 42
759 @
760 \eprog
761 the expressions "@(@ @d1@ \bot @)@", "@(@ @d2@ \bot @)@" and 
762 "@(d2 (D2@ \bot @) )@" are all
763 equivalent to "\bot", whereas "@(@ @n@ \bot @)@", "@(@ @n@ @(@ @N @
764 \bot @) )@", "@(@ @d1@ @(@ @D1@ \bot @) )@" and "@(@ @s@ \bot @)@"
765 are all equivalent to @42@.  In particular, "@(@ @N@ \bot @)@" is equivalent to
766 "\bot" while "@(@ @D1@ \bot @)@" is not equivalent to "\bot".
767
768 The optional deriving part of a @newtype@ declaration is treated in
769 the same way as the deriving component of a @data@ declaration; see
770 Section~\ref{derived-decls}.
771
772 A @newtype@ declaration may use field-naming syntax, though of course
773 there may only be one field.  Thus:
774 \bprog
775 @
776   newtype Age = Age { unAge :: Int }
777 @
778 \eprog
779 brings into scope both a constructor and a de-constructor:
780 \bprog
781 @
782   Age   :: Int -> Age
783   unAge :: Age -> Int
784 @
785 \eprog
786
787 \subsection{Type Classes and Overloading}
788 \index{class}
789 \index{overloading}
790 \label{overloading}
791 \label{classes}
792
793 \subsubsection{Class Declarations}
794 \index{class declaration}
795 %\index{class declaration@@{\tt class} declaration}
796 \label{class-decls}
797
798 @@@
799 topdecl -> @class@ [scontext @=>@] tycls tyvar [@where@ cdecls]
800 scontext -> simpleclass
801         |  @(@ simpleclass_1 @,@ ... @,@ simpleclass_n @)@              & (n>=0)
802 simpleclass -> qtycls tyvar                     
803 cdecls  -> @{@ cdecl_1 @;@ ... @;@ cdecl_n @}@          & (n>=0)
804 cdecl   -> gendecl
805         |  (funlhs | var) rhs
806 @@@
807 \index{topdecl@@{\em topdecl} (@class@)}%
808 \indexsyn{gendecl}%
809 \indexsyn{cdecls}%
810 \indexsyn{cdecl}%
811 \index{declaration!within a {\tt class} declaration}
812
813 \noindent
814 A {\em class declaration} introduces a new class and the operations
815 ({\em class methods}) on it.
816 A class declaration has the general form:
817 \[\ba{rl}
818 "@class@ cx @=>@ C u @where@ cdecls"
819 % "@{@"&"...@;@ v_i @::@ cx_i @=>@ t_i @;@ ...@;@"\\
820 %                               &"...@;@ @infix@ n v_i@;@ ...@;@"\\
821 %                               &"valdef_1 @;@ ... @;@ valdef_m @}@"
822 \ea\]
823 This introduces a new class name "C"; the type variable "u" is
824 scoped only over the class method signatures in the class body.
825 The context "cx" specifies the superclasses\index{superclass} of "C", as
826 described below; the only type variable that may be referred to in "cx"
827 is "u".
828
829 The superclass relation must not be cyclic; i.e.~it must form a
830 directed acyclic graph.\index{superclass}
831
832 The "cdecls" part of a @class@ declaration contains three kinds
833 of declarations:
834 \begin{itemize}
835 \item
836 The class declaration introduces new {\em class methods}
837 \index{class method}
838 "v_i", whose scope extends outside the @class@ declaration.
839 The class methods of a class declaration are precisely the "v_i" for
840 which there is an explicit type signature
841 \[
842 "v_i @::@ cx_i @=>@ t_i"
843 \]
844 in "cdecls".  
845 Class methods share the top level namespace with variable
846 bindings and field names; they must not conflict with other top level
847 bindings in scope. 
848 That is, a class method can 
849 not have the same name as a top level definition, a field name, or
850 another class method.
851
852 The type of the top-level class method "v_i" is:
853 \[
854 v_i :: \forall u,\overline{w}.~(C u, cx_i) \Rightarrow t_i
855 \]
856 The "t_i" must mention "u"; it may mention type variables
857 "\overline{w}" other than "u", in which case the type of "v_i" is
858 polymorphic in both "u" and "\overline{w}\/".
859 The "cx_i" may constrain only "\overline{w}"; in particular,
860 the "cx_i" may not constrain "u".
861 For example:
862 \bprog
863 @
864   class Foo a where
865     op :: Num b => a -> b -> a
866 @
867 \eprog
868 Here the type of @op@ is
869 "\forall a, b.~(@Foo@~a,~@Num@~b)~ \Rightarrow a \rightarrow b \rightarrow a".
870
871 \item
872 The "cdecls" may also contain a {\em fixity declaration} for any of the class methods 
873 (but for no other values).
874 \index{fixity declaration}
875 However, since class methods declare top-level values, the fixity declaration for a class
876 method may alternatively appear at top level, outside the class declaration.
877
878 \item
879 Lastly, the "cdecls" may contain a
880 {\em default class method}
881 \index{default class method}
882 for any of the "v_i".  The default class method for "v_i" is used if no binding for it
883 is given in a particular @instance@ declaration (see
884 Section~\ref{instance-decls}).
885 The default method declaration is a normal value definition, except that the
886 left hand side may only be a variable or function definition.  For example:
887 \bprog
888 @
889   class Foo a where
890     op1, op2 :: a -> a
891     (op1, op2) = ...
892 @
893 \eprog
894 is not permitted, because the left hand side of the default declaration is a
895 pattern.
896 \end{itemize}
897 Other than these cases, no other declarations are permitted in "cdecls".
898
899 %Figure~\ref{standard-classes} shows some standard \Haskell{} classes,
900 %including the use of superclasses.
901 %; note the class inclusion diagram on the right.
902 %For example, @Eq@ is a superclass of @Ord@, and thus in
903 %any context @Ord a@ is equivalent to @(Eq a, Ord a)@.  Figures~\ref{data-class},
904 %\ref{prelude-bool} and \ref{numeric-inclusions} show the remaining
905 %standard \Haskell{} classes.
906
907 A @class@
908 declaration with no @where@ part
909 \index{class declaration!with an empty @where@ part}
910 may be useful for combining a
911 collection of classes into a larger one that inherits all of the
912 class methods in the original ones.  For example:
913 \bprog
914 @
915   class  (Read a, Show a) => Textual a
916 @
917 \eprog
918 In such a case, if a type is an instance of all
919 superclasses,\index{superclass} it is 
920 not {\em automatically} an instance of the subclass, even though the
921 subclass has no immediate class methods.  The @instance@ declaration must be
922 given explicitly with no @where@ part.
923 \index{instance declaration!with an empty @where@ part}
924
925 \subsubsection{Instance Declarations}
926 \label{instance-decls}
927 \index{instance declaration}
928
929 @@@
930 topdecl -> @instance@ [scontext @=>@] qtycls inst [@where@ idecls]
931 inst    -> gtycon
932         |  @(@ gtycon tyvar_1 ... tyvar_k @)@   & (k>=0, tyvars {\rm distinct})
933         |  @(@ tyvar_1 @,@ ... @,@ tyvar_k @)@  & (k>=2, tyvars {\rm distinct})
934         |  @[@ tyvar @]@
935         |  @(@ tyvar_1 @->@ tyvar_2 @)@         & (tyvar_1 {\rm and} tyvar_2 {\rm distinct})
936 idecls  -> @{@ idecl_1 @;@ ... @;@ idecl_n @}@          & (n>=0)
937 idecl   -> (funlhs | var) rhs
938         |                                               & (empty)
939 @@@
940 \index{topdecl@@{\em topdecl} (@instance@)}
941 \indexsyn{inst}%
942 \indexsyn{valdefs}%
943 \indexsyn{gtycon}%
944 \indexsyn{idecl}%
945 \indexsyn{idecls}%
946 %\index{instance declaration@@{\tt instance} declaration}
947 \index{declaration!within an {\tt instance} declaration}
948 %\ToDo{tycls left off above}
949 An {\em instance declaration} introduces an instance of a class.  Let
950 \[ "@class@ cx @=>@ C u @where@ @{@ cbody @}@" \]
951 be a @class@ declaration.  The general form of the corresponding
952 instance declaration is:
953 \[ "@instance@ cx' @=>@ C (T u_1 ... u_k) @where@ @{@ d @}@" \]
954 where "k\geq0".
955 The type "(T u_1 ... u_k)" must take the form of
956 a type constructor "T" applied to simple type variables "u_1, ... u_k";
957 furthermore, "T" must not be a type synonym\index{type synonym}, 
958 and the "u_i" must all be distinct.
959
960 This prohibits instance declarations
961 such as:
962 \bprog
963 @
964   instance C (a,a) where ...
965   instance C (Int,a) where ...
966   instance C [[a]] where ...
967 @
968 \eprog
969 The declarations "d" may contain bindings only for the class
970 methods\index{class method} of "C".  It is illegal to give a 
971 binding for a class method that is not in scope, but the name under
972 which it is in scope is immaterial; in particular, it may be a qualified
973 name.  (This rule is identical to that used for subordinate names in
974 export lists --- Section~\ref{export}.)
975 For example, this is legal, even though @range@ is in scope only
976 with the qualified name @Ix.range@.
977 \bprog
978 @
979   module A where
980     import qualified Ix
981
982     instance Ix.Ix T where
983       range = ...
984 @
985 \eprog
986 The declarations may not contain any type
987 signatures or fixity declarations,\index{type signature}\index{fixity declaration}
988 since these have already been given in the @class@
989 declaration.  As in the case of default class methods
990 \index{default class method}%
991 (Section~\ref{class-decls}), the method declarations must take the form of
992 a variable or function definition.
993
994 % However, unlike other declarations, the name of the bound
995 % variable may be qualified.  So this is legal:
996 % \bprog
997
998 %  module A where
999 %    import qualified B( Foo(op) )
1000 %    instance B.Foo Int where
1001 %      B.op = ...
1002 %
1003 %\eprog
1004 % Here, module @A@ imports class @Foo@ from module @B@, and then gives an 
1005 %instance declaration for @Foo@.  Since @B@ is imported @qualified@, the name
1006 %of the class method, @op@, is not in scope; so the definition must define @B.op@.
1007 % Hence the need for the "qfunlhs" and "qvar" left hand sides in "idecl".
1008
1009 If no binding is given for some class method then the
1010 corresponding default class method
1011 \index{default class method}
1012 in the @class@ declaration is used (if
1013 present); if such a default does
1014 not exist then the class method of this instance
1015 is bound to @undefined@ 
1016 and no compile-time error results.
1017
1018 An @instance@ declaration that makes the type "T" to be an instance
1019 of class "C" is called a {\em C-T instance declaration}
1020 \index{instance declaration} and is
1021 subject to these static restrictions:
1022 %\index{instance declaration!with respect to modules}
1023 \begin{itemize}
1024
1025 \item A type may not be declared as an instance of a
1026 particular class more than once in the program.
1027
1028 \item The class and type must have the same kind; 
1029 this can be determined using kind inference as described
1030 in Section~\ref{kindinference}\index{kind}\index{kind inference}.
1031
1032 \item 
1033 Assume that the type variables in the instance type "(T u_1 ... u_k)"
1034 satisfy the constraints in the instance context "cx'".  Under this
1035 assumption, the following two conditions must also be satisfied:
1036 \begin{enumerate}
1037 \item
1038 The constraints expressed by the superclass context "cx[(T u1 ... uk)/u]"
1039         of "C" must be satisfied.  In other words, "T" must be an instance
1040         of each of "C"'s superclasses and the contexts of all
1041         superclass instances must be implied by "cx'".
1042 \item
1043 Any constraints on the type variables in the instance type
1044       that are required for the class method declarations in "d" to be
1045       well-typed must also be satisfied.
1046 \end{enumerate}
1047
1048 % "T" must be an instance of each of "C"'s superclasses.  More precisely,
1049 % under the assumption that the constraints expressed by the
1050 % instance context "cx'" are satisfied, the constraints expressed by the
1051 % superclass context "cx[(T u1 ... uk)/u]" must also be satisfied.
1052
1053 % Furthermore, under the same assumption, any constraints arising from the
1054 % class method declarations in "d" must also be satisfied.  
1055
1056 In fact, except in pathological cases 
1057 it is possible to infer from the instance declaration the
1058 most general instance context "cx'" satisfying the above two constraints, 
1059 but it is nevertheless mandatory
1060 to write an explicit instance context.
1061 \end{itemize}
1062 The following example illustrates the restrictions imposed by superclass instances:
1063 \bprog
1064 @
1065   class Foo a => Bar a where ...
1066   
1067   instance (Eq a, Show a) => Foo [a] where ...
1068   
1069   instance Num a => Bar [a] where ...
1070 @
1071 \eprog
1072 This example is valid Haskell.  Since @Foo@ is a superclass of @Bar@,
1073 the second instance declaration is only valid if @[a]@ is an
1074 instance of @Foo@ under the assumption @Num a@.  
1075 The first instance declaration does indeed say that @[a]@ is an instance
1076 of @Foo@ under this assumption, because @Eq@ and @Show@ are superclasses
1077 of @Num@.
1078
1079 If the two instance declarations instead read like this:
1080 \bprog
1081 @
1082   instance Num a => Foo [a] where ...
1083   
1084   instance (Eq a, Show a) => Bar [a] where ...
1085 @
1086 \eprog
1087 then the program would be invalid.  The second instance declaration is
1088 valid only if @[a]@ is an instance of @Foo@ under the assumptions
1089 @(Eq a, Show a)@.  But this does not hold, since @[a]@ is only an
1090 instance of @Foo@ under the stronger assumption @Num a@.
1091
1092 Further examples of 
1093 @instance@ declarations may be found in Chapter~\ref{stdprelude}.
1094
1095 \subsubsection{Derived Instances}
1096 \index{derived instance}
1097 \label{derived-decls}
1098
1099 As mentioned in Section~\ref{datatype-decls}, @data@ and @newtype@
1100 declarations 
1101 contain an optional @deriving@ form.  If the form is included, then
1102 {\em derived instance declarations} are automatically generated for
1103 the datatype in each of the named classes.
1104 These instances are subject to the same restrictions as user-defined
1105 instances.  When deriving a class "C" for a type "T", instances for
1106 all superclasses of "C" must exist for "T", either via an explicit
1107 @instance@ declaration or by including the superclass in the
1108 @deriving@ clause.
1109
1110 Derived instances provide convenient commonly-used operations for
1111 user-de\-fined da\-ta\-types.  For example, derived instances for datatypes
1112 in the class @Eq@ define the operations @==@ and @/=@, freeing the
1113 programmer from the need to define them.
1114 %and taking advantage of
1115 %\Haskell{}'s class mechanism to overload these operations.
1116
1117 The only classes in the Prelude for
1118 which derived instances are allowed are
1119 @Eq@\indexdi{Eq},
1120 @Ord@\indexdi{Ord},
1121 @Enum@\indexdi{Enum},
1122 @Bounded@\indexdi{Bounded},
1123 @Show@\indexdi{Show},
1124 and @Read@\indexdi{Read},
1125 all mentioned in Figure~\ref{standard-classes}, page~\pageref{standard-classes}.
1126 The
1127 precise details of how the derived instances are generated for each of
1128 these classes are provided in Chapter~\ref{derived-appendix}, including
1129 a specification of when such derived instances are possible. 
1130 %(which is important for the following discussion).
1131 Classes defined by the standard libraries may also be derivable.
1132
1133 A static error results if it is not possible to derive an @instance@
1134 declaration over a class named in a @deriving@ form.  For example,
1135 not all datatypes can properly support class methods in
1136 @Enum@.\indexclass{Enum}  It is 
1137 also a static error to give an explicit @instance@ declaration for
1138 a class that is also derived.
1139 %These rules also apply to the superclasses
1140 %of the class in question.
1141
1142 If the @deriving@ form is omitted from a @data@ or @newtype@
1143 declaration, then {\em no} instance declarations
1144 are derived for 
1145 that datatype; that is, omitting a @deriving@ form is equivalent to
1146 including an empty deriving form: @deriving ()@.
1147
1148 % OLD:
1149 %On the other hand, if the @deriving@ form is omitted from a @data@
1150 %declaration, then @instance@ declarations are derived for the datatype
1151 %in as many of the six classes mentioned above as is possible (see
1152 %Appendix~\ref{derived-appendix}); that is, no
1153 %static error will result if the @instance@ declarations cannot be generated.
1154
1155 %OLD:
1156 %If {\em no} derived @instance@ declarations for a datatype
1157 %are wanted, then the empty deriving form @deriving ()@ must be given
1158 %in the @data@ declaration for that type.
1159
1160 \subsubsection{Ambiguous Types, and Defaults for Overloaded Numeric Operations}
1161 \label{default-decls}
1162 \index{default declaration@@{\tt default} declaration}
1163 \index{overloading!defaults}
1164
1165 @@@
1166 topdecl -> @default@ @(@type_1 @,@ ... @,@ type_n@)@ & (n>=0)
1167 @@@
1168 \index{topdecl@@{\em topdecl} (@default@)}
1169
1170 \noindent
1171 A problem inherent with \Haskell{}-style overloading is the
1172 possibility of an {\em ambiguous type}.
1173 \index{ambiguous type}
1174 For example, using the
1175 @read@ and @show@ functions defined in Chapter~\ref{derived-appendix},
1176 and supposing that just @Int@ and @Bool@ are members of @Read@ and
1177 @Show@, then the expression
1178 \bprog
1179 @
1180   let x = read "..." in show x  -- invalid
1181 @
1182 \eprog
1183 is ambiguous, because the types for @show@ and @read@,
1184 \[\ba{ll}
1185 @show@ & ":: \forall a.~@Show@~ a \Rightarrow a \rightarrow  @String@" \\
1186 @read@ & ":: \forall a.~@Read@~ a \Rightarrow @String@ \rightarrow a"
1187 \ea\]
1188 could be satisfied by instantiating @a@ as either @Int@
1189 in both cases, or @Bool@.  Such expressions
1190 are considered ill-typed, a static error.
1191
1192 We say that an expression @e@ has an {\em ambiguous type}
1193 if, in its type "\forall \overline{u}.~cx \Rightarrow t", 
1194 there is a type variable "u" in "\overline{u}" that occurs in "cx" 
1195 but not in "t".  Such types are invalid.
1196
1197 For example, the earlier expression involving @show@ and @read@ has
1198 an ambiguous type since its type is 
1199 "\forall a.~ @Show@~ a, @Read@~ a \Rightarrow @String@".
1200
1201 Ambiguous types can only be circumvented by
1202 input from the user.  One way is through the use of {\em expression
1203 type-signatures}
1204 \index{expression type-signature}
1205 as described in Section~\ref{expression-type-sigs}.
1206 For example, for the ambiguous expression given earlier, one could
1207 write:
1208 \bprog
1209 @
1210   let x = read "..." in show (x::Bool)
1211 @
1212 \eprog
1213 which disambiguates the type.
1214
1215 Occasionally, an otherwise ambiguous expression needs to be made
1216 the same type as some variable, rather than being given a fixed
1217 type with an expression type-signature.  This is the purpose
1218 of the function @asTypeOf@ (Chapter~\ref{stdprelude}):
1219 "x" @`asTypeOf`@ "y" has the value of "x", but "x" and "y" are
1220 forced to have the same type.  For example,
1221 \bprog
1222 @
1223   approxSqrt x = encodeFloat 1 (exponent x `div` 2) `asTypeOf` x
1224 @
1225 \eprog
1226 (See Section~\ref{coercion} for a description of @encodeFloat@ and @exponent@.)
1227
1228 Ambiguities in the class @Num@\indexclass{Num}
1229 are most common, so \Haskell{}
1230 provides another way to resolve them---with a {\em
1231 default declaration}:
1232 \[
1233 "@default (@t_1 @,@ ... @,@ t_n@)@"
1234 \]
1235 where "n\geq0", and each
1236 "t_i" must be a type for which "@Num @t_i" holds.
1237 In situations where an ambiguous type is discovered, an ambiguous type variable, "v", 
1238 is defaultable if:
1239 \begin{itemize}
1240 \item "v" appears only in constraints of the form "C v", where "C" is a class, and
1241 \item at least one of these classes is a numeric class,
1242         (that is, @Num@ or a subclass of @Num@), and 
1243 \item all of these classes are defined in the Prelude or a standard library
1244 (Figures~\ref{basic-numeric-1}--\ref{basic-numeric-2},
1245 pages~\pageref{basic-numeric-1}--\pageref{basic-numeric-2}
1246 show the numeric classes, and
1247 Figure~\ref{standard-classes}, page~\pageref{standard-classes},
1248 shows the classes defined in the Prelude.)
1249 \end{itemize}
1250 Each defaultable variable is replaced by the first type in the
1251 default list that is an instance of all the ambiguous variable's classes.
1252 It is a static error if no such type is found.
1253
1254 Only one default declaration is permitted per module, and its effect
1255 is limited to that module.  If no default declaration is given in a
1256 module then it assumed to be:
1257 \bprog
1258 @
1259   default (Integer, Double)
1260 @
1261 \eprog
1262 The empty default declaration, @default ()@, turns off all defaults in a module.
1263
1264 \subsection{Nested Declarations}
1265 \label{nested}
1266
1267 The following declarations may be used in any declaration list,
1268 including the top level of a module.
1269
1270 \subsubsection{Type Signatures}
1271 \index{type signature}
1272 \label{type-signatures}
1273
1274 @@@
1275 gendecl -> vars @::@ [context @=>@] type
1276 vars    -> var_1 @,@ ...@,@ var_n               & (n>=1)
1277 @@@
1278 \indexsyn{signdecl}%
1279 \indexsyn{vars}%
1280 A type signature specifies types for variables, possibly with respect
1281 to a context.  A type signature has the form:
1282 \[
1283 "v_1, ..., v_n @::@ cx @=>@ t"
1284 \]
1285 which is equivalent to asserting
1286 "v_i @::@ cx @=>@ t"
1287 for each "i" from "1" to "n".  Each "v_i" must have a value binding in
1288 the same declaration list that contains the type signature; i.e.~it is
1289 invalid to give a type signature for a variable bound in an
1290 outer scope.
1291 Moreover, it is invalid to give more than one type signature for one
1292 variable, even if the signatures are identical.
1293
1294 As mentioned in Section~\ref{type-syntax},
1295 every type variable appearing in a signature
1296 is universally quantified over that signature, and hence
1297 the scope of a type variable is limited to the type
1298 signature that contains it.  For example, in the following
1299 declarations
1300 \bprog
1301 @
1302   f :: a -> a
1303   f x = x :: a                  -- invalid
1304 @
1305 \eprog
1306 the @a@'s in the two type signatures are quite distinct.  Indeed,
1307 these declarations contain a static error, since @x@ does not have
1308 type "\forall a.~a".  (The type of @x@ is dependent on the type of
1309 @f@; there is currently no way in \Haskell{} to specify a signature
1310 for a variable with a dependent type; this is explained in Section
1311 \ref{monomorphism}.)
1312
1313 If a given program includes a signature
1314 for a variable "f", then each use of "f" is treated as having the
1315 declared type.  It is a static error if the same type cannot also be
1316 inferred for the defining occurrence of "f".
1317
1318 If a variable "f" is defined without providing a corresponding type
1319 signature declaration, then each use of "f" outside its own declaration
1320 group (see Section~\ref{dependencyanalysis}) is treated as having the
1321 corresponding inferred, or {\em principal} type \index{principal type}.
1322 However, to ensure that type inference is still possible, the defining
1323 occurrence, and all uses of "f" within its declaration group must have
1324 the same monomorphic type (from which the principal type is obtained
1325 by generalization, as described in Section~\ref{generalization}).
1326
1327 %%A type signature for "x" may be more specific than the principal
1328 %%type derivable from the value binding of "x" (see
1329 %%Section~\ref{type-semantics}), but it is an error to give a type
1330 %%that is more
1331 %%general than, or incomparable to, the principal type.
1332 %%\index{principal type}
1333 %%If a more specific type is given then all occurrences of the
1334 %%variable must be used at the more specific type or at a more
1335 %%specific type still.
1336 %
1337 For example, if we define\nopagebreak[4]
1338 \bprog
1339 @
1340   sqr x  =  x*x
1341 @
1342 \eprog
1343 then the principal type is 
1344 "@sqr@ :: \forall a.~ @Num@~ a \Rightarrow a \rightarrow a", 
1345 which allows
1346 applications such as @sqr 5@ or @sqr 0.1@.  It is also valid to declare
1347 a more specific type, such as
1348 \bprog
1349 @
1350   sqr :: Int -> Int
1351 @
1352 \eprog
1353 but now applications such as @sqr 0.1@ are invalid.  Type signatures such as
1354 \bprog
1355 @
1356   sqr :: (Num a, Num b) => a -> b     -- invalid
1357   sqr :: a -> a                       -- invalid
1358 @
1359 \eprog
1360 are invalid, as they are more general than the principal type of @sqr@.
1361
1362 Type signatures can also be used to support
1363 {\em polymorphic recursion}\index{polymorphic recursion}.
1364 The following definition is pathological, but illustrates how a type
1365 signature can be used to specify a type more general than the one that
1366 would be inferred:
1367 \bprog
1368 @
1369   data T a  =  K (T Int) (T a)
1370   f         :: T a -> a
1371   f (K x y) =  if f x == 1 then f y else undefined
1372 @
1373 \eprog
1374 If we remove the signature declaration, the type of @f@ will be
1375 inferred as @T Int -> Int@ due to the first recursive call for which
1376 the argument to @f@ is @T Int@.  Polymorphic recursion allows the user
1377 to supply the more general type signature, @T a -> a@.
1378
1379 \subsubsection{Fixity Declarations}
1380 \index{fixity declaration}
1381 \label{fixity}
1382
1383 @@@
1384 gendecl -> fixity [integer] ops
1385 fixity  -> @infixl@ | @infixr@ | @infix@
1386 ops     -> op_1 @,@ ... @,@ op_n                &  (n>=1)
1387 op      -> varop | conop 
1388 @@@
1389 \indexsyn{gendecl}%
1390 \indexsyn{fixity}%
1391 \indexsyn{ops}%
1392 \indexsyn{op}%
1393 %\indextt{infixl}\indextt{infixr}\indextt{infix}
1394 A fixity declaration gives the fixity and binding
1395 precedence of one or more operators.  The "integer" in a fixity declaration
1396 must be in the range "0" to "9".
1397 A fixity declaration may appear anywhere that 
1398 a type signature appears and, like a type signature, declares a property of
1399 a particular operator.  Also like a type signature,
1400 a fixity declaration can only occur in the same sequence of declarations as
1401 the declaration of the operator itself, and at most one fixity declaration
1402 may be given for any operator.  (Class methods are a minor exception;
1403 their fixity declarations can occur either in the class declaration itself
1404 or at top level.)
1405
1406 There are three kinds of fixity, non-, left- and right-associativity
1407 (@infix@, @infixl@, and @infixr@, respectively), and ten precedence
1408 levels, 0 to 9 inclusive (level 0 binds least tightly, and level 9
1409 binds most tightly).  If the "digit" is omitted, level 9 is assumed.
1410 Any operator lacking a fixity declaration
1411 is assumed to be @infixl 9@ (See Section~\ref{expressions} for more on
1412 the use of fixities).
1413 Table~\ref{prelude-fixities} lists the fixities and precedences of
1414 the operators defined in the Prelude.
1415
1416 \begin{table}[htb]
1417 \[
1418 \centerline{
1419 \bto{|r||l|l|l|}
1420 \hline 
1421 Prec-  & Left associative       & Non-associative       & Right associative \\
1422 edence & operators              & operators             & operators \\ \hline\hline
1423 %9  & @!@, @!!@, @//@   &                               & @.@             \\ \hline
1424 9  & @!!@               &                               & @.@             \\ \hline
1425 8  &                    &                               & @^@, @^^@, @**@ \\ \hline
1426 7  & @*@, @/@, @`div`@,                 &               &  \\
1427    & @`mod`@, @`rem`@, @`quot`@         &               &  \\ \hline
1428 6  & @+@, @-@           &                               &                 \\ \hline
1429 5  &                    &                               & @:@, @++@       \\ \hline
1430 4  &                    & @==@, @/=@, @<@, @<=@, @>@, @>=@, &             \\
1431    &                    & @`elem`@, @`notElem`@         &                 \\ \hline
1432 3  &                    &                               & @&&@            \\ \hline
1433 2  &                    &                               & @||@            \\ \hline
1434 1  &    @>>@, @>>=@     &                               &               \\ \hline
1435 0  &                    &                               & @$@, @$!@, @`seq`@    \\ \hline
1436 \eto}
1437 \]
1438 %**<div align=center> <h4>Table 2</h4> </div>
1439 \ecaption{Precedences and fixities of prelude operators}
1440 % Removed (:%) -- infixl 7, on the grounds that it's not exported from 
1441 % PreludeRatio!
1442 \label{prelude-fixities}
1443 \index{""!""!@@{\tt  {\char'041}{\char'041}}}
1444 \indextt{.}
1445 \indextt{**}
1446 \index{^@@{\tt  {\char'136}}} % this is ^
1447 \index{^^@@{\tt  {\char'136}{\char'136}}} % this is ^^
1448 \indextt{*}
1449 \indextt{/}
1450 \indextt{div}
1451 \indextt{mod}
1452 \indextt{rem}
1453 \indextt{+}
1454 \indextt{-}
1455 \indextt{:}
1456 \indextt{++}
1457 \indextt{/=}
1458 \indextt{<}
1459 \indextt{<=}
1460 \indextt{==}
1461 \indextt{>}
1462 \indextt{>=}
1463 \indextt{elem}
1464 \indextt{notElem}
1465 \index{&&@@{\tt  \&\&}}
1466 \index{""|""|@@{\tt  {\char'174}{\char'174}}}
1467 \indextt{>>}
1468 \indextt{>>=}
1469 \index{$@@{\tt  {\char'044}}}
1470 \end{table}
1471
1472 % Old table
1473 % \begin{tabular}{|c|l|l|}\hline
1474 % Precedence & Fixity & Operators \\ \hline
1475 % 9 & @infixl@ & @!@, @!!@, @//@ \\
1476 %   & @infixr@ & @.@ \\
1477 % 8 & @infixr@ & @**@, @^@, @^^@ \\
1478 % 7 & @infixl@ & @%@, @*@ \\
1479 %   & @infix@  & @/@, @`div`@, @`mod`@, @`rem`@ \\
1480 % 6 & @infixl@ & @+@, @-@ \\
1481 %   & @infix@  & @:+@ \\
1482 % 5 & @infixr@ & @:@, @++@ \\
1483 %   & @infix@  & @\\@ \\
1484 % 4 & @infix@  & @/=@, @<@, @<=@, @==@, @>@, @>=@, @`elem`@, @`notElem`@ \\
1485 % 3 & @infixr@ & @&&@ \\
1486 % 2 & @infixr@ & @||@ \\
1487 % 1 & @infixr@  & @>>@, @>>=@ \\
1488 % 0 & @infixr@ & @$@ \\ \hline
1489 % \end{tabular}}
1490
1491 Fixity is a property of a particular entity (constructor or variable), just like
1492 its type; fixity is not a property of that entity's {\em name}.
1493 For example: 
1494 \bprog
1495 @
1496   module Bar( op ) where
1497     infixr 7 `op`
1498     op = ...
1499   
1500   module Foo where
1501     import qualified Bar
1502     infix 3 `op`
1503   
1504     a `op` b = (a `Bar.op` b) + 1
1505   
1506     f x = let
1507              p `op` q = (p `Foo.op` q) * 2
1508           in ...
1509 @
1510 \eprog
1511 Here, @`Bar.op`@ is @infixr 7@, @`Foo.op`@ is @infix 3@, and
1512 the nested definition of @op@ in @f@'s right-hand side has the
1513 default fixity of @infixl 9@.  (It would also be possible
1514 to give a fixity to the nested definition of @`op`@ with a nested
1515 fixity declaration.)
1516
1517
1518
1519 \subsubsection{Function and Pattern Bindings}
1520  \label{function-bindings}\label{pattern-bindings}
1521 \index{function binding}\index{pattern binding}
1522
1523 @@@
1524 decl    ->  (funlhs | pat^0) rhs
1525
1526 funlhs  ->  var apat \{ apat \}
1527         |   pat^{i+1} varop^{(a,i)} pat^{i+1}
1528         |   lpat^i varop^{({\rm{}l},i)} pat^{i+1}
1529         |   pat^{i+1} varop^{({\rm{}r},i)} rpat^i
1530         |   @(@ funlhs @)@  apat \{ apat \}
1531
1532 rhs     ->  @=@ exp [@where@ decls]
1533         |   gdrhs [@where@ decls]
1534
1535 gdrhs   ->  gd @=@ exp [gdrhs]
1536
1537 gd      ->  @|@ exp^0 
1538 @@@
1539 \indexsyn{decl}%
1540 \indexsyn{rhs}%
1541 \indexsyn{gdrhs}%
1542 \indexsyn{gd}%
1543 We distinguish two cases within this syntax: a {\em pattern binding}
1544 occurs when the left hand side is a "pat^0"; 
1545 otherwise, the binding is called a {\em function
1546 binding}.  Either binding may appear at the top-level of a module or
1547 within a @where@ or @let@ construct.  
1548
1549 \subsubsubsection{Function bindings.}
1550 \index{function binding}
1551 A function binding binds a variable to a function value.  The general
1552 form of a function binding for variable "x" is:
1553 \[\ba{lll}
1554 "x" & "p_{11} ... p_{1k}" & "match_1"\\
1555 "..." \\
1556 "x" & "p_{n1} ... p_{nk}" & "match_n"
1557 \ea\]
1558 where each "p_{ij}" is a pattern, and where each "match_i" is of the
1559 general form:
1560 \[\ba{l}
1561 "@=@ e_i @where {@ decls_i @}@"
1562 \ea\]
1563 or
1564 \[\ba{lll}
1565 "@|@ g_{i1}"   & "@=@ e_{i1} " \\
1566 "..." \\
1567 "@|@ g_{im_i}" & "@=@ e_{im_i}" \\
1568                & \multicolumn{2}{l}{"@where {@ decls_i @}@"}
1569 \ea\]
1570 and where "n>=1", "1<=i<=n", "m_i>=1".  The former is treated
1571 as shorthand for a particular case of the latter, namely:
1572 \[\ba{l}
1573 "@| True =@ e_i @where {@ decls_i @}@"
1574 \ea\]
1575
1576 Note that all clauses defining a function must be contiguous, and the
1577 number of patterns in each clause must be the same.  The set of
1578 patterns corresponding to each match must be {\em
1579 linear}\index{linearity}\index{linear pattern}---no variable is
1580 allowed to appear more than once in the entire set.
1581
1582 Alternative syntax is provided for binding functional values to infix
1583 operators.  For example, these three function
1584 definitions are all equivalent:
1585 \bprog
1586 @
1587   plus x y z = x+y+z
1588   x @\bkqB@plus@\bkqA@ y = \ z -> x+y+z
1589   (x @\bkqB@plus@\bkqA@ y) z = x+y+z
1590 @
1591 \eprogNoSkip
1592
1593 \outline{
1594 \paragraph*{Translation:}
1595 The general binding form for functions is semantically
1596 equivalent to the equation (i.e.~simple pattern binding):
1597 \[
1598 "x @= \@ x_1 ... x_k @-> case (@x_1@, @...@, @x_k@) of@"
1599 \ba[t]{lcl}
1600 "@(@p_{11}, ..., p_{1k}@)@ match_1"  \\
1601 "..." \\
1602 "@(@p_{n1}, ..., p_{nk}@)@ match_n"
1603 \ea\]
1604 where the "x_i" are new identifiers.
1605 }
1606
1607 \subsubsubsection{Pattern bindings.}
1608 \label{patbind}
1609 \index{pattern binding}
1610
1611 A pattern binding binds variables to values.  A {\em simple} pattern
1612 binding has form "p = e".
1613 \index{simple pattern binding}
1614 The pattern "p" is
1615 matched ``lazily'' as an irrefutable pattern\index{irrefutable
1616 pattern}, as if there were an implicit @~@ in front 
1617 of it.  See the translation in
1618 Section~\ref{let-expressions}.
1619
1620 The {\em general} form of a pattern binding is "p match", where a
1621 "match" is the same structure as for function bindings above; in other
1622 words, a pattern binding is:
1623 \[\ba{rcl}
1624 "p" & "@|@ g_{1}"   & "@=@ e_{1}" \\
1625     & "@|@ g_{2}"   & "@=@ e_{2}" \\
1626     & "..." \\
1627     & "@|@ g_{m}"   & "@=@ e_{m}" \\
1628     & \multicolumn{2}{l}{"@where {@ decls @}@"}
1629 \ea\]
1630
1631 %{\em Note}: the simple form
1632 %\WeSay{Yes}
1633 %"p @=@ e" is equivalent to "p @| True =@ e".
1634
1635 \outline{
1636 \paragraph*{Translation:}
1637 The pattern binding above is semantically equivalent to this
1638 simple pattern binding:
1639 \[\ba{lcl}
1640 "p" &@=@& "@let@ decls @in@" \\
1641     &   & "@if @g_1@ then @e_1@ else@" \\
1642     &   & "@if @g_2@ then @e_2@ else@" \\
1643     &   & ...                          \\
1644     &   & "@if @g_m@ then @e_m@ else error "Unmatched pattern"@"
1645 \ea\]
1646 }
1647
1648 \paragraph*{A note about syntax.}  It is usually straightforward
1649 to tell whether a binding is a pattern binding or a function binding,
1650 but the existence of @n+k@ patterns\index{n+k pattern@@"n@+@k" pattern}
1651 sometimes confuses the issue.
1652 Here are four examples:
1653 \bprog
1654 @
1655   x + 1 = ...           -- Function binding, defines (+)
1656                         -- Equivalent to   (+) x 1 = ...
1657
1658   (x + 1) = ...         -- Pattern binding, defines x
1659
1660   (x + 1) * y = ...     -- Function binding, defines (*)
1661                         -- Equivalent to   (*) (x+1) y = ...
1662
1663   (x + 1) y = ...       -- Function binding, defines (+)
1664                         -- Equivalent to   (+) x 1 y = ...
1665 @
1666 \eprog
1667 The first two can be distinguished because a pattern binding
1668 has a "pat^0" on the left hand side, not a "pat"  --- the former cannot
1669 be an unparenthesised @n+k@ pattern.
1670
1671 \subsection{Static Semantics of Function and Pattern Bindings}
1672 \label{dependencyanalysis}
1673
1674 The static semantics of the function and pattern bindings of
1675 a @let@ expression or @where@ clause
1676 % (including that of the top-level of
1677 % a program that has been translated into a @let@ expression as
1678 % described at the beginning of Section~\ref{modules})
1679 are discussed in this section.
1680
1681 \subsubsection{Dependency Analysis}
1682 \label{depend-anal}
1683
1684 In general the static semantics are given by the
1685 normal Hindley-Milner\index{Hindley-Milner type system} inference rules.
1686 A {\em dependency
1687 analysis\index{dependency analysis} transformation} is first performed
1688 to increase polymorphism.
1689 Two variables bound by value declarations are in the
1690 same {\em declaration group} if either
1691 \index{declaration group}
1692 \begin{enumerate}
1693 \item
1694 they are bound by the same pattern binding, or
1695 \item
1696 their bindings are mutually recursive (perhaps via some
1697 other declarations that are also part of the group).
1698 \end{enumerate}
1699 Application of the following 
1700 rules causes each @let@ or @where@ construct (including the @where@
1701 defining the top level bindings in a module) to bind only the
1702 variables of a single declaration group, thus capturing the required
1703 dependency analysis:\footnote{%
1704 A similar transformation is described in 
1705 Peyton Jones' book \cite{peyton-jones:book}.}
1706 \begin{enumerate}
1707 \item The order of declarations in @where@/@let@ constructs is irrelevant.
1708 \item @let {@"d_1"@; @"d_2"@} in @"e" = @let {@"d_1"@} in (let {@"d_2"@} in @"e"@)@ \\
1709 \ \ \ \ (when no identifier bound in "d_2" appears free in "d_1")
1710 \end{enumerate}
1711
1712 %----------------
1713
1714 \subsubsection{Generalization}
1715 \label{generalization}
1716
1717 The Hindley-Milner type system assigns types to a @let@-expression
1718 in two stages.
1719 First, the right-hand side of the declaration is typed, giving a type with
1720 no universal quantification.  Second, all type variables that occur in this
1721 type are universally quantified unless they are associated with
1722 bound variables in the type environment;
1723 this is called {\em generalization}.\index{generalization}
1724 Finally, the body of the @let@-expression is typed.
1725
1726 For example, consider the declaration
1727 \bprog
1728 @
1729   f x = let g y = (y,y)
1730         in ...
1731
1732 @
1733 \eprog
1734 The type of @g@'s definition is 
1735 "a \rightarrow (a,a)".  The generalization step
1736 attributes to @g@ the polymorphic type 
1737 "\forall a.~ a \rightarrow (a,a)",
1738 after which the typing of the ``@...@'' part can proceed.
1739
1740 When typing overloaded definitions, all the overloading 
1741 constraints from a single declaration group are collected together, 
1742 to form the context for the type of each variable declared in the group.
1743 For example, in the definition:
1744 \bprog
1745 @
1746   f x = let g1 x y = if x>y then show x else g2 y x
1747             g2 p q = g1 q p
1748         in ...
1749 @
1750 \eprog
1751 The types of the definitions of @g1@ and @g2@ are both
1752 "a \rightarrow a \rightarrow @String@", and the accumulated constraints are
1753 "@Ord@~a" (arising from the use of @>@), and "@Show@~a" (arising from the
1754 use of @show@).
1755 The type variables appearing in this collection of constraints are
1756 called the {\em constrained type variables}.
1757
1758 The generalization step attributes to both @g1@ and @g2@ the type
1759 \[
1760 "\forall a.~(@Ord@~a,~@Show@~a) \Rightarrow a \rightarrow a \rightarrow @String@"
1761 \]
1762 Notice that @g2@ is overloaded in the same way as @g1@ even though the
1763 occurrences of @>@ and @show@ are in the definition of @g1@.
1764
1765 If the programmer supplies explicit type signatures for more than one variable
1766 in a declaration group, the contexts of these signatures must be 
1767 identical up to renaming of the type variables.
1768
1769 \subsubsection{Context Reduction Errors}
1770 \label{context-reduction}
1771 \index{context reduction}
1772 As mentioned in Section~\ref{type-semantics}, the context of a type
1773 may constrain only a type variable, or the application of a type variable
1774 to one or more types.  Hence, types produced by
1775 generalization must be expressed in a form in which all context
1776 constraints have be reduced to this ``head normal form''.
1777 Consider, for example, the
1778 definition:
1779 \bprog
1780 @
1781   f xs y  =  xs == [y]
1782 @
1783 \eprog
1784 Its type is given by
1785 \bprog
1786 @
1787   f :: Eq a => [a] -> a -> Bool
1788 @
1789 \eprog
1790 and not
1791 \bprog
1792 @
1793   f :: Eq [a] => [a] -> a -> Bool
1794 @
1795 \eprog
1796 Even though the equality is taken at the list type, the context must
1797 be simplified, using the instance declaration for @Eq@ on lists,
1798 before generalization.  If no such instance is in scope, a static
1799 error occurs.
1800
1801 Here is an example that shows the need for a
1802 constraint of the form "C (m t)" where m is one of the type
1803 variables being generalized; that is, where the class "C" applies to a type
1804 expression that is not a type variable or a type constructor.
1805 Consider:
1806 \bprog
1807 @
1808   f :: (Monad m, Eq (m a)) => a -> m a -> Bool
1809   f x y = return x == y
1810 @
1811 \eprog
1812 The type of @return@ is @Monad m => a -> m a@; the type of @(==)@ is
1813 @Eq a => a -> a -> Bool@.  The type of @f@ should be
1814 therefore @(Monad m, Eq (m a)) => a -> m a -> Bool@, and the context
1815 cannot be simplified further.
1816
1817 The instance declaration derived from a data type @deriving@ clause
1818 (see Section~\ref{derived-decls})
1819 must, like any instance declaration, have a {\em simple} context; that is,
1820 all the constraints must be of the form "C a", where "a" is a type variable.
1821 For example, in the type
1822 \bprog
1823 @
1824   data Apply a b = App (a b)  deriving Show
1825 @
1826 \eprog
1827 the derived Show instance will produce a context @Show (a b)@, which
1828 cannot be reduced and is not simple; thus a static error results.
1829
1830 \subsubsection{Monomorphism}
1831 \label{monomorphism}
1832 Sometimes it is not possible to generalize over all the type variables
1833 used in the type of the definition.
1834 For example, consider the declaration\nopagebreak[4]
1835 \bprog
1836 @
1837   f x = let g y z = ([x,y], z)
1838         in ...
1839 @
1840 \eprog
1841 In an environment where @x@ has type "a",
1842 the type of @g@'s definition is 
1843 "a \rightarrow b \rightarrow @([@a@]@,b@)@".
1844 The generalization step attributes to @g@ the type 
1845 "\forall b.~ a \rightarrow b \rightarrow @([@a@]@,b@)@";
1846 only "b" can be universally quantified because "a" occurs in the
1847 type environment.
1848 We say that the type of @g@ is {\em monomorphic in the type variable "a"}.
1849 \index{monomorphic type variable}
1850
1851 The effect of such monomorphism is that the first argument of all 
1852 applications of @g@ must be of a single type.  
1853 For example, it would be valid for
1854 the ``@...@'' to be
1855 \bprog
1856 @
1857   (g True, g False)
1858 @
1859 \eprog
1860 (which would, incidentally, force @x@ to have type @Bool@) but invalid
1861 for it to be 
1862 \bprog
1863 @
1864   (g True, g 'c')
1865 @
1866 \eprog
1867 In general, a type "\forall \overline{u}.~cx \Rightarrow t"
1868 is said to be {\em monomorphic}
1869 \index{monomorphic type variable}
1870 in the type variable "a" if "a" is free in
1871 "\forall \overline{u}.~cx \Rightarrow t".
1872
1873 It is worth noting that the explicit type signatures provided by \Haskell{}
1874 are not powerful enough to express types that include monomorphic type
1875 variables.  For example, we cannot write
1876 \bprog
1877 @
1878   f x = let 
1879           g :: a -> b -> ([a],b)
1880           g y z = ([x,y], z)
1881         in ...
1882 @
1883 \eprog
1884 because that would claim that @g@ was polymorphic in both @a@ and @b@
1885 (Section~\ref{type-signatures}).  In this program, @g@ can only be given
1886 a type signature if its first argument is restricted to a type not involving
1887 type variables; for example
1888 \bprog
1889 @
1890   g :: Int -> b -> ([Int],b)
1891 @
1892 \eprog
1893 This signature would also cause @x@ to have type @Int@.
1894
1895 \subsubsection{The Monomorphism Restriction}
1896 \index{monomorphism restriction}
1897 \label{sect:monomorphism-restriction}
1898
1899 \Haskell{} places certain extra restrictions on the generalization
1900 step, beyond the standard Hindley-Milner restriction described above,
1901 which further reduces polymorphism in particular cases.
1902
1903 The monomorphism restriction depends on the binding syntax of a
1904 variable.  Recall that a variable is bound by either a {\em function
1905 binding} or a {\em pattern binding}, and that a {\em simple} pattern
1906 binding is a pattern binding in which the pattern consists of only a
1907 single variable (Section~\ref{pattern-bindings}).
1908
1909 The following two rules define the monomorphism restriction:
1910 \outline{
1911 \paragraph*{The monomorphism restriction}
1912
1913 \begin{description}
1914 \item[Rule 1.]
1915 We say that a given declaration group is {\em unrestricted} if and only if:
1916 \begin{description}
1917 \item[(a):]
1918 every variable in the group is bound by a function binding or a simple
1919 pattern binding\index{simple pattern binding} (Section~\ref{patbind}), {\em and}
1920 \item[(b):]
1921 an explicit type signature is given for every variable in the group
1922 that is bound by simple pattern binding.
1923 \end{description}
1924 The usual Hindley-Milner restriction on polymorphism is that
1925 only type variables that do not occur free in the environment may be generalized.
1926 In addition, {\em the constrained type variables of
1927 a restricted declaration group may not be generalized}
1928 in the generalization step for that group.
1929 (Recall that a type variable is constrained if it must belong
1930 to some type class; see Section~\ref{generalization}.)
1931
1932 % \item[Rule 1.]
1933 % The variables of a given declaration group are monomorphic in
1934 % all their constrained type variables if and only if:
1935 % \begin{description}
1936 % \item[either (a):]
1937 % one or more variables in the declaration group 
1938 % is bound by a non-simple pattern binding.
1939 % \item[or (b):]
1940 % one or more variables in the declaration group is bound 
1941 % by a simple pattern binding, and
1942 % no type signature is given for any of the variables in the group.
1943 % \end{description}
1944
1945 \item[Rule 2.]
1946 Any monomorphic type variables that remain when type inference for
1947 an entire module is complete, are considered {\em ambiguous}\index{ambiguous type},
1948 and are resolved to particular types using the defaulting 
1949 rules (Section~\ref{default-decls}).
1950 \end{description}
1951 }
1952
1953 % When all variables in a declaration group are declared using function
1954 % binding the monomorphism restriction will not apply.  Any variable
1955 % declared in a non-simple pattern binding will invoke monomorphism for
1956 % the entire group containing it.  Simple pattern bindings will be
1957 % monomorphic unless a type signature is supplied.
1958 %
1959
1960 \paragraph*{Motivation}
1961
1962 Rule 1 is required for two reasons, both of which are fairly subtle.
1963 \begin{itemize}
1964 \item
1965 {\em Rule 1 prevents computations from being unexpectedly repeated.}
1966 For example, @genericLength@ is a standard function (in library @List@) whose
1967 type is given by
1968 \bprog
1969 @
1970   genericLength :: Num a => [b] -> a
1971 @
1972 \eprog
1973 Now consider the following expression:
1974 \bprog
1975 @
1976   let { len = genericLength xs } in (len, len)
1977 @
1978 \eprog
1979 It looks as if @len@ should be computed only once, but without Rule~1 it might
1980 be computed twice, once at each of two different overloadings.  If the 
1981 programmer does actually wish the computation to be repeated, an explicit
1982 type signature may be added:
1983 \bprog
1984 @
1985   let { len :: Num a => a; len = genericLength xs } in (len, len)
1986 @
1987 \eprog
1988
1989 \item {\em Rule~1 prevents ambiguity.}  For example, consider the declaration
1990 group
1991 \bprog
1992 @
1993   [(n,s)] = reads t
1994 @
1995 \eprog
1996 Recall that @reads@ is a standard function whose type is given by the
1997 signature
1998 \bprog
1999 @
2000   reads :: (Read a) => String -> [(a,String)]
2001 @
2002 \eprog
2003 Without Rule~1, @n@ would be assigned the 
2004 type "\forall a.~@Read@~a \Rightarrow a" 
2005 and @s@ the type "\forall a." "@Read@~a" "\Rightarrow @String@".
2006 The latter is an invalid type, because it is inherently ambiguous.
2007 It is not possible to determine at what overloading to use @s@, nor
2008 can this be solved by adding a type signature for @s@.
2009 Hence, when {\em non-simple} pattern bindings\index{simple pattern binding}
2010 are used (Section~\ref{patbind}), the types inferred are 
2011 always monomorphic in their constrained type variables, irrespective of whether
2012 a type signature is provided.
2013 In this case, both @n@ and @s@ are monomorphic in "a".
2014
2015 The same constraint applies to pattern-bound functions.  For example, in
2016 \bprog
2017 @
2018   (f,g) = ((+),(-))
2019 @
2020 \eprog
2021 both @f@ and @g@ are monomorphic regardless of any type
2022 signatures supplied for @f@ or @g@.
2023 \end{itemize}
2024
2025 Rule~2 is required because there is no way to enforce monomorphic use
2026 of an {\em exported} binding, except by performing type inference on modules
2027 outside the current module.  Rule~2 states that the exact types of all
2028 the variables bound in a module must be determined by that module alone, and not
2029 by any modules that import it.
2030 \bprog
2031 @
2032   module M1(len1) where
2033     default( Int, Double )
2034     len1 = genericLength "Hello"
2035
2036   module M2 where
2037     import M1(len1)
2038     len2 = (2*len1) :: Rational
2039 @
2040 \eprog
2041 When type inference on module @M1@ is complete, @len1@ has the 
2042 monomorphic type @Num a => a@ (by Rule 1).  Rule 2 now states that
2043 the monomorphic type variable @a@ is ambiguous, and must be resolved using
2044 the defaulting rules of Section~\ref{default-decls}.
2045 Hence, @len1@ gets type @Int@, and its use in @len2@ is type-incorrect.
2046 (If the above code is actually what is wanted, a type signature on
2047 @len1@ would solve the problem.)
2048
2049 This issue does not arise for nested bindings, because their entire scope is 
2050 visible to the compiler.
2051
2052 \paragraph*{Consequences}
2053
2054 The monomorphism rule has a number of consequences for the programmer.
2055 Anything defined with function syntax usually
2056 generalizes as a function is expected to.  Thus in
2057 \bprog
2058 @
2059   f x y = x+y
2060 @
2061 \eprog
2062 the function @f@ may be used at any overloading in class @Num@.
2063 There is no danger of recomputation here.  However, the same function
2064 defined with pattern syntax:
2065 \bprog
2066 @
2067   f = \x -> \y -> x+y
2068 @
2069 \eprog
2070 requires a type signature if @f@ is to be fully overloaded.
2071 Many functions are most naturally defined using simple pattern
2072 bindings; the user must be careful to affix these with type signatures
2073 to retain full overloading.  The standard prelude contains many
2074 examples of this:
2075 \bprog
2076 @
2077   sum  :: (Num a) => [a] -> a
2078   sum  =  foldl (+) 0  
2079 @
2080 \eprog
2081
2082 Rule~1 applies to both top-level and nested definitions.  Consider
2083 \bprog
2084 @
2085   module M where
2086     len1 = genericLength "Hello"
2087     len2 = (2*len1) :: Rational
2088 @
2089 \eprog
2090 Here, type inference finds that @len1@ has the monomorphic type (@Num a => a@);
2091 and the type variable @a@ is resolved to @Rational@ when performing type
2092 inference on @len2@.
2093
2094 % Even when a function is defined using a function binding, it may still
2095 % be made monomorphic by another variable in the same declaration group.
2096 % Since groups defined through mutually recursive functions need not be
2097 % syntacticly adjacent, it may be difficult to see where overloading is
2098 % being lost.  In this example @fact'@ is defined with a pattern binding
2099 % and forces @fact@ to be monomorphic in the absence of a type signature
2100 % for either @fact@ or @fact'@.  This would in turn result in an error as
2101 % per Rule~2.
2102 % \bprog
2103
2104 % module Mod1(fact)
2105 % import Mod2
2106 % fact 0 = 1
2107 % fact n = n*fact'(n-1)
2108
2109 % module Mod2(fact')
2110 % import Mod1
2111 % fact' = fact
2112
2113 % \eprog
2114
2115 \subsection{Kind Inference}
2116 \index{kind}
2117 \index{kind inference}
2118 \label{kindinference}
2119
2120 This section describes the rules that are used to perform {\em kind
2121 inference}, i.e. to calculate a suitable kind for each type
2122 constructor and class appearing in a given
2123 program.
2124
2125 The first step in the kind inference process is to arrange the set of
2126 datatype, synonym, and class definitions into dependency groups.  This can
2127 be achieved in much the same way as the dependency analysis for value
2128 declarations that was described in Section~\ref{dependencyanalysis}.
2129 For example, the following program fragment includes the definition
2130 of a datatype constructor @D@, a synonym @S@ and a class @C@, all of
2131 which would be included in the same dependency group:
2132 \bprog
2133 @
2134   data C a => D a = Foo (S a)
2135   type S a = [D a]
2136   class C a where
2137       bar :: a -> D a -> Bool
2138 @
2139 \eprog
2140 The kinds of variables, constructors, and classes within each group
2141 are determined using standard techniques of type inference and
2142 kind-preserving unification \cite{jones:cclasses}.  For example, in the
2143 definitions above, the parameter @a@ appears as an argument of the
2144 function constructor @(->)@ in the type of @bar@ and hence must
2145 have kind $\ast$.  It follows that both @D@ and @S@ must have
2146 kind $\ast\rightarrow\ast$ and that every instance of class @C@ must
2147 have kind $\ast$.
2148
2149 % The kind of any constructor that is exported from a module without
2150 % exposing its definition must be specified explicitly in the interface
2151 % for that module.  This is described in Section~\ref{somebodyneedstofillthisin}.
2152
2153 It is possible that some parts of an inferred kind may not be fully
2154 determined by the corresponding definitions; in such cases, a default
2155 of $\ast$ is assumed.  For example, we could assume an arbitrary kind
2156 $\kappa$ for the @a@ parameter in each of the following examples:
2157 \bprog
2158 @
2159   data App f a = A (f a)
2160   data Tree a  = Leaf | Fork (Tree a) (Tree a)
2161 @
2162 \eprog
2163 This would give kinds
2164 $(\kappa\rightarrow\ast)\rightarrow\kappa\rightarrow\ast$ and
2165 $\kappa\rightarrow\ast$ for @App@ and @Tree@, respectively, for any
2166 kind $\kappa$, and would require an extension to allow polymorphic
2167 kinds.  Instead, using the default binding $\kappa=\ast$, the
2168 actual kinds for these two constructors are
2169 $(\ast\rightarrow\ast)\rightarrow\ast\rightarrow\ast$ and
2170 $\ast\rightarrow\ast$, respectively.
2171
2172 Defaults are applied to each dependency group without consideration of
2173 the ways in which particular type constructor constants or classes are
2174 used in later dependency groups or elsewhere in the program.  For example,
2175 adding the following definition to those above does not influence the
2176 kind inferred for @Tree@ (by changing it to
2177 $(\ast\rightarrow\ast)\rightarrow\ast$, for instance), and instead
2178 generates a static error because the kind of @[]@, $\ast\rightarrow\ast$,
2179 does not match the kind $\ast$ that is expected for an argument of @Tree@:
2180 \bprog
2181 @
2182   type FunnyTree = Tree []     -- invalid
2183 @
2184 \eprog
2185 This is important because it ensures that each constructor and class are
2186 used consistently with the same kind whenever they are in scope.
2187
2188 %**~footer
2189
2190 % Local Variables: 
2191 % mode: latex
2192 % End: