864133824d029a4b03854f157794ff5d5cef84f0
[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 @
766 \bot @) )@", "@(@ @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 @Ix.range@.
979 \bprog
980 @
981   module A where
982     import qualified Ix
983
984     instance 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 @@@
1539 \indexsyn{decl}%
1540 \indexsyn{pat}%
1541 \indexsyn{rhs}%
1542 \indexsyn{gdrhs}%
1543 \indexsyn{qs}%
1544 We distinguish two cases within this syntax: a {\em pattern binding}
1545 occurs when the left hand side is a \hprime{"pat"}; 
1546 otherwise, the binding is called a {\em function
1547 binding}.  Either binding may appear at the top-level of a module or
1548 within a @where@ or @let@ construct.  
1549
1550 \subsubsubsection{Function bindings}
1551 \index{function binding}
1552 A function binding binds a variable to a function value.  The general
1553 form of a function binding for variable "x" is:
1554 \[\ba{lll}
1555 "x" & "p_{11} ... p_{1k}" & "match_1"\\
1556 "..." \\
1557 "x" & "p_{n1} ... p_{nk}" & "match_n"
1558 \ea\]
1559 where each "p_{ij}" is a pattern, and where each "match_i" is of the
1560 general form:
1561 \[\ba{l}
1562 "@=@ e_i @where {@ decls_i @}@"
1563 \ea\]
1564 or
1565 \[\ba{lll}
1566
1567 "@|@ \hprime{gs_{i1}}"   & "@=@ e_{i1} " \\
1568 "..." \\
1569 "@|@ \hprime{gs_{im_i}}" & "@=@ e_{im_i}" \\
1570                & \multicolumn{2}{l}{"@where {@ decls_i @}@"}
1571 \ea\]
1572 and where "n>=1", "1<=i<=n", "m_i>=1".  The former is treated
1573 as shorthand for a particular case of the latter, namely:
1574 \[\ba{l}
1575 "@| True =@ e_i @where {@ decls_i @}@"
1576 \ea\]
1577
1578 Note that all clauses defining a function must be contiguous, and the
1579 number of patterns in each clause must be the same.  The set of
1580 patterns corresponding to each match must be {\em
1581 linear}\index{linearity}\index{linear pattern}---no variable is
1582 allowed to appear more than once in the entire set.
1583
1584 Alternative syntax is provided for binding functional values to infix
1585 operators.  For example, these three function
1586 definitions are all equivalent:
1587 \bprog
1588 @
1589   plus x y z = x+y+z
1590   x @\bkqB@plus@\bkqA@ y = \ z -> x+y+z
1591   (x @\bkqB@plus@\bkqA@ y) z = x+y+z
1592 @
1593 \eprog
1594
1595 \begin{haskellprime}
1596
1597 Note that fixity resolution applies to the infix variants of the
1598 function binding in the same way as for expressions
1599 (Section~\ref{fixity-resolution}).  Applying fixity resolution to the
1600 left side of the equals in a function binding must leave the "varop"
1601 being defined at the top level.  For example, if we are defining a new
1602 operator @##@ with precedence 6, then this definition would be
1603 illegal:
1604 \bprog
1605 @
1606   a ## b : xs = exp
1607 @
1608 \eprog
1609 because @:@ has precedence 5, so the left hand side resolves to
1610 @(a ## x) : xs@, and this cannot be a pattern binding because @(a ## x)@
1611 is not a valid pattern.
1612
1613 \end{haskellprime}
1614
1615 \outline{
1616 \paragraph*{Translation:}
1617 The general binding form for functions is semantically
1618 equivalent to the equation (i.e.~simple pattern binding):
1619 \[
1620 "x @= \@ x_1 ... x_k @-> case (@x_1@, @...@, @x_k@) of@"
1621 \ba[t]{lcl}
1622 "@(@p_{11}, ..., p_{1k}@)@ match_1"  \\
1623 "..." \\
1624 "@(@p_{n1}, ..., p_{nk}@)@ match_n"
1625 \ea\]
1626 where the "x_i" are new identifiers.
1627 }
1628
1629 \subsubsubsection{Pattern bindings}
1630 \label{patbind}
1631 \index{pattern binding}
1632
1633 A pattern binding binds variables to values.  A {\em simple} pattern
1634 binding has form "p = e".
1635 \index{simple pattern binding}
1636 The pattern "p" is
1637 matched ``lazily'' as an irrefutable pattern\index{irrefutable
1638 pattern}, as if there were an implicit @~@ in front 
1639 of it.  See the translation in
1640 Section~\ref{let-expressions}.
1641
1642 The {\em general} form of a pattern binding is "p match", where a
1643 "match" is the same structure as for function bindings above; in other
1644 words, a pattern binding is:
1645 \[\ba{rcl}
1646 "p" & "@|@ \hprime{gs_{1}}"   & "@=@ e_{1}" \\
1647     & "@|@ \hprime{gs_{2}}"   & "@=@ e_{2}" \\
1648     & "..." \\
1649     & "@|@ \hprime{gs_{m}}"   & "@=@ e_{m}" \\
1650     & \multicolumn{2}{l}{"@where {@ decls @}@"}
1651 \ea\]
1652
1653 %{\em Note}: the simple form
1654 %\WeSay{Yes}
1655 %"p @=@ e" is equivalent to "p @| True =@ e".
1656
1657 \outline{
1658 \paragraph*{Translation:}
1659 The pattern binding above is semantically equivalent to this
1660 simple pattern binding:
1661 \[\ba{lcl}
1662 "p" &@=@& "@let@ decls @in@" \\
1663     &   & \hprime{@case () of @} \\
1664     &   & \hprime{"@  () | @gs_{1}@ -> @e_{1}"} \\
1665     &   & \hprime{"@     | @gs_{2}@ -> @e_{2}"} \\
1666     &   & \hprime{"@       @..."} \\
1667     &   & \hprime{"@     | @gs_{m}@ -> @e_{m}"} \\
1668     &   & \hprime{"@  _ -> error "Unmatched pattern"@"}
1669 \ea\]
1670 }
1671
1672 \subsection{Static Semantics of Function and Pattern Bindings}
1673 \label{dependencyanalysis}
1674
1675 The static semantics of the function and pattern bindings of
1676 a @let@ expression or @where@ clause
1677 % (including that of the top-level of
1678 % a program that has been translated into a @let@ expression as
1679 % described at the beginning of Section~\ref{modules})
1680 are discussed in this section.
1681
1682 \subsubsection{Dependency Analysis}
1683 \label{depend-anal}
1684
1685 In general the static semantics are given by \hprime{applying} the
1686 normal Hindley-Milner\index{Hindley-Milner type system} inference
1687 rules.  \hprime{In order to increase polymorphism, these rules are applied to
1688 groups of bindings identified by a \emph{dependency analysis}.}
1689
1690 \begin{haskellprime}
1691
1692 A binding "b1" \emph{depends} on a binding "b2" in the same list of
1693 declarations if either
1694
1695 \begin{enumerate}
1696 \item "b1" contains a free identifier that has no type signature and
1697 is bound by "b2", or
1698 \item "b1" depends on a binding that depends on "b2".
1699 \end{enumerate}
1700
1701 A \emph{declaration group} is a minimal set of mutually dependent
1702 bindings. Hindley-Milner type inference is applied to each declaration
1703 group in dependency order. The order of declarations in @where@/@let@
1704 constructs is irrelevant.
1705
1706 \end{haskellprime}
1707
1708 % Notes: from http://hackage.haskell.org/trac/haskell-prime/wiki/RelaxedDependencyAnalysis
1709
1710 %     * 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.
1711 %     * defining dependencies between bindings is a little simpler than dependencies between variables.
1712 %     * the dependency analysis transformation formerly listed in this
1713 %     * section is no longer always possible. 
1714
1715 %----------------
1716
1717 \subsubsection{Generalization}
1718 \label{generalization}
1719
1720 \begin{haskellprime}
1721
1722 The Hindley-Milner type system assigns types to a let-expression in two stages:
1723
1724 \begin{enumerate}
1725 \item The declaration groups are considered in dependency order. For
1726 each group, a type with no universal quantification is inferred for
1727 each variable bound in the group. Then, all type variables that occur
1728 in these types are universally quantified unless they are associated
1729 with bound variables in the type environment; this is called
1730 generalization.
1731
1732 \item Finally, the body of the let-expression is typed.
1733 \end{enumerate}
1734
1735 \end{haskellprime}
1736
1737 % Notes: from http://hackage.haskell.org/trac/haskell-prime/wiki/RelaxedDependencyAnalysis
1738
1739 %     * 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.
1740 %     * The original does not deal with functions, non-trivial patterns
1741 %     * or recursion. 
1742
1743 For example, consider the declaration
1744 \bprog
1745 @
1746   f x = let g y = (y,y)
1747         in ...
1748
1749 @
1750 \eprog
1751 The type of @g@'s definition is 
1752 "a \rightarrow (a,a)".  The generalization step
1753 attributes to @g@ the polymorphic type 
1754 "\forall a.~ a \rightarrow (a,a)",
1755 after which the typing of the ``@...@'' part can proceed.
1756
1757 When typing overloaded definitions, all the overloading 
1758 constraints from a single declaration group are collected together, 
1759 to form the context for the type of each variable declared in the group.
1760 For example, in the definition:
1761 \bprog
1762 @
1763   f x = let g1 x y = if x>y then show x else g2 y x
1764             g2 p q = g1 q p
1765         in ...
1766 @
1767 \eprog
1768 The types of the definitions of @g1@ and @g2@ are both
1769 "a \rightarrow a \rightarrow @String@", and the accumulated constraints are
1770 "@Ord@~a" (arising from the use of @>@), and "@Show@~a" (arising from the
1771 use of @show@).
1772 The type variables appearing in this collection of constraints are
1773 called the {\em constrained type variables}.
1774
1775 The generalization step attributes to both @g1@ and @g2@ the type
1776 \[
1777 "\forall a.~(@Ord@~a,~@Show@~a) \Rightarrow a \rightarrow a \rightarrow @String@"
1778 \]
1779 Notice that @g2@ is overloaded in the same way as @g1@ even though the
1780 occurrences of @>@ and @show@ are in the definition of @g1@.
1781
1782 If the programmer supplies explicit type signatures for more than one variable
1783 in a declaration group, the contexts of these signatures must be 
1784 identical up to renaming of the type variables.
1785
1786 \subsubsection{Context Reduction Errors}
1787 \label{context-reduction}
1788 \index{context reduction}
1789 As mentioned in Section~\ref{type-semantics}, the context of a type
1790 may constrain only a type variable, or the application of a type variable
1791 to one or more types.  Hence, types produced by
1792 generalization must be expressed in a form in which all context
1793 constraints have be reduced to this ``head normal form''.
1794 Consider, for example, the
1795 definition:
1796 \bprog
1797 @
1798   f xs y  =  xs == [y]
1799 @
1800 \eprog
1801 Its type is given by
1802 \bprog
1803 @
1804   f :: Eq a => [a] -> a -> Bool
1805 @
1806 \eprog
1807 and not
1808 \bprog
1809 @
1810   f :: Eq [a] => [a] -> a -> Bool
1811 @
1812 \eprog
1813 Even though the equality is taken at the list type, the context must
1814 be simplified, using the instance declaration for @Eq@ on lists,
1815 before generalization.  If no such instance is in scope, a static
1816 error occurs.
1817
1818 Here is an example that shows the need for a
1819 constraint of the form "C (m t)" where m is one of the type
1820 variables being generalized; that is, where the class "C" applies to a type
1821 expression that is not a type variable or a type constructor.
1822 Consider:
1823 \bprog
1824 @
1825   f :: (Monad m, Eq (m a)) => a -> m a -> Bool
1826   f x y = return x == y
1827 @
1828 \eprog
1829 The type of @return@ is @Monad m => a -> m a@; the type of @(==)@ is
1830 @Eq a => a -> a -> Bool@.  The type of @f@ should be
1831 therefore @(Monad m, Eq (m a)) => a -> m a -> Bool@, and the context
1832 cannot be simplified further.
1833
1834 The instance declaration derived from a data type @deriving@ clause
1835 (see Section~\ref{derived-decls})
1836 must, like any instance declaration, have a {\em simple} context; that is,
1837 all the constraints must be of the form "C a", where "a" is a type variable.
1838 For example, in the type
1839 \bprog
1840 @
1841   data Apply a b = App (a b)  deriving Show
1842 @
1843 \eprog
1844 the derived Show instance will produce a context @Show (a b)@, which
1845 cannot be reduced and is not simple; thus a static error results.
1846
1847 \subsubsection{Monomorphism}
1848 \label{monomorphism}
1849 Sometimes it is not possible to generalize over all the type variables
1850 used in the type of the definition.
1851 For example, consider the declaration\nopagebreak[4]
1852 \bprog
1853 @
1854   f x = let g y z = ([x,y], z)
1855         in ...
1856 @
1857 \eprog
1858 In an environment where @x@ has type "a",
1859 the type of @g@'s definition is 
1860 "a \rightarrow b \rightarrow @([@a@]@,b@)@".
1861 The generalization step attributes to @g@ the type 
1862 "\forall b.~ a \rightarrow b \rightarrow @([@a@]@,b@)@";
1863 only "b" can be universally quantified because "a" occurs in the
1864 type environment.
1865 We say that the type of @g@ is {\em monomorphic in the type variable "a"}.
1866 \index{monomorphic type variable}
1867
1868 The effect of such monomorphism is that the first argument of all 
1869 applications of @g@ must be of a single type.  
1870 For example, it would be valid for
1871 the ``@...@'' to be
1872 \bprog
1873 @
1874   (g True, g False)
1875 @
1876 \eprog
1877 (which would, incidentally, force @x@ to have type @Bool@) but invalid
1878 for it to be 
1879 \bprog
1880 @
1881   (g True, g 'c')
1882 @
1883 \eprog
1884 In general, a type "\forall \overline{u}.~cx \Rightarrow t"
1885 is said to be {\em monomorphic}
1886 \index{monomorphic type variable}
1887 in the type variable "a" if "a" is free in
1888 "\forall \overline{u}.~cx \Rightarrow t".
1889
1890 It is worth noting that the explicit type signatures provided by \Haskell{}
1891 are not powerful enough to express types that include monomorphic type
1892 variables.  For example, we cannot write
1893 \bprog
1894 @
1895   f x = let 
1896           g :: a -> b -> ([a],b)
1897           g y z = ([x,y], z)
1898         in ...
1899 @
1900 \eprog
1901 because that would claim that @g@ was polymorphic in both @a@ and @b@
1902 (Section~\ref{type-signatures}).  In this program, @g@ can only be given
1903 a type signature if its first argument is restricted to a type not involving
1904 type variables; for example
1905 \bprog
1906 @
1907   g :: Int -> b -> ([Int],b)
1908 @
1909 \eprog
1910 This signature would also cause @x@ to have type @Int@.
1911
1912 \subsubsection{The Monomorphism Restriction}
1913 \index{monomorphism restriction}
1914 \label{sect:monomorphism-restriction}
1915
1916 \Haskell{} places certain extra restrictions on the generalization
1917 step, beyond the standard Hindley-Milner restriction described above,
1918 which further reduces polymorphism in particular cases.
1919
1920 The monomorphism restriction depends on the binding syntax of a
1921 variable.  Recall that a variable is bound by either a {\em function
1922 binding} or a {\em pattern binding}, and that a {\em simple} pattern
1923 binding is a pattern binding in which the pattern consists of only a
1924 single variable (Section~\ref{pattern-bindings}).
1925
1926 The following two rules define the monomorphism restriction:
1927 \outline{
1928 \paragraph*{The monomorphism restriction}
1929
1930 \begin{description}
1931 \item[Rule 1.]
1932 We say that a given declaration group is {\em unrestricted} if and only if:
1933 \begin{description}
1934 \item[(a):]
1935 every variable in the group is bound by a function binding or a simple
1936 pattern binding\index{simple pattern binding} (Section~\ref{patbind}), {\em and}
1937 \item[(b):]
1938 an explicit type signature is given for every variable in the group
1939 that is bound by simple pattern binding.
1940 \end{description}
1941 The usual Hindley-Milner restriction on polymorphism is that
1942 only type variables that do not occur free in the environment may be generalized.
1943 In addition, {\em the constrained type variables of
1944 a restricted declaration group may not be generalized}
1945 in the generalization step for that group.
1946 (Recall that a type variable is constrained if it must belong
1947 to some type class; see Section~\ref{generalization}.)
1948
1949 % \item[Rule 1.]
1950 % The variables of a given declaration group are monomorphic in
1951 % all their constrained type variables if and only if:
1952 % \begin{description}
1953 % \item[either (a):]
1954 % one or more variables in the declaration group 
1955 % is bound by a non-simple pattern binding.
1956 % \item[or (b):]
1957 % one or more variables in the declaration group is bound 
1958 % by a simple pattern binding, and
1959 % no type signature is given for any of the variables in the group.
1960 % \end{description}
1961
1962 \item[Rule 2.]
1963 Any monomorphic type variables that remain when type inference for
1964 an entire module is complete, are considered {\em ambiguous}\index{ambiguous type},
1965 and are resolved to particular types using the defaulting 
1966 rules (Section~\ref{default-decls}).
1967 \end{description}
1968 }
1969
1970 % When all variables in a declaration group are declared using function
1971 % binding the monomorphism restriction will not apply.  Any variable
1972 % declared in a non-simple pattern binding will invoke monomorphism for
1973 % the entire group containing it.  Simple pattern bindings will be
1974 % monomorphic unless a type signature is supplied.
1975 %
1976
1977 \paragraph*{Motivation}
1978
1979 Rule 1 is required for two reasons, both of which are fairly subtle.
1980 \begin{itemize}
1981 \item
1982 {\em Rule 1 prevents computations from being unexpectedly repeated.}
1983 For example, @genericLength@ is a standard function (in library @List@) whose
1984 type is given by
1985 \bprog
1986 @
1987   genericLength :: Num a => [b] -> a
1988 @
1989 \eprog
1990 Now consider the following expression:
1991 \bprog
1992 @
1993   let { len = genericLength xs } in (len, len)
1994 @
1995 \eprog
1996 It looks as if @len@ should be computed only once, but without Rule~1 it might
1997 be computed twice, once at each of two different overloadings.  If the 
1998 programmer does actually wish the computation to be repeated, an explicit
1999 type signature may be added:
2000 \bprog
2001 @
2002   let { len :: Num a => a; len = genericLength xs } in (len, len)
2003 @
2004 \eprog
2005
2006 \item {\em Rule~1 prevents ambiguity.}  For example, consider the declaration
2007 group
2008 \bprog
2009 @
2010   [(n,s)] = reads t
2011 @
2012 \eprog
2013 Recall that @reads@ is a standard function whose type is given by the
2014 signature
2015 \bprog
2016 @
2017   reads :: (Read a) => String -> [(a,String)]
2018 @
2019 \eprog
2020 Without Rule~1, @n@ would be assigned the 
2021 type "\forall a.~@Read@~a \Rightarrow a" 
2022 and @s@ the type "\forall a." "@Read@~a" "\Rightarrow @String@".
2023 The latter is an invalid type, because it is inherently ambiguous.
2024 It is not possible to determine at what overloading to use @s@, nor
2025 can this be solved by adding a type signature for @s@.
2026 Hence, when {\em non-simple} pattern bindings\index{simple pattern binding}
2027 are used (Section~\ref{patbind}), the types inferred are 
2028 always monomorphic in their constrained type variables, irrespective of whether
2029 a type signature is provided.
2030 In this case, both @n@ and @s@ are monomorphic in "a".
2031
2032 The same constraint applies to pattern-bound functions.  For example, in
2033 \bprog
2034 @
2035   (f,g) = ((+),(-))
2036 @
2037 \eprog
2038 both @f@ and @g@ are monomorphic regardless of any type
2039 signatures supplied for @f@ or @g@.
2040 \end{itemize}
2041
2042 Rule~2 is required because there is no way to enforce monomorphic use
2043 of an {\em exported} binding, except by performing type inference on modules
2044 outside the current module.  Rule~2 states that the exact types of all
2045 the variables bound in a module must be determined by that module alone, and not
2046 by any modules that import it.
2047 \bprog
2048 @
2049   module M1(len1) where
2050     default( Int, Double )
2051     len1 = genericLength "Hello"
2052
2053   module M2 where
2054     import M1(len1)
2055     len2 = (2*len1) :: Rational
2056 @
2057 \eprog
2058 When type inference on module @M1@ is complete, @len1@ has the 
2059 monomorphic type @Num a => a@ (by Rule 1).  Rule 2 now states that
2060 the monomorphic type variable @a@ is ambiguous, and must be resolved using
2061 the defaulting rules of Section~\ref{default-decls}.
2062 Hence, @len1@ gets type @Int@, and its use in @len2@ is type-incorrect.
2063 (If the above code is actually what is wanted, a type signature on
2064 @len1@ would solve the problem.)
2065
2066 This issue does not arise for nested bindings, because their entire scope is 
2067 visible to the compiler.
2068
2069 \paragraph*{Consequences}
2070
2071 The monomorphism rule has a number of consequences for the programmer.
2072 Anything defined with function syntax usually
2073 generalizes as a function is expected to.  Thus in
2074 \bprog
2075 @
2076   f x y = x+y
2077 @
2078 \eprog
2079 the function @f@ may be used at any overloading in class @Num@.
2080 There is no danger of recomputation here.  However, the same function
2081 defined with pattern syntax:
2082 \bprog
2083 @
2084   f = \x -> \y -> x+y
2085 @
2086 \eprog
2087 requires a type signature if @f@ is to be fully overloaded.
2088 Many functions are most naturally defined using simple pattern
2089 bindings; the user must be careful to affix these with type signatures
2090 to retain full overloading.  The standard prelude contains many
2091 examples of this:
2092 \bprog
2093 @
2094   sum  :: (Num a) => [a] -> a
2095   sum  =  foldl (+) 0  
2096 @
2097 \eprog
2098
2099 Rule~1 applies to both top-level and nested definitions.  Consider
2100 \bprog
2101 @
2102   module M where
2103     len1 = genericLength "Hello"
2104     len2 = (2*len1) :: Rational
2105 @
2106 \eprog
2107 Here, type inference finds that @len1@ has the monomorphic type (@Num a => a@);
2108 and the type variable @a@ is resolved to @Rational@ when performing type
2109 inference on @len2@.
2110
2111 % Even when a function is defined using a function binding, it may still
2112 % be made monomorphic by another variable in the same declaration group.
2113 % Since groups defined through mutually recursive functions need not be
2114 % syntacticly adjacent, it may be difficult to see where overloading is
2115 % being lost.  In this example @fact'@ is defined with a pattern binding
2116 % and forces @fact@ to be monomorphic in the absence of a type signature
2117 % for either @fact@ or @fact'@.  This would in turn result in an error as
2118 % per Rule~2.
2119 % \bprog
2120
2121 % module Mod1(fact)
2122 % import Mod2
2123 % fact 0 = 1
2124 % fact n = n*fact'(n-1)
2125
2126 % module Mod2(fact')
2127 % import Mod1
2128 % fact' = fact
2129
2130 % \eprog
2131
2132 \subsection{Kind Inference}
2133 \index{kind}
2134 \index{kind inference}
2135 \label{kindinference}
2136
2137 This section describes the rules that are used to perform {\em kind
2138 inference}, i.e. to calculate a suitable kind for each type
2139 constructor and class appearing in a given
2140 program.
2141
2142 The first step in the kind inference process is to arrange the set of
2143 datatype, synonym, and class definitions into dependency groups.  This can
2144 be achieved in much the same way as the dependency analysis for value
2145 declarations that was described in Section~\ref{dependencyanalysis}.
2146 For example, the following program fragment includes the definition
2147 of a datatype constructor @D@, a synonym @S@ and a class @C@, all of
2148 which would be included in the same dependency group:
2149 \bprog
2150 @
2151   data C a => D a = Foo (S a)
2152   type S a = [D a]
2153   class C a where
2154       bar :: a -> D a -> Bool
2155 @
2156 \eprog
2157 The kinds of variables, constructors, and classes within each group
2158 are determined using standard techniques of type inference and
2159 kind-preserving unification \cite{jones:cclasses}.  For example, in the
2160 definitions above, the parameter @a@ appears as an argument of the
2161 function constructor @(->)@ in the type of @bar@ and hence must
2162 have kind $\ast$.  It follows that both @D@ and @S@ must have
2163 kind $\ast\rightarrow\ast$ and that every instance of class @C@ must
2164 have kind $\ast$.
2165
2166 % The kind of any constructor that is exported from a module without
2167 % exposing its definition must be specified explicitly in the interface
2168 % for that module.  This is described in Section~\ref{somebodyneedstofillthisin}.
2169
2170 It is possible that some parts of an inferred kind may not be fully
2171 determined by the corresponding definitions; in such cases, a default
2172 of $\ast$ is assumed.  For example, we could assume an arbitrary kind
2173 $\kappa$ for the @a@ parameter in each of the following examples:
2174 \bprog
2175 @
2176   data App f a = A (f a)
2177   data Tree a  = Leaf | Fork (Tree a) (Tree a)
2178 @
2179 \eprog
2180 This would give kinds
2181 $(\kappa\rightarrow\ast)\rightarrow\kappa\rightarrow\ast$ and
2182 $\kappa\rightarrow\ast$ for @App@ and @Tree@, respectively, for any
2183 kind $\kappa$, and would require an extension to allow polymorphic
2184 kinds.  Instead, using the default binding $\kappa=\ast$, the
2185 actual kinds for these two constructors are
2186 $(\ast\rightarrow\ast)\rightarrow\ast\rightarrow\ast$ and
2187 $\ast\rightarrow\ast$, respectively.
2188
2189 Defaults are applied to each dependency group without consideration of
2190 the ways in which particular type constructor constants or classes are
2191 used in later dependency groups or elsewhere in the program.  For example,
2192 adding the following definition to those above does not influence the
2193 kind inferred for @Tree@ (by changing it to
2194 $(\ast\rightarrow\ast)\rightarrow\ast$, for instance), and instead
2195 generates a static error because the kind of @[]@, $\ast\rightarrow\ast$,
2196 does not match the kind $\ast$ that is expected for an argument of @Tree@:
2197 \bprog
2198 @
2199   type FunnyTree = Tree []     -- invalid
2200 @
2201 \eprog
2202 This is important because it ensures that each constructor and class are
2203 used consistently with the same kind whenever they are in scope.
2204
2205 %**~footer
2206
2207 % Local Variables: 
2208 % mode: latex
2209 % End: