wiki:NoMonomorphismRestriction

Version 3 (modified by igloo, 4 years ago) (diff)

--

Proposal: NoMonomorphismRestriction

Ticket #131
Dependencies none
Related MonoPatBinds, alternative monomorphism restriction replacement options

Compiler support

GHC full (-XNoMonomorphismRestriction -XNoMonoPatBinds)
nhc98 full (doesn't support the monomorphism restriction)
Hugs none, but has a "Different implementation of the monomorphism restriction for top-level bindings"
UHC full (doesn't support the monomorphism restriction)
JHC none?
LHC full (-XNoMonomorphismRestriction -XNoMonoPatBinds)

Summary

Remove the monomorphism restriction. Bindings are polymorphic unless constrained by a type signature.

Description

The monomorphism is a frequent source of confusion to Haskell programmers the first times they are caught by it. It is widely regarded as an ugly part of the language. Arguments for removing it include:

  • Removes a wart from the language
  • Many implementations don't implement it, or implement it incorrectly, and users haven't found any significant problems as a result
  • "As much polymorphism as possible" is in the spirit of Haskell - it is strange to limit polymorphism for performance reasons (indeed, this is arguably a poor compromise)
  • It turns out to be quite hard to demonstrate a performance problem due to the M-R, at least with GHC, because its optimiser often recovers the sharing.
  • Even if you do get loss of sharing, profiling will quickly pinpoint it
  • Haskell doesn't specify an evaluation strategy so introducing the concept of 'sharing' is strange indeed.

There have been 4 other suggestions related to the monomorphism restriction:

Add a monomorphic `:=` operator
Use redundant parens to indicate a monomorphic binding

Both of these imply removing the monomorphism restriction for normal bindings. They would be separate proposals that depend on this one. While it would be nice, if we decide to implement one of these, to do so at the same time as implementing NoMonomorphismRestriction, it is not necessary.

Enable the monomorphism restriction on a per module basis

This is an alternative to this proposal. If the monomorphism restriction was on by default, then it would not solve the confusion problems, as people unfamiliar with it would not know to turn it off. If it was off by default, then people would need to realise that they need to turn it on, at which point adding type signatures instead would make it clearer what is going on.

Bindings are monomorphic unless constrained by a type signature

Seems against the spirit of Haskell. But see Let should not be generalised which argues the case for this approach, at least for nested bindings.

Opposition

In the discussion on the mailing list, Simon Peyton Jones wrote:

As many of you will know I am now leaning strongly towards doing no generalisation whatsoever on nested bindings. See http://research.microsoft.com/~simonpj/papers/constraints/index.htm

So I'd cut the cake differently:

  • top level: generalise, no monomorphism restriction
  • nested: do not generalise, monomorphism restriction for every binding

References

None.

Report Delta

In Section 4.5.5 remove:

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.3).

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 (Section 4.4.3.2), 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; see Section 4.5.2.)

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 (Section 4.3.4).

Motivation

Rule 1 is required for two reasons, both of which are fairly subtle.

  • Rule 1 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
    
    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)
    
  • 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 forall a. Read a =>a and s the type forall 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 (Section 4.4.3.2), 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 of Section 4.3.4. 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.)

This issue does not arise for nested bindings, because their entire scope is visible to the compiler.

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.

In Section 5 replace:

(There are two minor exceptions to this statement. First, default declarations scope over a single module (Section 4.3.4). Second, Rule 2 of the monomorphism restriction (Section 4.5.5) is affected by module boundaries. )

with:

(There is a minor exception to this statement: Default declarations scope over a single module (Section 4.3.4).)