Commit 2aac0ba1 authored by Adam Gundry's avatar Adam Gundry Committed by Ben Gamari
Browse files

Update OverloadedLabels docs and document HasField

Test Plan: n/a

Reviewers: bgamari, austin

Reviewed By: bgamari

Subscribers: thomie

Differential Revision: https://phabricator.haskell.org/D3144
parent ad617a3e
......@@ -1444,6 +1444,9 @@ not the Prelude versions:
via rebindable syntax if you use `-XOverloadedLists`;
see :ref:`overloaded-lists`.
- An overloaded label "``#foo``" means "``fromLabel @"foo"``", rather than
"``GHC.OverloadedLabels.fromLabel @"foo"``" (see :ref:`overloaded-labels`).
:ghc-flag:`-XRebindableSyntax` implies :ghc-flag:`-XNoImplicitPrelude`.
In all cases (apart from arrow notation), the static semantics should be
......@@ -3187,6 +3190,183 @@ More details:
g = MkT { .. } -- Illegal (b)
h (MkT { .. }) = True -- Illegal (b)
.. _record-field-selector-polymorphism:
Record field selector polymorphism
----------------------------------
The module :base-ref:`GHC.Records <GHC-Records.html>` defines the following: ::
class HasField (x :: k) r a | x r -> a where
getField :: r -> a
A ``HasField x r a`` constraint represents the fact that ``x`` is a
field of type ``a`` belonging to a record type ``r``. The
``getField`` method gives the record selector function.
This allows definitions that are polymorphic over record types with a specified
field. For example, the following works with any record type that has a field
``name :: String``: ::
foo :: HasField "name" r String => r -> String
foo r = reverse (getField @"name" r)
``HasField`` is a magic built-in typeclass (similar to ``Coercible``, for
example). It is given special treatment by the constraint solver (see
:ref:`solving-hasfield-constraints`). Users may define their own instances of
``HasField`` also (see :ref:`virtual-record-fields`).
.. _solving-hasfield-constraints:
Solving HasField constraints
~~~~~~~~~~~~~~~~~~~~~~~~~~~~
If the constraint solver encounters a constraint ``HasField x r a``
where ``r`` is a concrete datatype with a field ``x`` in scope, it
will automatically solve the constraint using the field selector as
the dictionary, unifying ``a`` with the type of the field if
necessary. This happens irrespective of which extensions are enabled.
For example, if the following datatype is in scope ::
data Person = Person { name :: String }
the end result is rather like having an instance ::
instance HasField "name" Person String where
getField = name
except that this instance is not actually generated anywhere, rather
the constraint is solved directly by the constraint solver.
A field must be in scope for the corresponding ``HasField`` constraint
to be solved. This retains the existing representation hiding
mechanism, whereby a module may choose not to export a field,
preventing client modules from accessing or updating it directly.
Solving ``HasField`` constraints depends on the field selector functions that
are generated for each datatype definition:
- If a record field does not have a selector function because its type would allow
an existential variable to escape, the corresponding ``HasField`` constraint
will not be solved. For example, ::
{-# LANGUAGE ExistentialQuantification #-}
data Exists t = forall x . MkExists { unExists :: t x }
does not give rise to a selector ``unExists :: Exists t -> t x`` and we will not
solve ``HasField "unExists" (Exists t) a`` automatically.
- If a record field has a polymorphic type (and hence the selector function is
higher-rank), the corresponding ``HasField`` constraint will not be solved,
because doing so would violate the functional dependency on ``HasField`` and/or
require impredicativity. For example, ::
{-# LANGUAGE RankNTypes #-}
data Higher = MkHigher { unHigher :: forall t . t -> t }
gives rise to a selector ``unHigher :: Higher -> (forall t . t -> t)`` but does
not lead to solution of the constraint ``HasField "unHigher" Higher a``.
- A record GADT may have a restricted type for a selector function, which may lead
to additional unification when solving ``HasField`` constraints. For example, ::
{-# LANGUAGE GADTs #-}
data Gadt t where
MkGadt :: { unGadt :: Maybe v } -> Gadt [v]
gives rise to a selector ``unGadt :: Gadt [v] -> Maybe v``, so the solver will reduce
the constraint ``HasField "unGadt" (Gadt t) b`` by unifying ``t ~ [v]`` and
``b ~ Maybe v`` for some fresh metavariable ``v``, rather as if we had an instance ::
instance (t ~ [v], b ~ Maybe v) => HasField "unGadt" (Gadt t) b
- If a record type has an old-fashioned datatype context, the ``HasField``
constraint will be reduced to solving the constraints from the context.
For example, ::
{-# LANGUAGE DatatypeContexts #-}
data Eq a => Silly a = MkSilly { unSilly :: a }
gives rise to a selector ``unSilly :: Eq a => Silly a -> a``, so
the solver will reduce the constraint ``HasField "unSilly" (Silly a) b`` to
``Eq a`` (and unify ``a`` with ``b``), rather as if we had an instance ::
instance (Eq a, a ~ b) => HasField "unSilly" (Silly a) b
.. _virtual-record-fields:
Virtual record fields
~~~~~~~~~~~~~~~~~~~~~
Users may define their own instances of ``HasField``, provided they do
not conflict with the built-in constraint solving behaviour. This
allows "virtual" record fields to be defined for datatypes that do not
otherwise have them.
For example, this instance would make the ``name`` field of ``Person``
accessible using ``#fullname`` as well: ::
instance HasField "fullname" Person String where
getField = name
More substantially, an anonymous records library could provide
``HasField`` instances for its anonymous records, and thus be
compatible with the polymorphic record selectors introduced by this
proposal. For example, something like this makes it possible to use
``getField`` to access ``Record`` values with the appropriate
string in the type-level list of fields: ::
data Record (xs :: [(k, Type)]) where
Nil :: Record '[]
Cons :: Proxy x -> a -> Record xs -> Record ('(x, a) ': xs)
instance HasField x (Record ('(x, a) ': xs)) a where
getField (Cons _ v _) = v
instance HasField x (Record xs) a => HasField x (Record ('(y, b) ': xs)) a where
getField (Cons _ _ r) = getField @x r
r :: Record '[ '("name", String) ]
r = Cons Proxy "R" Nil)
x = getField @"name" r
Since representations such as this can support field labels with kinds other
than ``Symbol``, the ``HasField`` class is poly-kinded (even though the built-in
constraint solving works only at kind ``Symbol``). In particular, this allows
users to declare scoped field labels such as in the following example: ::
data PersonFields = Name
s :: Record '[ '(Name, String) ]
s = Cons Proxy "S" Nil
y = getField @Name s
In order to avoid conflicting with the built-in constraint solving,
the following user-defined ``HasField`` instances are prohibited (in
addition to the usual rules, such as the prohibition on type
families appearing in instance heads):
- ``HasField _ r _`` where ``r`` is a variable;
- ``HasField _ (T ...) _`` if ``T`` is a data family (because it
might have fields introduced later, using data instance declarations);
- ``HasField x (T ...) _`` if ``x`` is a variable and ``T`` has any
fields at all (but this instance is permitted if ``T`` has no fields);
- ``HasField "foo" (T ...) _`` if ``T`` has a field ``foo`` (but this
instance is permitted if it does not).
If a field has a higher-rank or existential type, the corresponding ``HasField``
constraint will not be solved automatically (as described above), but in the
interests of simplicity we do not permit users to define their own instances
either. If a field is not in scope, the corresponding instance is still
prohibited, to avoid conflicts in downstream modules.
.. _deriving:
Extensions to the "deriving" mechanism
......@@ -6010,42 +6190,47 @@ The class ``IsLabel`` is defined as:
::
class IsLabel (x :: Symbol) a where
fromLabel :: Proxy# x -> a
fromLabel :: a
This is rather similar to the class ``IsString`` (see
:ref:`overloaded-strings`), but with an additional type parameter that makes the
text of the label available as a type-level string (see
:ref:`type-level-literals`).
:ref:`type-level-literals`). Note that ``fromLabel`` had an extra ``Proxy# x``
argument in GHC 8.0, but this was removed in GHC 8.2 as a type application (see
:ref:`visible-type-application`) can be used instead.
There are no predefined instances of this class. It is not in scope by default,
but can be brought into scope by importing
:base-ref:`GHC.OverloadedLabels <GHC-OverloadedLabels.html>`:. Unlike
:base-ref:`GHC.OverloadedLabels <GHC-OverloadedLabels.html>`. Unlike
``IsString``, there are no special defaulting rules for ``IsLabel``.
During typechecking, GHC will replace an occurrence of an overloaded label like
``#foo`` with
::
fromLabel (proxy# :: Proxy# "foo")
This will have some type ``alpha`` and require the solution of a class
constraint ``IsLabel "foo" alpha``.
``#foo`` with ``fromLabel @"foo"``. This will have some type ``alpha`` and
require the solution of a class constraint ``IsLabel "foo" alpha``.
The intention is for ``IsLabel`` to be used to support overloaded record fields
and perhaps anonymous records. Thus, it may be given instances for base
datatypes (in particular ``(->)``) in the future.
When writing an overloaded label, there must be no space between the hash sign
and the following identifier. :ref:`magic-hash` makes use of postfix hash
signs; if ``OverloadedLabels`` and ``MagicHash`` are both enabled then ``x#y``
means ``x# y``, but if only ``OverloadedLabels`` is enabled then it means ``x
#y``. To avoid confusion, you are strongly encouraged to put a space before the
hash when using ``OverloadedLabels``.
If :ghc-flag:`-XRebindableSyntax` is enabled, overloaded
labels will be desugared using whatever ``fromLabel`` function is in scope,
rather than always using ``GHC.OverloadedLabels.fromLabel``.
When using ``OverloadedLabels`` (or ``MagicHash``) in a ``.hsc`` file (see
:ref:`hsc2hs`), the hash signs must be doubled (write ``##foo`` instead of
``#foo``) to avoid them being treated as ``hsc2hs`` directives.
When writing an overloaded label, there must be no space between the hash sign
and the following identifier. The :ghc-flag:`-XMagicHash` extension makes use
of postfix hash signs; if :ghc-flag:`-XOverloadedLabels` and
:ghc-flag:`-XMagicHash` are both enabled then ``x#y`` means ``x# y``, but if
only :ghc-flag:`-XOverloadedLabels` is enabled then it means ``x #y``. The
:ghc-flag:`-XUnboxedTuples` extension makes ``(#`` a single lexeme, so when
:ghc-flag:`-XUnboxedTuples` is enabled you must write a space between an opening
parenthesis and an overloaded label. To avoid confusion, you are strongly
encouraged to put a space before the hash when using
:ghc-flag:`-XOverloadedLabels`.
When using :ghc-flag:`-XOverloadedLabels` (or other extensions that make use of
hash signs) in a ``.hsc`` file (see :ref:`hsc2hs`), the hash signs must be
doubled (write ``##foo`` instead of ``#foo``) to avoid them being treated as
``hsc2hs`` directives.
Here is an extension of the record access example in :ref:`type-level-literals`
showing how an overloaded label can be used as a record selector:
......@@ -6070,7 +6255,7 @@ showing how an overloaded label can be used as a record selector:
instance Has Point "y" Int where from (Point _ y) _ = y
instance Has a l b => IsLabel l (a -> b) where
fromLabel _ x = from x (Get :: Label l)
fromLabel x = from x (Get :: Label l)
example = #x (Point 1 2)
......
......@@ -484,6 +484,13 @@ languageOptions =
, flagReverse = "-XNoOverlappingInstances"
, flagSince = "6.8.1"
}
, flag { flagName = "-XOverloadedLabels"
, flagDescription =
"Enable :ref:`overloaded labels <overloaded-labels>`."
, flagType = DynamicFlag
, flagReverse = "-XNoOverloadedLabels"
, flagSince = "8.0.1"
}
, flag { flagName = "-XOverloadedLists"
, flagDescription =
"Enable :ref:`overloaded lists <overloaded-lists>`."
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment