[Git][ghc/ghc][wip/int-index/emb-type] VDQ: User's Guide entry draft
Vladislav Zavialov (@int-index)
gitlab at gitlab.haskell.org
Fri Oct 28 16:08:10 UTC 2022
Vladislav Zavialov pushed to branch wip/int-index/emb-type at Glasgow Haskell Compiler / GHC
Commits:
03af4870 by Vladislav Zavialov at 2022-10-28T19:44:21+04:00
VDQ: User's Guide entry draft
- - - - -
3 changed files:
- docs/users_guide/exts/explicit_namespaces.rst
- + docs/users_guide/exts/required_type_arguments.rst
- docs/users_guide/exts/types.rst
Changes:
=====================================
docs/users_guide/exts/explicit_namespaces.rst
=====================================
@@ -11,7 +11,7 @@ Explicit namespaces in import/export
:implied by: :extension:`TypeOperators`, :extension:`TypeFamilies`
:since: 7.6.1
- Enable use of explicit namespaces in module export lists.
+ Enable use of explicit namespaces in module export lists, patterns, and expressions.
In an import or export list, such as ::
@@ -41,3 +41,9 @@ In addition, with :extension:`PatternSynonyms` you can prefix the name of a
data constructor in an import or export list with the keyword
``pattern``, to allow the import or export of a data constructor without
its parent type constructor (see :ref:`patsyn-impexp`).
+
+Furthermore, :extension:`ExplicitNamespaces` permits the use of the ``type``
+keyword in patterns and expressions::
+ f (type t) x = ... -- in a pattern
+ r = f (type Integer) 10 -- in an expression
+This is used in conjunction with :extension:`RequiredTypeArguments`.
\ No newline at end of file
=====================================
docs/users_guide/exts/required_type_arguments.rst
=====================================
@@ -0,0 +1,111 @@
+Required type arguments
+=======================
+
+.. extension:: RequiredTypeArguments
+ :shortdesc: Enable required type arguments in terms.
+
+ :since: 9.6.1
+ :status: Experimental
+
+ Allow visible dependent quantification ``forall x ->`` in types of terms.
+
+**This feature is only partially implemented in GHC.** In this section we
+describe the implemented subset, while the full specification can be found in
+`GHC Proposal #281 <https://github.com/ghc-proposals/ghc-proposals/blob/master/proposals/0281-visible-forall.rst>`__.
+
+The :extension:`RequiredTypeArguments` extension enables the use of visible
+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.
+
+When we define ``id``, we can use a lambda to bind a variable that stands for
+the function argument::
+
+ -- For reference: id :: forall a. a -> a
+ id = \x -> x
+
+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*::
+
+ -- For reference: id_vdq :: forall a -> a -> a
+ id_vdq = \(type t) x -> x
+
+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
+
+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::
+
+ -- For reference: id_vdq :: forall a -> a -> a
+ id_vdq = \(type t) (x :: t) -> x :: t
+ -- ↑ ↑ ↑
+ -- bound used used
+
+At use sites, we also instantiate this type variable explicitly::
+
+ n = id_vdq (type Integer) 42
+ s = id_vdq (type String) "Hello"
+
+Relation to :extension:`TypeApplications`
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+:extension:`RequiredTypeArguments` are similar to :extension:`TypeApplications`
+in that we pass a type to a function as an explicit argument. The difference is
+that type applications are optional: it is up to the caller whether to write
+``id @Bool True`` or ``id True``. By default, the compiler infers that the
+type variable is intantiated to ``Bool``. The existence of a type argument is
+not reflected syntactically in the expression, it is invisible unless we use a
+*visibility override*, i.e. ``@``.
+
+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
+
+You may use an underscore to infer a required type argument::
+
+ x3 = id_vdq (type _) 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
+they are never ambiguous. Consider the type of ``Foreign.Storable.sizeOf``::
+
+ sizeOf :: forall a. Storable a => a -> Int
+
+The value parameter is not actually used, its only purpose is to drive type
+inference. At call sites, one might write ``sizeOf (undefined :: Bool)`` or
+``sizeOf @Bool undefined``. Either way, the ``undefined`` is entirely
+superfluous and exists only to avoid an ambiguous type variable.
+
+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
+passing a dummy value.
+
+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::
+
+ n = id_vdq Integer 42
+
+In this example we pass ``Integer`` as opposed to ``(type Integer)``. **This is
+not currently implemented**. But for reasons of forward-compatibility,
+:extension:`RequiredTypeArguments` neither allows the ``type`` syntax nor
+implies :extension:`ExplicitNamespaces` that does.
\ No newline at end of file
=====================================
docs/users_guide/exts/types.rst
=====================================
@@ -21,6 +21,7 @@ Types
representation_polymorphism
type_literals
type_applications
+ required_type_arguments
rank_polymorphism
impredicative_types
linear_types
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/03af487095a01027b6975a073ebe84e7f15c5bfd
--
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/03af487095a01027b6975a073ebe84e7f15c5bfd
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/20221028/1845bd25/attachment-0001.html>
More information about the ghc-commits
mailing list