In this section, we describe the syntax and informal semantics of Haskell declarations.

module        -> module modid [exports] where body
              |  body
body          -> { [impdecls ;] [[fixdecls ;] topdecls [;]] }
              |  { impdecls [;] }

topdecls      -> topdecl1 ; ... ; topdecln                
topdecl       -> type simpletype = type
              |  data [context =>] simpletype = constrs [deriving]
              |  newtype [context =>] simpletype = con atype [deriving]
              |  class [context =>] simpleclass [where { cbody [;] }]
              |  instance [context =>] qtycls inst [where { valdefs [;] }]
              |  default (type1 , ... , typen)            
              |  decl

decls         -> decl1 ; ... ; decln                      
decl          -> signdecl
              |  valdef
decllist      -> { decls [;] }

signdecl      -> vars :: [context =>] type

vars          -> var1 , ..., varn                      (n>=1)

The declarations in the syntactic category topdecls are only allowed at the top level of a Haskell module (see Section 5), whereas decls may be used either at the top level or in nested scopes (i.e. those within a let or where construct).

For exposition, we divide the declarations into three groups: user-defined datatypes, consisting of type, newtype, and data declarations (Section 4.2); type classes and overloading, consisting of class, instance, and default declarations (Section 4.3); and nested declarations, consisting of value bindings and type signatures (Section 4.4).

Haskell has several primitive datatypes that are "hard-wired" (such as integers and floating-point numbers), but most "built-in" datatypes are defined with normal Haskell code, using normal type and data declarations. These "built-in" datatypes are described in detail in Section 6.1.

4.1 Overview of Types and Classes

Haskell uses a traditional Hindley-Milner polymorphic type system to provide a static type semantics , but the type system has been extended with type and constructor classes (or just classes) that provide a structured way to introduce overloaded functions. classUnmatched {

A class declaration (Section 4.3.1) introduces a new type class and the overloaded operations that must be supported by any type that is an instance of that class. An instance declaration (Section 4.3.2) declares that a type is an instance of a class and includes the definitions of the overloaded operations---called class methods---instantiated on the named type.

For example, suppose we wish to overload the operations (+) and negate on types Int and Float. We introduce a new type class called Num:

class Num a  where          -- simplified class declaration for Num
  (+)    :: a -> a -> a
  negate :: a -> a

We may then declare Int and Float to be instances of this class:

instance Num Int  where     -- simplified instance of Num Int
  x + y       =  addInt x y
  negate x    =  negateInt x

instance Num Float  where   -- simplified instance of Num Float
  x + y       =  addFloat x y
  negate x    =  negateFloat x

More examples of type and constructor classes can be found in the papers by Jones or Wadler and Blott . The term `type class' was used to describe the original Haskell 1.0 type system; `constructor class' was used to describe an extension to the original type classes. There is no longer any reason to use two different terms: in this report, `type class' includes both the original Haskell type classes and the constructor classes introduced by Jones.

4.1.1 Syntax of Types

type          -> btype [-> type]                       (function type)

btype         -> [btype] atype                         (type application)

atype         -> gtycon
              |  tyvar
              |  ( type1 , ... , typek )               (tuple type, k>=2)
              |  [ type ]                              (list type)
              |  ( type )                              (parenthesised constructor)

gtycon        -> qtycon
              |  ()                                    (unit type)
              |  []                                    (list constructor)
              |  (->)                                  (function constructor)
              |  (,{,})                                (tupling constructors)

The syntax for Haskell type expressions is given above. Just as data values are built using data constructors, type values are built from type constructors. As with data constructors, the names of type constructors start with uppercase letters.

To ensure that they are valid, type expressions are classified into different kinds which take one of two possible forms:

• The symbol * represents the kind of all nullary type constructors.

• If k1 and k2 are kinds, then k1->k2 is the kind of types that take a type of kind k1 and return a type of kind k2.

1. Type variables, written as identifiers beginning with a lowercase letter. The kind of a variable is determined implicitly by the context in which it appears.

2. Type constructors. Most type constructors are written as identifiers beginning with an uppercase letter. For example:
   • Char, Int, Integer, Float, Double and Bool are type constants with kind *.
   • Maybe and IO are unary type constructors, and treated as types with kind *->*.
   • A datatype declaration data T ... adds the type constructor T to the type vocabulary. The kind of T is determined by kind inference.
   Special syntax is provided for some type constructors:
   • The trivial type is written as () and has kind *. It denotes the "nullary tuple" type, and has exactly one value, also written () (see Sections 3.9 and 6.1.5).
   • The function type is written as (->) and has kind *->*->*.
   • The list type is written as [] and has kind *->*.
   • The tuple types are written as (,), (,,), and so on. Their kinds are *->*->*, *->*->*->*, and so on.
   Use of the (->) and [] constants is described in more detail below.

3. Type application. If t1 is a type of kind k1->k2 and t2 is a type of kind k1, then t1 t2 is a type expression of kind k2.

4. A parenthesised type, having form (t), is identical to the type t.

Special syntax is provided to allow certain type expressions to be written in a more traditional style:

1. A function type has the form t1 -> t2, which is equivalent to the type (->) t1 t2. Function arrows associate to the right.

2. A tuple type has the form (t1,..., t_k) where k>=2, which is equivalent to the type (,...,) t1 ... t_k where there are k-1 commas between the parenthesis. It denotes the type of k-tuples with the first component of type t1, the second component of type t2, and so on (see Sections 3.8 and 6.1.4).

3. A list type has the form [t] which is equivalent to the type [] t. It denotes the type of lists with elements of type t (see Sections 3.7 and 6.1.3).

Expressions and types have a consistent syntax. If t_i is the type of expression or pattern e_i, then the expressions (\ e1 -> e2), [e1], and (e1,e2) have the types (t1 -> t2), [t1], and (t1,t2), respectively.

With one exception, the type variables in a Haskell type expression are all assumed to be universally quantified; there is no explicit syntax for universal quantification . For example, the type expression a -> a denotes the type for all a. a -> a. For clarity, however, we often write quantification explicitly when discussing the types of Haskell programs.

The exception referred to is that of the distinguished type variable in a class declaration (Section 4.3.1).

4.1.2 Syntax of Class Assertions and Contexts

context       -> class
              |  ( class1 , ... , classn )             (n>=1)
class         -> qtycls tyvar 
simpleclass   -> tycls tyvar 
tycls         -> conid
tyvar         -> varid

A context consists of one or more class assertions, and has the general form

( C_1 u_1, ..., C_n u_n )

where C1, ..., C_n are class identifiers, and u1, ..., u_n are type variables; the parentheses may be omitted when n=1. In general, we use c to denote a context and we write c => t to indicate the type t restricted by the context c. The context c must only contain type variables referenced in t. For convenience, we write c => t even if the context c is empty, although in this case the concrete syntax contains no =>.

4.1.3 Semantics of Types and Classes

In this subsection, we provide informal details of the type system. (Wadler and Blott and Jones discuss type and constructor classes, respectively, in more detail.)

The Haskell type system attributes a type to each expression in the program. In general, a type is of the form for all u. c => t, where u is a set of type variables u1, ..., u_n. In any such type, any of the universally-quantified type variables u_i which are free in c must also be free in t. Furthermore, the context c must be of the form given above in Section 4.1.2; that is, it must have the form (C1 u1, ..., C_n u_n) where C1, ..., C_n are class identifiers, and u1, ..., u_n are type variables.

The type of an expression e depends on a type environment that gives types for the free variables in e, and a class environment that declares which types are instances of which classes (a type becomes an instance of a class only via the presence of an instance declaration or a deriving clause).

Types are related by a generalization order (specified below); the most general type that can be assigned to a particular expression (in a given environment) is called its principal type. Haskell's extended Hindley-Milner type system can infer the principal type of all expressions, including the proper use of overloaded class methods (although certain ambiguous overloadings could arise, as described in Section 4.3.4). Therefore, explicit typings (called type signatures) are usually optional (see Sections 3.16 and 4.4.1).

The type for all u. c1 => t1 is more general than the type for all w. c2 => t2 if and only if there is a substitution S whose domain is u such that:

• t2 is identical to S(t1).
• Whenever c2 holds in the class environment, S(c1) also holds.

The main point about contexts above is that, given the type for all u. c => t, the presence of C u_i in the context c expresses the constraint that the type variable u_i may be instantiated as t' within the type expression t only if t' is a member of the class C. For example, consider the function double:

	double x = x + x

4.2 User-Defined Datatypes

In this section, we describe algebraic datatypes (data declarations), renamed datatypes (newtype declarations), and type synonyms (type declarations). These declarations may only appear at the top level of a module.

4.2.1 Algebraic Datatype Declarations

topdecl       -> data [context =>] simpletype = constrs [deriving]

simpletype    -> tycon tyvar1 ... tyvark 

constrs       -> constr1 | ... | constrn               (n>=1)
constr        -> con [!] atype1 ... [!] atypek         (arity con = k, k>=0)
              |  (btype | ! atype) conop (btype | ! atype)  (infix conop)
              |  con { fielddecl1 , ... , fielddecln }  (n>=1)
fielddecl     -> vars :: (type | ! atype)

deriving      -> deriving (dclass | (dclass1, ... , dclassn)) (n>=0)
dclass        -> qtycls

An algebraic datatype declaration introduces a new type and constructors over that type and has the form:

data c => T u_1 ... u_k = K_1 t_11 ... t_1k_1 | ... | K_n t_n1 ... t_nk_n

where c is a context. This declaration introduces a new type constructor T with constituent data constructors K1, ..., K_n whose types are given by:

K_i :: for all u_1 ... u_k. c_i => t_i1 -> ... -> t_ik_i -> (T u_1 ... u_k)

where c_i is the largest subset of c that constrains only those type variables free in the types t_i1, ..., t_iki. The type variables u1 through u_k must be distinct and may appear in c and the t_ij; it is a static error for any other type variable to appear in c or on the right-hand-side. The new type constant T has a kind of the form k1->...->k_k->* where the kinds k_i of the argument variables u_i are determined by kind inference as described in Section 4.6. This means that T may be used in type expressions with anywhere between 0 and k arguments.

For example, the declaration

data Eq a => Set a = NilSet | ConsSet a (Set a)

In the example given, the overloaded type for ConsSet ensures that ConsSet can only be applied to values whose type is an instance of the class Eq. The context in the data declaration has no other effect whatsoever.

The visibility of a datatype's constructors (i.e. the "abstractness" of the datatype) outside of the module in which the datatype is defined is controlled by the form of the datatype's name in the export list as described in Section 5.5.

The optional deriving part of a data declaration has to do with derived instances, and is described in Section 4.3.3.

4.2.2 Labeled Fields

data C = F { f1,f2 :: Int, f3 :: Bool}

data C = F Int Int Bool

4.2.3 Strictness Flags

Translation: A declaration of the form data c => T u_1 ... u_k = ... | K s_1 ... s_n | ... where each si is either of the form ! ti or ti, is replaced by a declaration of the form data c => T u_1 ... u_k = ... | K' t_1 ... t_n | ... each occurrence of K in a pattern is replaced by K', where K' is a `hidden constructor' not directly available to the programmer. Each occurrence of K in an expression is replaced with (\ x_1 ... x_n -> ( ((K' op_1 x_1) op_2 x_2) ... ) op_n x_n) where opi is the lazy apply function $ if si is of the form ti, and opi is the strict apply function `strict` (see Section 6.2.7) if si is of the form ! ti.

Strictness flags may require the explicit inclusion of an Eval context in a data declaration (see Section 6.2.7). This occurs precisely when the context of a strict function used in the above translation propagates to a type variable. For example, in

data (Eval a) => Pair a b = MakePair !a b

data (Integral a) => Rational a = !a :% !a  -- Rational library

4.2.4 Type Synonym Declarations

topdecl       -> type simpletype = type
simpletype    -> tycon tyvar1 ... tyvark

type T u_1 ... u_k = t

which introduces a new type constructor, T. The type (T t1 ... t_k) is equivalent to the type t[t1/u1, ..., t_k/u_k]. The type variables u1 through u_k must be distinct and are scoped only over t; it is a static error for any other type variable to appear in t. The kind of the new type constructor T is of the form k1->...->k_k->k where the kinds k_i of the arguments u_i and k of the right hand side t are determined by kind inference as described in Section 4.6. For example, the following definition can be used to provide an alternative way of writing the list type constructor:

	type List = []

Although recursive and mutually recursive datatypes are allowed, this is not so for type synonyms, unless an algebraic datatype intervenes. For example,

type Rec a   =  [Circ a]
data Circ a  =  Tag [Rec a]

type Rec a   =  [Circ a]        -- invalid
type Circ a  =  [Rec a]         --

4.2.5 Datatype Renamings

Type synonyms are a strictly syntactic mechanism to make type signatures more readable. A synonym and its definition are completely interchangeable.

topdecl       -> newtype [context =>] simpletype = con atype [deriving]
simpletype    -> tycon tyvar1 ... tyvark               

A declaration of the form

newtype c => T u_1 ... u_k = N t

is valid if and only if

data c => T u_1 ... u_k = N !t

is valid (see Section 4.2.1). The type ( T u1 ... u_k ) renames the datatype t.

A newtype declaration introduces a new type whose representation is the same as an existing type. It differs from a type synonym in that it creates a distinct type which must be explicitly coerced to or from the original type. The constructor N in an expression coerces a value from type t to type ( T u1 ... u_k ). Using N in a pattern coerces a value from type ( T u1 ... u_k ) to type t. These coercions are free of any execution time overhead; newtype does not change the underlying representation of an object.

New instances (see Section 4.3.2) can be defined for a type defined by newtype but may not be defined for a type synonym. A type created by newtype differs from an algebraic datatype in that the representation of an algebraic datatype has an extra level of indirection. This difference makes access to the representation less efficient. The difference is reflected in different rules for pattern matching (see Section 3.17). Unlike algebraic datatypes, the newtype constructor N is unlifted, so that N bottom is the same as bottom.

The following examples clarify the differences between data (algebraic datatypes), type (type synonyms), and newtype (renaming types.) Given the declarations

data D1 = D1 Int
data D2 = D2 !Int
type S = Int
newtype N = N Int
d1 (D1 i) = 42
d2 (D2 i) = 42
s i = 42
n (N i) = 42

The optional deriving part of a newtype declaration is treated in the same way as the deriving component of a data declaration; see Section 4.3.3.

4.3 Type Classes and Overloading

4.3.1 Class Declarations

topdecl       -> class [context =>] simpleclass [where { cbody [;] }]
cbody         -> [ cmethods [ ; cdefaults ] ]
cmethods      -> signdecl1 ; ... ; signdecln           (n >= 1)
cdefaults     -> valdef1 ; ... ; valdefn               (n >= 1)

A class declaration introduces a new class and the operations ( class methods) on it. A class declaration has the general form:

This introduces a new class name C; the type variable u is scoped only over the class method signatures in the class body. The context c specifies the superclasses of C, as described below; the only type variable that may be referred to in c is u. The class declaration introduces new class methods v1, ..., v_n, whose scope extends outside the class declaration, with types:

v_i :: for all u,w. (C u, c_i) => t_i

The t_i must mention u; they may mention type variables w other than u, and the type of v_i is polymorphic in both u and w. The c_i may constrain only w; in particular, the c_i may not constrain u. For example:

	class Foo a where
		op :: Num b => a -> b -> a

Default class methods for any of the v_i may be included in the class declaration as a normal valdef; no other definitions are permitted. The default class method for v_i is used if no binding for it is given in a particular instance declaration (see Section 4.3.2).

Class methods share the top level namespace with variable bindings and field names; they must not conflict with other top level bindings in scope. That is, a class method can not have the same name as a top level definition, a field name, or another class method.

A class declaration with no where part may be useful for combining a collection of classes into a larger one that inherits all of the class methods in the original ones. For example:

class  (Read a, Show a) => Textual a

The superclass relation must not be cyclic; i.e. it must form a directed acyclic graph.

4.3.2 Instance Declarations

topdecl       -> instance [context =>] qtycls inst [where { valdefs [;] }]
inst          -> gtycon
              |  ( gtycon tyvar1 ... tyvark )          (k>=0, tyvars  distinct)
              |  ( tyvar1 , ... , tyvark )             (k>=2, tyvars  distinct)
              |  [ tyvar ]
              |  ( tyvar1 -> tyvar2 )                  tyvar1  and tyvar2  distinct
valdefs       -> valdef1 ; ... ; valdefn               (n>=0)

class c => C u where { cbody }

be a class declaration. The general form of the corresponding instance declaration is:

instance c' => C (T u_1 ... u_k) where { d }

where k>=0 and T is not a type synonym. The constructor being instanced, (T u1 ... u_k), is a type constructor applied to simple type variables u1, ... u_k, which must be distinct. This prohibits instance declarations such as:

instance C (a,a) where ...
instance C (Int,a) where ...
instance C [[a]] where ...

If no binding is given for some class method then the corresponding default class method in the class declaration is used (if present); if such a default does not exist then the class method of this instance is bound to undefined and no compile-time error results.

An instance declaration that makes the type T to be an instance of class C is called a C-T instance declaration and is subject to these static restrictions:

• A type may not be declared as an instance of a particular class more than once in the program.

• The class and type must have the same kind.

• Assume that the type variables in the instance type (T u1 ... u_k) satisfy the constraints in the instance context c'. Under this assumption, the following two conditions must also be satisfied:
  1. The constraints expressed by the superclass context c[(T u1 ... uk)/u] of C must be satisfied. In other words, T must be an instance of each of C's superclasses and the contexts of all superclass instances must be implied by c'.
  2. Any constraints on the type variables in the instance type that are required for the class method declarations in d to be well-typed must also be satisfied.

  In fact, except in pathological cases it is possible to infer from the instance declaration the most general instance context c' satisfying the above two constraints, but it is nevertheless mandatory to write an explicit instance context.

class Foo a => Bar a where ...

instance (Eq a, Show a) => Foo [a] where ...

instance Num a => Bar [a] where ...

If the two instance declarations instead read like this:

instance Num a => Foo [a] where ...

instance (Eq a, Show a) => Bar [a] where ...

Further examples of instance declarations may be found in Appendix A.

4.3.3 Derived Instances

As mentioned in Section 4.2.1, data and newtype declarations contain an optional deriving form. If the form is included, then derived instance declarations are automatically generated for the datatype in each of the named classes. These instances are subject to the same restrictions as user-defined instances. When deriving a class C for a type T, instances for all superclasses of C must exist for T, either via an explicit instance declaration or by including the superclass in the deriving clause.

Derived instances provide convenient commonly-used operations for user-defined datatypes. For example, derived instances for datatypes in the class Eq define the operations == and /=, freeing the programmer from the need to define them.

The only classes in the Prelude for which derived instances are allowed are Eq, Ord, Enum, Bounded, Show, and Read, all defined in Figure 5, page . The precise details of how the derived instances are generated for each of these classes are provided in Appendix D, including a specification of when such derived instances are possible. Instances of class Eval are always implicitly derived for algebraic datatypes. The class Eval is may not be explicitly listed in a deriving form or defined by an explicit instance declaration. Classes defined by the standard libraries may also be derivable.

A static error results if it is not possible to derive an instance declaration over a class named in a deriving form. For example, not all datatypes can properly support class methods in Enum. It is also a static error to give an explicit instance declaration for a class that is also derived.

If the deriving form is omitted from a data or newtype declaration, then no instance declarations (except for Eval) are derived for that datatype; that is, omitting a deriving form is equivalent to including an empty deriving form: deriving ().

4.3.4 Defaults for Overloaded Numeric Operations

topdecl       -> default (type1 , ... , typen)            

A problem inherent with Haskell-style overloading is the possibility of an ambiguous type. For example, using the read and show functions defined in Appendix D, and supposing that just Int and Bool are members of Read and Show, then the expression

let x = read "..." in show x	-- invalid

could be satisfied by instantiating a as either Int in both cases, or Bool. Such expressions are considered ill-typed, a static error.

We say that an expression e is ambiguously overloaded if, in its type for all u. c => t, there is a type variable u in u which occurs in c but not in t. Such types are invalid.

For example, the earlier expression involving show and read is ambiguously overloaded since its type is for all a. Show a, Read a => String.

Overloading ambiguity can only be circumvented by input from the user. One way is through the use of expression type-signatures as described in Section 3.16. For example, for the ambiguous expression given earlier, one could write:

let x = read "..." in show (x::Bool)

Occasionally, an otherwise ambiguous expression needs to be made the same type as some variable, rather than being given a fixed type with an expression type-signature. This is the purpose of the function asTypeOf (Appendix A): x `asTypeOf` y has the value of x, but x and y are forced to have the same type. For example,

approxSqrt x = encodeFloat 1 (exponent x `div` 2) `asTypeOf` x

Ambiguities in the class Num are most common, so Haskell provides another way to resolve them---with a default declaration:

default (t_1 , ... , t_n)

where n>=0, and each t_i must be a monotype for which Num t_i holds. In situations where an ambiguous type is discovered, an ambiguous type variable is defaultable if at least one of its classes is a numeric class (that is, Num or a subclass of Num) and if all of its classes are defined in the Prelude or a standard library (Figures 6--7, pages -- show the numeric classes, and Figure 5, page , shows the classes defined in the Prelude.) Each defaultable variable is replaced by the first type in the default list that is an instance of all the ambiguous variable's classes. It is a static error if no such type is found.

Only one default declaration is permitted per module, and its effect is limited to that module. If no default declaration is given in a module then it assumed to be:

default (Int, Double)

4.4 Nested Declarations

The following declarations may be used in any declaration list, including the top level of a module.

4.4.1 Type Signatures

signdecl      -> vars :: [context =>] type

v_1, ..., v_n :: c => t

which is equivalent to asserting v_i :: c => t for each i from 1 to n. Each v_i must have a value binding in the same declaration list that contains the type signature; i.e. it is invalid to give a type signature for a variable bound in an outer scope. Moreover, it is invalid to give more than one type signature for one variable.

As mentioned in Section 4.1.1, every type variable appearing in a signature is universally quantified over that signature, and hence the scope of a type variable is limited to the type signature that contains it. For example, in the following declarations

f :: a -> a
f x = x :: a			-- invalid

If a given program includes a signature for a variable f, then each use of f is treated as having the declared type. It is a static error if the same type cannot also be inferred for the defining occurrence of f.

If a variable f is defined without providing a corresponding type signature declaration, then each use of f outside its own declaration group (see Section 4.5) is treated as having the corresponding inferred, or principal type . However, to ensure that type inference is still possible, the defining occurrence, and all uses of f within its declaration group must have the same monomorphic type (from which the principal type is obtained by generalization, as described in Section 4.5.2).

For example, if we define

sqr x  =  x*x

sqr :: Int -> Int

sqr :: (Num a, Num b) => a -> b     -- invalid
sqr :: a -> a                       -- invalid

Type signatures can also be used to support polymorphic recursion. The following definition is pathological, but illustrates how a type signature can be used to specify a type more general than the one that would be inferred:

        data T a  =  K (T Int) (T a)
        f         :: T a -> a
        f (K x y) =  if f x == 1 then f y else undefined

4.4.2 Function and Pattern Bindings

decl          -> valdef

valdef        -> lhs = exp [where decllist]
              |  lhs gdrhs [where decllist]

lhs           -> pat0
              |  funlhs

funlhs        -> var apat { apat }
              |  pati+1 varop(a,i) pati+1
              |  lpati varop( l,i) pati+1
              |  pati+1 varop( r,i) rpati

gdrhs         -> gd = exp [gdrhs]

gd            -> | exp0 

Function bindings. A function binding binds a variable to a function value. The general form of a function binding for variable x is:

where each p_ij is a pattern, and where each match_i is of the general form:

or

and where n>=1, 1<=i<=n, m_i>=1. The former is treated as shorthand for a particular case of the latter, namely:

Note that all clauses defining a function must be contiguous, and the number of patterns in each clause must be the same. The set of patterns corresponding to each match must be linear---no variable is allowed to appear more than once in the entire set.

Alternative syntax is provided for binding functional values to infix operators. For example, these two function definitions are equivalent:

plus x y z = x+y+z
x `plus` y = \ z -> x+y+z

Translation: The general binding form for functions is semantically equivalent to the equation (i.e. simple pattern binding): x x1 x2 ... xk = case (x1, ..., xk) of (p11, ..., p1k) match1 ... (pm1, ..., pmk) matchm where the xi are new identifiers.

Pattern bindings. A pattern binding binds variables to values. A simple pattern binding has form p = e. The pattern p is matched "lazily" as an irrefutable pattern , as if there were an implicit ~ in front of it. See the translation in Section 3.12.

The general form of a pattern binding is p match, where a match is the same structure as for function bindings above; in other words, a pattern binding is:

Translation: The pattern binding above is semantically equivalent to this simple pattern binding: p = let decls in if g1 then e1 else if g2 then e2 else ... if gm then em else error "Unmatched pattern"

4.5 Static Semantics of Function and Pattern Bindings

The static semantics of the function and pattern bindings of a let expression or where clause are discussed in this section.

4.5.1 Dependency Analysis

4.5.2 Generalization

The Hindley-Milner type system assigns types to a let-expression in two stages. First, the right-hand side of the declaration is typed, giving a type with no universal quantification. Second, all type variables which occur in this type are universally quantified unless they are associated with bound variables in the type environment; this is called generalization. Finally, the body of the let-expression is typed.

For example, consider the declaration

	f x = let g y = (y,y)
	      in ...

When typing overloaded definitions, all the overloading constraints from a single declaration group are collected together, to form the context for the type of each variable declared in the group. For example, in the definition:

	f x = let g1 x y = if x>y then show x else g2 y x
	          g2 p q = g1 q p
	      in ...

The generalization step attributes to both g1 and g2 the type

for all a. (Ord a, Show a) => a -> a -> String

Notice that g2 is overloaded in the same way as g1 even though the occurrences of > and show are in the definition of g1.

If the programmer supplies explicit type signatures for more than one variable in a declaration group, the contexts of these signatures must be identical up to renaming of the type variables.

As mentioned in Section 4.1.3, the context of a type may constrain only type variables. Consider, for example, the definition:

	f xs y  =  xs == [y]

	f :: Eq a => [a] -> a -> Bool

	f :: Eq [a] => [a] -> a -> Bool

At generalization, the context of the generalized type must be reducible. That is, class constraints must apply only to type variables, not more general type expressions. For example, the following example is invalid:

f x = show (return x)

4.5.3 Monomorphism

	f x = let g y z = ([x,y], z)
	      in ...

The effect of such monomorphism is that the first argument of all applications of g must be of a single type. For example, it would be valid for the "..." to be

	(g True, g False)

	(g True, g 'c')

It is worth noting that the explicit type signatures provided by Haskell are not powerful enough to express types which include monomorphic type variables. For example, we cannot write

	f x = let 
		g :: a -> b -> ([a],b)
		g y z = ([x,y], z)
	      in ...

		g :: Int -> b -> ([Int],b)

4.5.4 The Monomorphism Restriction

Haskell places certain extra restrictions on the generalization step, beyond the standard Hindley-Milner restriction described above, which further reduces polymorphism in particular cases.

The monomorphism restriction depends on the binding syntax of a variable. Recall that a variable is bound by either a function binding or a pattern binding, and that a simple pattern binding is a pattern binding in which the pattern consists of only a single variable (Section 4.4.2).

Two rules define the monomorphism restriction:

Rule 1.

We say that a given declaration group is unrestricted if and only if:

(a):

every variable in the group is bound by a function binding or a simple pattern binding, and

(b):

an explicit type signature is given for every variable in the group which is bound by simple pattern binding.

The usual Hindley-Milner restriction on polymorphism is that only type variables free in the environment may be generalized. In addition, the constrained type variables of a restricted declaration group may not be generalized in the generalization step for that group. (Recall that a type variable is constrained if it must belong to some type class; see Section 4.5.2.)

Rule 2.

The type of a variable exported from a module must be completely polymorphic; that is, it must not have any free type variables. It follows from Rule 1 that if all top-level declaration groups are unrestricted, then Rule 2 is automatically satisfied.

Rule 1 is required for two reasons, both of which are fairly subtle. First, it prevents computations from being unexpectedly repeated. For example, genericLength is a standard function (in library List) whose type is given by

	genericLength :: Num a => [b] -> a

	let { len = genericLength xs } in (len, len)

	let { len :: Num a => a; len = genericLength xs } in (len, len)

   (f,g) = ((+),(-))

Rule 1 also prevents ambiguity. For example, consider the declaration group

	[(n,s)] = reads t

	reads :: (Read a) => String -> [(a,String)]

Lastly, Rule 2 is required because there is no way to enforce monomorphic use of an exported binding, except by performing type inference on modules outside the current module.

The monomorphism rule has a number of consequences for the programmer. Anything defined with function syntax usually generalizes as a function is expected to. Thus in

	f x y = x+y

	f = \x -> \y -> x+y

sum            :: (Num a) => [a] -> a
sum            =  foldl (+) 0  

4.6 Kind Inference

This section describes the rules that are used to perform kind inference, i.e. to calculate a suitable kind for each type constructor and class appearing in a given program.

The first step in the kind inference process is to arrange the set of datatype, synonym, and class definitions into dependency groups. This can be achieved in much the same way as the dependency analysis for value declarations that was described in Section 4.5. For example, the following program fragment includes the definition of a datatype constructor D, a synonym S and a class C, all of which would be included in the same dependency group:

	data C a => D a = Foo (S a)
	type S a = [D a]
	class C a where
	    bar :: a -> D a -> Bool

It is possible that some parts of an inferred kind may not be fully determined by the corresponding definitions; in such cases, a default of * is assumed. For example, we could assume an arbitrary kind k for the a parameter in each of the following examples:

	data App f a = A (f a)
	data Tree a  = Leaf | Fork (Tree a) (Tree a)

Defaults are applied to each dependency group without consideration of the ways in which particular type constructor constants or classes are used in later dependency groups or elsewhere in the program. For example, adding the the following definition to those above do not influence the kind inferred for Tree (by changing it to (*->*)->*, for instance), and instead generates a static error because the kind of [], *->*, does not match the kind * that is expected for an argument of Tree:

	type FunnyTree = Tree []     -- invalid

Next section: Modules
The Haskell 1.3 Report