diff options
Diffstat (limited to 'docs')
| -rw-r--r-- | docs/users_guide/9.2.1-notes.rst | 11 | ||||
| -rw-r--r-- | docs/users_guide/exts/impredicative_types.rst | 59 | ||||
| -rw-r--r-- | docs/users_guide/ghci.rst | 29 |
3 files changed, 46 insertions, 53 deletions
diff --git a/docs/users_guide/9.2.1-notes.rst b/docs/users_guide/9.2.1-notes.rst index bdc0271e6f..516bf36563 100644 --- a/docs/users_guide/9.2.1-notes.rst +++ b/docs/users_guide/9.2.1-notes.rst @@ -3,6 +3,17 @@ Version 9.2.1 ============== +Language +~~~~~~~~ + +* :extension:`ImpredicativeTypes`: Finally, polymorphic types have become first class! + GHC 9.2 includes a full implementation of the Quick Look approach to type inference for + impredicative types, as described in in the paper + `A quick look at impredicativity + <https://www.microsoft.com/en-us/research/publication/a-quick-look-at-impredicativity/>`__ + (Serrano et al, ICFP 2020). More information here: :ref:`impredicative-polymorphism`. + This replaces the old (undefined, flaky) behaviour of the :extension:`ImpredicativeTypes` extension. + Compiler ~~~~~~~~ diff --git a/docs/users_guide/exts/impredicative_types.rst b/docs/users_guide/exts/impredicative_types.rst index 2380526fb6..01d6476923 100644 --- a/docs/users_guide/exts/impredicative_types.rst +++ b/docs/users_guide/exts/impredicative_types.rst @@ -25,33 +25,32 @@ instantiate ``id``\'s type with ``b := (forall s. ST s a) -> a``, and that is not allowed. Instantiating polymorphic type variables with polymorphic types is called *impredicative polymorphism*. -GHC has extremely flaky support for *impredicative polymorphism*, -enabled with :extension:`ImpredicativeTypes`. If it worked, this would mean -that you *could* call a polymorphic function at a polymorphic type, and -parameterise data structures over polymorphic types. For example: :: - - f :: Maybe (forall a. [a] -> [a]) -> Maybe ([Int], [Char]) - f (Just g) = Just (g [3], g "hello") - f Nothing = Nothing - -Notice here that the ``Maybe`` type is parameterised by the -*polymorphic* type ``(forall a. [a] -> [a])``. However *the extension -should be considered highly experimental, and certainly un-supported*. -You are welcome to try it, but please don't rely on it working -consistently, or working the same in subsequent releases. See -:ghc-wiki:`this wiki page <impredicative-polymorphism>` for more details. - -If you want impredicative polymorphism, the main workaround is to use a -newtype wrapper. The ``id runST`` example can be written using this -workaround like this: :: - - runST :: (forall s. ST s a) -> a - id :: forall b. b -> b - - newtype Wrap a = Wrap { unWrap :: (forall s. ST s a) -> a } - - foo :: (forall s. ST s a) -> a - foo = unWrap (id (Wrap runST)) - -- Here id is called at monomorphic type (Wrap a) - - +GHC has robust support for *impredicative polymorphism*, +enabled with :extension:`ImpredicativeTypes`, using the so-called Quick Look +inference algorithm. It is described in the paper +`A quick look at impredicativity +<https://www.microsoft.com/en-us/research/publication/a-quick-look-at-impredicativity/>`__ +(Serrano et al, ICFP 2020). + +Switching on :extension:`ImpredicativeTypes` + +- Switches on :extension: `RankNTypes` + +- Allows user-written types to have foralls under type constructors, not just under arrows. + For example ``f :: Maybe (forall a. [a] -> [a])`` is a legal type signature. + +- Allows polymorphic types in Visible Type Application + (when :extension: `TypeApplications` is enabled). For example, you + can write ``reverse @(forall b. b->b) xs``. Using VTA with a + polymorphic type argument is useful in cases when Quick Look cannot + infer the correct instantiation. + +- Switches on the Quick Look type inference algorithm, as described + in the paper. This allows the compiler to infer impredicative instantiations of polymorphic + functions in many cases. For example, ``reverse xs`` will typecheck even if ``xs :: [forall a. a->a]``, + by instantiating ``reverse`` at type ``forall a. a->a``. + +For many years GHC has a special case for the function ``($)``, that allows it +to typecheck an application like ``runST $ (do { ... })``, even though that +instantiation may be impredicative. This special case remains: even without +:extension:`ImpredicativeTypes` GHC switches on Quick Look for applications of ``($)``. diff --git a/docs/users_guide/ghci.rst b/docs/users_guide/ghci.rst index d5a2083eab..92dc51e00f 100644 --- a/docs/users_guide/ghci.rst +++ b/docs/users_guide/ghci.rst @@ -2951,37 +2951,20 @@ commonly used commands. .. ghci-cmd:: :type; ⟨expression⟩ - Infers and prints the type of ⟨expression⟩, including explicit - forall quantifiers for polymorphic types. - The type reported is the type that would be inferred - for a variable assigned to the expression, but without the - monomorphism restriction applied. + Infers and prints the type of ⟨expression⟩. For polymorphic types + it instantiates the 'inferred' forall quantifiers (but not the + 'specified' ones; see :ref:`inferred-vs-specified`), solves constraints, and re-generalises. .. code-block:: none *X> :type length length :: Foldable t => t a -> Int -.. ghci-cmd:: :type +v; ⟨expression⟩ - - Infers and prints the type of ⟨expression⟩, but without fiddling - with type variables or class constraints. This is useful when you - are using :extension:`TypeApplications` and care about the distinction - between specified type variables (available for type application) - and inferred type variables (not available). This mode sometimes prints - constraints (such as ``Show Int``) that could readily be solved, but - solving these constraints may affect the type variables, so GHC refrains. - - .. code-block:: none - - *X> :set -fprint-explicit-foralls - *X> :type +v length - length :: forall (t :: * -> *). Foldable t => forall a. t a -> Int - .. ghci-cmd:: :type +d; ⟨expression⟩ - Infers and prints the type of ⟨expression⟩, defaulting type variables - if possible. In this mode, if the inferred type is constrained by + Infers and prints the type of ⟨expression⟩, instantiating *all* the forall + quantifiers, solving constraints, defaulting, and generalising. + In this mode, if the inferred type is constrained by any interactive class (``Num``, ``Show``, ``Eq``, ``Ord``, ``Foldable``, or ``Traversable``), the constrained type variable(s) are defaulted according to the rules described under :extension:`ExtendedDefaultRules`. |