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