Universally quantified

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 ∀ a. a → a.

For clarity, however, we often write quantification explicitly when discussing the types of Haskell programs. When we write an explicitly quantified type, the scope of the ∀ extends as far to the right as possible; for example, ∀ a. a → a means ∀ a. (a → a).

_P39

Context

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

 ( C1 u1 , . . . , Cn un )

where C1 , . . . , Cn are class identifiers, and each of the u1 , . . . , un is either a type variable, or the application of type variable to one or more types.

In general, we use cx to denote a context and we write cx => t to indicate the type t restricted by the context cx. The context cx must only contain type variables referenced in t. For convenience, we write cx => t even if the context cx is empty, although in this case the concrete syntax contains no =>.

_P39

Type of an expression

The Haskell type system attributes a type to each expression in the program. In general, a type is of the form ∀ u. cx ⇒ t, where u is a set of type variables u1 , . . . , un . In any such type, any of the universally quantified type variables ui that are free in cx must also be free in t.

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 preorder (specified below); the most general type, up to the equivalence induced by the generalization preorder, 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. Therefore, explicit typings (called type signatures) are usually optional.

_P39~P40

Type instantiation

A value of type ∀ u. cx ⇒ t, may be instantiated at types s if and only if the context cx[s/u] holds.

For example, consider the function double:

double x = x + x

The most general type of double is ∀ a. Num a ⇒ a → a. double may be applied to values of type Int (instantiating a to Int), since Num Int holds, because Int is an instance of the class Num.

_P40

Ambiguous types

A problem inherent with Haskell-style overloading is the possibility of an ambiguous type.

For example, using the read and show functions, and supposing that just Int and Bool are members of Read and Show, then the expression is ambiguous, because the types for show and read could be satisfied by instantiating a as either Int in both cases, or Bool.

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

-- show :: ∀ a. Show a ⇒ a → String 
-- read :: ∀ a. Read a ⇒ String → a

Such expressions are considered ill-typed, a static error.

We say that an expression e has an ambiguous type if, in its type ∀ u. cx ⇒ t, there is a type variable v in u that occurs in cx but not in t. Such types are invalid.

For example, the earlier expression involving show and read has an ambiguous type since its type is ∀ a. Show a, Read a ⇒ String.

_P48

Type signatures

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.

If a variable f is defined without providing a corresponding type signature declaration, then each use of f outside its own declaration group 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.

_P49~P50

Function bindings and Simple pattern bindings

A function binding binds a variable to a function value.
A pattern binding binds variables to values. A simple pattern binding has form p = e, The general form of a pattern binding is p match.

_P51~P53

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.

_P56

Delcaration group

In general the static semantics are given by applying the normal Hindley-Milner inference rules. In order to increase polymorphism, these rules are applied to groups of bindings identified by a dependency analysis.

A binding b1 depends on a binding b2 in the same list of declarations if either

1. b1 contains a free identifier that has no type signature and is bound by b2, or
2. b1 depends on a binding that depends on b2.

A declaration group is a minimal set of mutually dependent bindings. Hindley-Milner type inference is applied to each declaration group in dependency order. The order of declarations in where/let constructs is irrelevant.

_P54

Generalization

The Hindley-Milner type system assigns types to a let-expression in two stages:

1. The declaration groups are considered in dependency order. For each group, a type with no universal quantification is inferred for each variable bound in the group. Then, all type variables that occur in these types are universally quantified unless they are associated with bound variables in the type environment; this is called generalization.
2. Finally, the body of the let-expression is typed.

For example, consider the declaration

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

The type of g’s definition is a → (a, a). The generalization step attributes to g the polymorphic type ∀ a. a → (a, a), after which the typing of the “...” part can proceed.

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 types of the definitions of g1 and g2 are both a → a → String, and the accumulated constraints are Ord a (arising from the use of >), and Show a (arising from the use of show). The type variables appearing in this collection of constraints are called the constrained type variables.

The generalization step attributes to both g1 and g2 the type

∀ a. (Ord a, Show a) ⇒ a → a → String

_P54

Context reduction

The context of a type may constrain only a type variable, or the application of a type variable to one or more types. Hence, types produced by generalization must be expressed in a form in which all context constraints have be reduced to this “head normal form”. Consider, for example, the definition:

f xs y = xs == [y]

Its type is given by f :: Eq a => [a] -> a -> Bool and not f :: Eq [a] => [a] -> a -> Bool. Even though the equality is taken at the list type, the context must be simplified, using the instance declaration for Eq on lists, before generalization. If no such instance is in scope, a static error occurs.

The instance declaration derived from a data type deriving clause must, like any instance declaration, have a simple context; that is, all the constraints must be of the form C a, where a is a type variable.

For example, in the type

data Apply a b = App (a b) deriving Show

the derived Show instance will produce a context Show (a b), which cannot be reduced and is not simple; thus a static error results.

_P55

Monomorphism

Sometimes it is not possible to generalize over all the type variables used in the type of the definition. For example, consider the declaration

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

In an environment where x has type a, the type of g’s definition is a → b → ([a], b). The generalization step attributes to g the type ∀ b. a → b → ([a], b); only b can be universally quantified because a occurs in the type environment. We say that the type of g is monomorphic in the type variable a.

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)

which would, incidentally, force x to have type Bool, but invalid for it to be

(g True, g ’c’)

In general, a type ∀ u. cx ⇒ t is said to be monomorphic in the type variable a if a is free in ∀ u. cx ⇒ t.

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

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

because that would claim that g was polymorphic in both a and b. In this program, g can only be given a type signature if its first argument is restricted to a type not involving type variables; for example

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

This signature would also cause x to have type Int.

_P56

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. The following two rules define the monomorphism restriction:

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 that is bound by simple pattern binding.

The usual Hindley-Milner restriction on polymorphism is that only type variables that do not occur 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.)

Rule 2. Any monomorphic type variables that remain when type inference for an entire module is complete, are considered ambiguous, and are resolved to particular types using the defaulting rules.

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

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

Now consider the following expression:

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

It looks as if len should be computed only once, but without Rule 1 it might be computed twice, once at each of two different overloadings. If the programmer does actually wish the computation to be repeated, an explicit type signature may be added:

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

(2) Rule 1 prevents ambiguity. For example, consider the declaration group

[(n,s)] = reads t

Recall that reads is a standard function whose type is given by the signature

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

Without Rule 1, n would be assigned the type ∀ a. Read a ⇒ a and s the type ∀ a. Read a ⇒ String. The latter is an invalid type, because it is inherently ambiguous. It is not possible to determine at what overloading to use s, nor can this be solved by adding a type signature for s. Hence, when non-simple pattern bindings are used, the types inferred are always monomorphic in their constrained type variables, irrespective of whether a type signature is provided. In this case, both n and s are monomorphic in a.

The same constraint applies to pattern-bound functions. For example, in

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

both f and g are monomorphic regardless of any type signatures supplied for f or g.

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. Rule 2 states that the exact types of all the variables bound in a module must be determined by that module alone, and not by any modules that import it.

module M1(len1) where 
  default( Int, Double ) 
  len1 = genericLength "Hello"

module M2 where 
  import M1(len1) 
  len2 = (2 * len1) :: Rational

When type inference on module M1 is complete, len1 has the monomorphic type Num a => a (by Rule 1). Rule 2 now states that the monomorphic type variable a is ambiguous, and must be resolved using the defaulting rules. Hence, len1 gets type Int, and its use in len2 is type-incorrect. (If the above code is actually what is wanted, a type signature on len1 would solve the problem.)

_P56~P58

Consequences

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

the function f may be used at any overloading in class Num. There is no danger of recomputation here. However, the same function defined with pattern syntax:

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

requires a type signature if f is to be fully overloaded. Many functions are most naturally defined using simple pattern bindings; the user must be careful to affix these with type signatures to retain full overloading.

The standard prelude contains many examples of this:

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

Rule 1 applies to both top-level and nested definitions. Consider

module M where 
  len1 = genericLength "Hello" 
  len2 = (2 * len1) :: Rational

Here, type inference finds that len1 has the monomorphic type (Num a => a); and the type variable a is resolved to Rational when performing type inference on len2.

_P58

Reference

Haskell 2010 Language Report