diff options
| -rw-r--r-- | docs/users_guide/exts/let_generalisation.rst | 85 |
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. |