[Git][ghc/ghc][wip/int-index/rta-docs] docs: update information on RequiredTypeArguments
Vladislav Zavialov (@int-index)
gitlab at gitlab.haskell.org
Fri Dec 8 21:39:36 UTC 2023
Vladislav Zavialov pushed to branch wip/int-index/rta-docs at Glasgow Haskell Compiler / GHC
Commits:
05eba21b by Vladislav Zavialov at 2023-12-09T00:39:24+03:00
docs: update information on RequiredTypeArguments
Update the User's Guide and Release Notes to account for the recent
progress in the implementation of RequiredTypeArguments.
- - - - -
3 changed files:
- docs/users_guide/9.10.1-notes.rst
- docs/users_guide/exts/required_type_arguments.rst
- docs/users_guide/using-warnings.rst
Changes:
=====================================
docs/users_guide/9.10.1-notes.rst
=====================================
@@ -6,17 +6,33 @@ Version 9.10.1
Language
~~~~~~~~
-- Part 1 of GHC Proposal `#281
- <https://github.com/ghc-proposals/ghc-proposals/blob/master/proposals/0281-visible-forall.rst>`_
- "Visible forall in types of terms" has been implemented.
+- GHC Proposal `#281 <https://github.com/ghc-proposals/ghc-proposals/blob/master/proposals/0281-visible-forall.rst>`_
+ "Visible forall in types of terms" has been partially implemented.
The following code is now accepted by GHC::
- idv :: forall a -> a -> a
- idv (type a) (x :: a) = x
+ {-# LANGUAGE RequiredTypeArguments #-}
- x = idv (type Int) 42
+ vshow :: forall a -> Show a => a -> String
+ vshow t x = show (x :: t)
- This feature is guarded behind :extension:`RequiredTypeArguments` and :extension:`ExplicitNamespaces`.
+ s1 = vshow Int 42 -- "42"
+ s2 = vshow Double 42 -- "42.0"
+
+ The use of ``forall a ->`` instead of ``forall a.`` indicates a *required* type
+ argument. A required type argument is visually indistinguishable from a value
+ argument but does not exist at runtime.
+
+ This feature is guarded behind :extension:`RequiredTypeArguments`.
+
+- The :extension:`ExplicitNamespaces` extension can now be used in conjunction
+ with :extension:`RequiredTypeArguments` to select the type namespace in a
+ required type argument::
+
+ data T = T -- the name `T` is ambiguous
+ f :: forall a -> ... -- `f` expects a required type argument
+
+ x1 = f T -- refers to the /data/ constructor `T`
+ x2 = f (type T) -- refers to the /type/ constructor `T`
- Due to an oversight, previous GHC releases (starting from 9.4) allowed the use
of promoted data types in kinds, even when :extension:`DataKinds` was not
=====================================
docs/users_guide/exts/required_type_arguments.rst
=====================================
@@ -19,42 +19,83 @@ dependent quantification in types of terms::
id :: forall a. a -> a -- invisible dependent quantification
id_vdq :: forall a -> a -> a -- visible dependent quantification
-Note that the arrow in ``forall a ->`` is part of the syntax and not a function
-arrow, just like the dot in ``forall a.`` is not a type operator. The essence of
-a ``forall`` is the same regardless of whether it is followed by a dot or an
-arrow: it introduces a type variable. But the way we bind and specify this type
-variable at the term level differs.
+The arrow in ``forall a ->`` is part of the syntax and not a function arrow,
+just like the dot in ``forall a.`` is not a type operator.
-When we define ``id``, we can use a lambda to bind a variable that stands for
-the function argument::
+The choice between ``forall a.`` and ``forall a ->`` does not have any effect on
+program execution. Both quantifiers introduce type variables, which are erased
+during compilation. Rather, the main difference is in the syntax used at call
+sites::
- -- For reference: id :: forall a. a -> a
- id = \x -> x
+ x1 = id True -- invisible forall, the type argument is inferred by GHC
+ x2 = id @Bool True -- invisible forall, the type argument is supplied by the programmer
-At the same time, there is no mention of ``a`` in this definition at all. It is
-bound by the compiler behind the scenes, and that is why we call the ordinary
-``forall a.`` an *invisible* quantifier. Compare that to ``forall a ->``, which
-is considered *visible*::
+ x3 = id_vdq _ True -- visible forall, the type argument is inferred by GHC
+ x4 = id_vdq Bool True -- visible forall, the type argument is supplied by the programmer
- -- For reference: id_vdq :: forall a -> a -> a
- id_vdq = \(type t) x -> x
+Terminology: Dependent quantifier
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-This time we have two binders in the lambda:
-* ``type t``, corresponding to ``forall a ->`` in the signature
-* ``x``, corresponding to ``a ->`` in the signature
+Both ``forall a.`` and ``forall a ->`` are said to be dependent because the
+result type depends on the supplied type argument: ::
+
+ id @Integer :: Integer -> Integer
+ id @String :: String -> String
+
+ id_vdq Integer :: Integer -> Integer
+ id_vdq String :: String -> String
+
+Notice how the RHS of the signature is influenced by the LHS.
+
+This is in contrast to the function arrow ``->``, which is a non-dependent
+quantifier::
+
+ putStrLn "Hello" :: IO ()
+ putStrLn "World" :: IO ()
+
+The type of ``putStrLn`` is ``String -> IO ()``. No matter what string we pass
+as input, the result type ``IO ()`` does not depend on it.
+
+This notion of dependence is weaker than the one used in dependently-typed
+languages. Neither ``forall a.`` nor ``forall a ->`` constitute a dependent function.
+
+Terminology: Visible quantifier
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+
+We say that ``forall a.`` is an *invisible* quantifier and ``forall a ->`` is a
+*visible* quantifier. This might not be obvious at first, as the
+quantifiers themselves are clearly visible to our eye.
+
+The property actually describes whether GHC expects the type argument to be
+supplied visibly at call sites::
+
+ b1 = id True -- there is a hidden, invisible type argument `Bool`
+ b2 = id_vdq Bool True -- there is a visible type argument `Bool` in the source code
+
+A similar difference exists at definition sites. The function equation for
+``id`` does not mention any type variables::
+
+ id :: forall a. a -> a
+ id x = x -- the type variable `a` is not bound in the equation
+
+There is just one binder, ``x``, and it corresponds to the value argument, not
+to the type argument. Compare that with the function equation for ``id_vdq``::
+
+ id_vdq :: forall a -> a -> a
+ id_vdq t x = x
-And of course, now we also have the option of using the bound ``t`` in a
-subsequent pattern, as well as on the right-hand side of the lambda::
+This time we have two binders on the LHS:
- -- For reference: id_vdq :: forall a -> a -> a
- id_vdq = \(type t) (x :: t) -> x :: t
- -- ↑ ↑ ↑
- -- bound used used
+* ``t``, corresponding to ``forall a ->`` in the signature
+* ``x``, corresponding to ``a ->`` in the signature
-At use sites, we also instantiate this type variable explicitly::
+The bound ``t`` can be used in subsequent patterns, as well as on the right-hand
+side of the equation::
- n = id_vdq (type Integer) 42
- s = id_vdq (type String) "Hello"
+ id_vdq :: forall a -> a -> a
+ id_vdq t (x :: t) = x :: t
+ -- ↑ ↑ ↑
+ -- bound used used
Relation to :extension:`TypeApplications`
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
@@ -70,12 +111,12 @@ not reflected syntactically in the expression, it is invisible unless we use a
Required type arguments are compulsory. They must appear syntactically at call
sites::
- x1 = id_vdq (type Bool) True -- OK
- x2 = id_vdq True -- not OK
+ x1 = id_vdq Bool True -- OK
+ x2 = id_vdq True -- not OK
You may use an underscore to infer a required type argument::
- x3 = id_vdq (type _) True -- OK
+ x3 = id_vdq _ True -- OK
That is, it is mostly a matter of syntax whether to use ``forall a.`` with type
applications or ``forall a ->``. One advantage of required type arguments is that
@@ -92,20 +133,199 @@ With :extension:`RequiredTypeArguments`, we can imagine a slightly different API
sizeOf :: forall a -> Storable a => Int
-If ``sizeOf`` had this type, we could write ``sizeOf (type Bool)`` without
+If ``sizeOf`` had this type, we could write ``sizeOf Bool`` without
passing a dummy value.
+Required type arguments are erased during compilation. While the source program
+appears to bind and pass required type arguments alongside value arguments, the
+compiled program does not. There is no runtime overhead associated with required
+type arguments relative to the usual, invisible type arguments.
+
Relation to :extension:`ExplicitNamespaces`
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-The ``type`` keyword that we used in the examples is not actually part of
-:extension:`RequiredTypeArguments`. It is guarded behind
-:extension:`ExplicitNamespaces`. As described in the proposal, required type
-arguments can be passed without a syntactic marker, making them syntactically
-indistinguishble from ordinary function arguments::
+A required type argument is syntactically indistinguishable from a value
+argument. In a function call ``f arg1 arg2 arg3``, it is impossible to tell,
+without looking at the type of ``f``, which of the three arguments are required
+type arguments, if any.
+
+At the same time, one of the design goals of GHC is to be able to perform name
+resolution (find the binding sites of identifiers) without involving the type
+system. Consider: ::
+
+ data Ty = Int | Double | String deriving Show
+ main = print Int
+
+In this example, there are two constructors named ``Int`` in scope:
+
+* The **type constructor** ``Int`` of kind ``Type`` (imported from ``Prelude``)
+* The **data constructor** ``Int`` of type ``Ty`` (defined locally)
+
+How does the compiler or someone reading the code know that ``print Int`` is
+supposed to refer to the data constructor, not the type constructor? In GHC,
+this is resolved as follows. Each identifier is said to occur either in
+**type syntax** or **term syntax**, depending on the surrounding syntactic
+context::
+
+ -- Examples of X in type syntax
+ type T = X -- RHS of a type synonym
+ data D = MkD X -- field of a data constructor declaration
+ a :: X -- RHS of a type signature
+ b = f (c :: X) -- RHS of a type signature (in expressions)
+ f (x :: X) = x -- RHS of a type signature (in patterns)
+
+ -- Examples of X in term syntax
+ c X = a -- LHS of a function equation
+ c a = X -- RHS of a function equation
+
+One could imagine the entire program "zoned" into type syntax and term syntax,
+each zone having its own rules for name resolution:
+
+* In type syntax, type constructors take precedence over data constructors.
+* In term syntax, data constructors take precedence over type constructors.
+
+This means that in the ``print Int`` example, the data constructor is selected
+solely based on the fact that the ``Int`` occurs in term syntax. This is firmly
+determined before GHC attempts to type-check the expression, so the type of
+``print`` does not influence which of the two ``Int``\s is passed to it.
+
+This may not be the desired behavior in a required type argument. Consider::
+
+ vshow :: forall a -> Show a => a -> String
+ vshow t x = show (x :: t)
+
+ s1 = vshow Int 42 -- "42"
+ s2 = vshow Double 42 -- "42.0"
+
+The function calls ``vshow Int 42`` and ``vshow Double 42`` are written in
+*term* syntax, while the intended referents of ``Int`` and ``Double`` are the
+respective *type* constructors. As long as there are no data constructors named
+``Int`` or ``Double`` in scope, the example works as intended. However, if such
+clashing constructor names are introduced, they may disrupt name resolution::
+
+ data Ty = Int | Double | String
+
+ vshow :: forall a -> Show a => a -> String
+ vshow t x = show (x :: t)
+
+ s1 = vshow Int 42 -- error: Expected a type, but ‘Int’ has kind ‘Ty’
+ s2 = vshow Double 42 -- error: Expected a type, but ‘Double’ has kind ‘Ty’
+
+In this example the intent was to refer to ``Int`` and ``Double`` as types, but
+the names were resolved in favor of data constructors, resulting in type errors.
+
+The example can be fixed with the help of :extension:`ExplicitNamespaces`, which
+allows embedding type syntax into term syntax using the ``type`` keyword::
+
+ s1 = vshow (type Int) 42
+ s2 = vshow (type Double) 42
+
+A similar problem occurs with list and tuple syntax. In type syntax, ``[a]`` is
+the type of a list, i.e. ``Data.List.List a``. In term syntax, ``[a]`` is a
+singleton list, i.e. ``a : []``. A naive attempt to use the list type as a
+required type argument will result in a type error::
+
+ s3 = vshow [Int] [1,2,3] -- error: Expected a type, but ‘[Int]’ has kind ‘[Type]’
+
+The problem is that GHC assumes ``[Int]`` to stand for ``Int : []`` instead of
+the intended ``Data.List.List Int``. This, too, can be solved using the ``type`` keyword::
+
+ s3 = vshow (type [Int]) [1,2,3]
+
+Since the ``type`` keyword is merely a namespace disambiguation mechanism, it
+need not apply to the entire type argument. Using it to disambiguate only a part
+of the type argument is also valid::
+
+ f :: forall a -> ... -- `f`` is a function that expects a required type argument
+
+ r1 = f (type (Either () Int)) -- `type` applied to the entire type argument
+ r2 = f (Either (type ()) Int) -- `type` applied to one part of it
+ r3 = f (Either (type ()) (type Int)) -- `type` applied to multiple parts
+
+That is, the expression ``Either (type ()) (type Int)`` does *not* indicate that
+``Either`` is applied to two type arguments; rather, the entire expression is a
+single type argument and ``type`` is used to disambiguate parts of it.
+
+Outside a required type argument, it is illegal to use ``type``:
+::
+
+ r4 = type Int -- illegal use of ‘type’
+
+Finally, there are types that require the ``type`` keyword only due to
+limitations of the current implementation::
+
+ a1 = f (type (Int -> Bool)) -- function type
+ a2 = f (type (Read T => T)) -- constrained type
+ a3 = f (type (forall a. a)) -- universally quantified type
+ a4 = f (type (forall a. Read a => String -> a)) -- a combination of the above
+
+This restriction will be relaxed in a future release of GHC.
+
+Effect on implicit quantification
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+
+Implicit quantification is said to occur when GHC inserts an implicit ``forall``
+to bind type variables::
+
+ const :: a -> b -> a -- implicit quantification
+ const :: forall a b. a -> b -> a -- explicit quantification
+
+Normally, implicit quantification is unaffected by term variables in scope:
+::
+ f a = ... -- the LHS binds `a`
+ where const :: a -> b -> a
+ -- implicit quantification over `a` takes place
+ -- despite the `a` bound on the LHS of `f`
+
+When :extension:`RequiredTypeArguments` is in effect, names bound in term syntax
+are not implicitly quantified. This allows us to accept the following example: ::
+
+ readshow :: forall a -> (Read a, Show a) => String -> String
+ readshow t s = show (read s :: t)
+
+ s1 = readshow Int "42" -- "42"
+ s2 = readshow Double "42" -- "42.0"
+
+Note how ``t`` is bound on the LHS of a function equation (term syntax), and
+then used in a type annotation (type syntax). Under the usual rules for implicit
+quantification, the ``t`` would have been implicitly quantified: ::
+
+ -- RequiredTypeArguments
+ readshow t s = show (read s :: t) -- the `t` is captured
+ -- ↑ ↑
+ -- bound used
+
+ -- NoRequiredTypeArguments
+ readshow t s = show (read s :: t) -- the `t` is implicitly quantified as follows:
+ readshow t s = show (read s :: forall t. t)
+ -- ↑ ↑ ↑
+ -- bound bound used
+
+On the one hand, taking the current scope into account allows us to accept
+programs like the one above. On the other hand, some existing programs will no
+longer compile: ::
+
+ a = 42
+ f :: a -> a -- RequiredTypeArguments: the top-level `a` is captured
+
+Because of that, merely enabling :extension:`RequiredTypeArguments` might lead
+to type errors of this form::
+
+ Term variable ‘a’ cannot be used here
+ (term variables cannot be promoted)
+
+There are two possible ways to fix this error::
+
+ a = 42
+ f1 :: b -> b -- (1) use a different variable name
+ f2 :: forall a. a -> a -- (2) use an explicit forall
- n = id_vdq Integer 42
+If you are converting a large codebase to be compatible with
+:extension:`RequiredTypeArguments`, consider using
+:ghc-flag:`-Wterm-variable-capture` during the migration. It is a warning that
+detects instances of implicit quantification incompatible with
+:extension:`RequiredTypeArguments`: ::
-In this example we pass ``Integer`` as opposed to ``(type Integer)``.
-This means that :extension:`RequiredTypeArguments` is not tied to the ``type``
-syntax, which belongs to :extension:`ExplicitNamespaces`.
\ No newline at end of file
+ The type variable ‘a’ is implicitly quantified,
+ even though another variable of the same name is in scope:
+ ‘a’ defined at ...
\ No newline at end of file
=====================================
docs/users_guide/using-warnings.rst
=====================================
@@ -2441,21 +2441,17 @@ of ``-W(no-)*``.
:since: 9.8.1
- In accordance with `GHC Proposal #281
- <https://github.com/ghc-proposals/ghc-proposals/blob/master/proposals/0281-visible-forall.rst>`__,
- a new extension ``RequiredTypeArguments`` will be introduced in a future GHC release.
-
- Under ``RequiredTypeArguments``, implicit quantification of type variables does not take place
+ Under :extension:`RequiredTypeArguments`, implicit quantification of type variables does not take place
if there is a term variable of the same name in scope.
For example: ::
a = 15
- f :: a -> a -- Does ‘a’ refer to the term-level binding
- -- or is it implicitly quantified?
+ f :: a -> a -- NoRequiredTypeArguments: The ‘a’ is implicitly quantified
+ -- RequiredTypeArguments: The ‘a’ refers to the term-level binding
When :ghc-flag:`-Wterm-variable-capture` is enabled, GHC warns against implicit quantification
- that would stop working under ``RequiredTypeArguments``.
+ that would stop working under :extension:`RequiredTypeArguments`.
.. ghc-flag:: -Wmissing-role-annotations
:shortdesc: warn when type declarations don't have role annotations
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/05eba21bc16362174e8320884b1d468db9d61fc7
--
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/05eba21bc16362174e8320884b1d468db9d61fc7
You're receiving this email because of your account on gitlab.haskell.org.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/ghc-commits/attachments/20231208/f0d38976/attachment-0001.html>
More information about the ghc-commits
mailing list