summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--docs/users_guide/exts/let_generalisation.rst85
1 files changed, 35 insertions, 50 deletions
diff --git a/docs/users_guide/exts/let_generalisation.rst b/docs/users_guide/exts/let_generalisation.rst
index d966579377..c6de6454aa 100644
--- a/docs/users_guide/exts/let_generalisation.rst
+++ b/docs/users_guide/exts/let_generalisation.rst
@@ -11,72 +11,57 @@ Let-generalisation
Infer less polymorphic types for local bindings by default.
-An ML-style language usually generalises the type of any ``let``\-bound or
-``where``\-bound variable, so that it is as polymorphic as possible. With the
-extension :extension:`MonoLocalBinds` GHC implements a slightly more conservative
-policy, using the following rules:
+An ML-style language usually generalises the type of any let-bound or where-bound variable, so that it is as polymorphic as possible. With the extension :extension:`MonoLocalBinds` GHC implements a slightly more conservative policy, for reasons descibed in Section 4.2 of `"OutsideIn(X): Modular type inference with local assumptions”<https://www.microsoft.com/en-us/research/publication/outsideinx-modular-type-inference-with-local-assumptions/>`__,
+and a `related blog post
+<https://www.haskell.org/ghc/blog/20100930-LetGeneralisationInGhc7.html>`__.
-- A *binding group* is a strongly-connected component in the graph in which the nodes are let-bindings,
- and there is an edge from a let-binding B to the binding for each of the free variables in B's RHS.
- Before computing the strongly-connected components, any dependencies from variables with
- complete type signatures are removed.
+The extension :extension:`MonoLocalBinds` is implied by :extension:`TypeFamilies`
+and :extension:`GADTs`. You can switch it off again with
+:extension:`NoMonoLocalBinds <MonoLocalBinds>` but type inference becomes
+less predictable if you do so. (Read the paper!)
-- With :extension:`MonoLocalBinds`, a binding group is *generalised* if and only if
+To a first approximation, with :extension:`MonoLocalBinds` *top-level bindings are
+generalised, but local (i.e. nested) bindings are not*. The idea is
+that, at top level, the type environment has no free type variables,
+and so the difficulties described in these papers do not arise. But
+GHC implements a slightly more complicated rule, for two reasons:
- - Each of its free variables (excluding the variables bound by the group itself)
- is either *imported* or *closed* (see next bullet), or
+* The Monomorphism Restriction can cause even top-level bindings not to be generalised, and hence even the top-level type environment can have free type variables.
+* For stylistic reasons, programmers sometimes write local bindings that make no use of local variables, so the binding could equally well be top-level. It seems reasonable to generalise these.
- - Any of its binders has a partial type signature (see :ref:`partial-type-signatures`).
- Adding a partial type signature ``f :: _``, (or, more generally, ``f :: _ => _``)
- provides a per-binding way to ask GHC to
- perform let-generalisation, even though :extension:`MonoLocalBinds` is on.
+So here are the exact rules used by MonoLocalBinds.
+With MonoLocalBinds, a binding group will be *generalised* if and only if
- NB: even if the binding is generalised, it may still be affected by the
- monomorphism restriction, which reduces generalisation
- (`Haskell Report, Section 4.5.5 <http://www.haskell.org/onlinereport/decls.html#sect4.5.5>`__)
+* Each of its free variables (excluding the variables bound by the group itself) is closed (see next bullet), or
+* Any of its binders has a partial type signature (see Partial Type Signatures). Adding a partial type signature ``f :: _``, (or, more generally, ``f :: _ => _``) provides a per-binding way to ask GHC to perform let-generalisation, even though MonoLocalBinds is on.
-- A variable is *closed* if and only if
- - the variable is let-bound, and
+A variable ``f`` is called *closed* if and only if
- - one of the following holds:
+* The variable ``f`` is imported from another module, or
- - the variable has an explicit, complete (i.e. not partial) type signature
- that has no free type variables, or
+* The variable ``f`` is let-bound, and one of the following holds:
+ * ``f`` has an explicit, complete (i.e. not partial) type signature that has no free type variables, or
+ * its binding group is generalised over all its free type variables, so that ``f``'s type has no free type variables.
- - its binding group is fully generalised, so it has a closed type
+The key idea is that: *if a variable is closed, then its type definitely has no free type variables*.
- Note that a signature like ``f :: a -> a`` is equivalent to ``f :: forall a. a->a``,
- assuming ``a`` is not in scope, and hence is closed.
+Note that:
+* A signature like f :: a -> a is equivalent to ``f :: forall a. a -> a``, assuming ``a`` is not in scope. Hence ``f`` is closed, since it has a complete type signature with no free variables.
-For example, consider ::
+* Even if the binding is generalised, it may not be generalised over all its free type variables, either because it mentions locally-bound variables, or because of the monomorphism restriction (Haskell Report, Section 4.5.5)
- f x = x + 1
- g x = let h y = f y * 2
- k z = z+x
- in h x + k x
+Example 1 ::
-Here ``f`` is generalised because it has no free variables; and its
-binding group is unaffected by the monomorphism restriction; and hence
-``f`` is closed. The same reasoning applies to ``g``, except that it has
-one closed free variable, namely ``f``. Similarly ``h`` is closed, *even
-though it is not bound at top level*, because its only free variable
-``f`` is closed. But ``k`` is not closed, because it mentions ``x``
-which is not closed (because it is not let-bound).
+ f1 x = x+1
+ f2 y = f1 (y*2)
-Notice that a top-level binding that is affected by the monomorphism
-restriction is not closed, and hence may in turn prevent generalisation
-of bindings that mention it.
+``f1`` has free variable ``(+)``, but it is imported and hence closd. So ``f1``'s binding is generalised. As a result, its type ``f1 :: forall a. Num a => a -> a`` has no free type variables, so ``f1`` is closed. Hence ``f2``'s binding is generalised (since its free variables, ``f1`` and ``(*)`` are both closed).
-The rationale for this more conservative strategy is given in `the
-papers <https://www.microsoft.com/en-us/research/wp-content/uploads/2016/02/jfp-outsidein.pdf>`__
-"Let should not be generalised" and "Modular type inference with local
-assumptions", and a related `blog post
-<https://www.haskell.org/ghc/blog/20100930-LetGeneralisationInGhc7.html>`__.
+These comments apply whether the bindings for ``f1`` and ``f2`` are at top level or nested.
-The extension :extension:`MonoLocalBinds` is implied by :extension:`TypeFamilies`
-and :extension:`GADTs`. You can switch it off again with
-:extension:`NoMonoLocalBinds <MonoLocalBinds>` but type inference becomes
-less predictable if you do so. (Read the papers!)
+Example 2 ::
+ f3 x = let g y = x+y in ....
+The binding for ``g`` has a free variable ``x`` that is lambda-bound, and hence not closed. So ``g``\'s binding is not generalised.