diff options
Diffstat (limited to 'docs/users_guide/exts')
| -rw-r--r-- | docs/users_guide/exts/data_kinds.rst | 54 | ||||
| -rw-r--r-- | docs/users_guide/exts/linear_types.rst | 2 | ||||
| -rw-r--r-- | docs/users_guide/exts/poly_kinds.rst | 28 | ||||
| -rw-r--r-- | docs/users_guide/exts/primitives.rst | 14 | ||||
| -rw-r--r-- | docs/users_guide/exts/representation_polymorphism.rst | 2 |
5 files changed, 51 insertions, 49 deletions
diff --git a/docs/users_guide/exts/data_kinds.rst b/docs/users_guide/exts/data_kinds.rst index 75e60f6a0f..50816cbb53 100644 --- a/docs/users_guide/exts/data_kinds.rst +++ b/docs/users_guide/exts/data_kinds.rst @@ -45,8 +45,8 @@ With :extension:`DataKinds`, the example above can then be rewritten to: :: data Nat = Ze | Su Nat data Vec :: Type -> Nat -> Type where - Nil :: Vec a 'Ze - Cons :: a -> Vec a n -> Vec a ('Su n) + Nil :: Vec a Ze + Cons :: a -> Vec a n -> Vec a (Su n) With the improved kind of ``Vec``, things like ``Vec Int Char`` are now ill-kinded, and GHC will report an error. @@ -62,27 +62,26 @@ following types :: data List a = Nil | Cons a (List a) - data Pair a b = Pair a b + data Pair a b = MkPair a b data Sum a b = L a | R b -give rise to the following kinds and type constructors (where promoted -constructors are prefixed by a tick ``'``): :: +give rise to the following kinds and type constructors: :: Nat :: Type - 'Zero :: Nat - 'Succ :: Nat -> Nat + Zero :: Nat + Succ :: Nat -> Nat List :: Type -> Type - 'Nil :: forall k. List k - 'Cons :: forall k. k -> List k -> List k + Nil :: forall k. List k + Cons :: forall k. k -> List k -> List k Pair :: Type -> Type -> Type - 'Pair :: forall k1 k2. k1 -> k2 -> Pair k1 k2 + MkPair :: forall k1 k2. k1 -> k2 -> Pair k1 k2 Sum :: Type -> Type -> Type - 'L :: k1 -> Sum k1 k2 - 'R :: k2 -> Sum k1 k2 + L :: k1 -> Sum k1 k2 + R :: k2 -> Sum k1 k2 Virtually all data constructors, even those with rich kinds, can be promoted. There are only a couple of exceptions to this rule: @@ -108,22 +107,25 @@ There are only a couple of exceptions to this rule: Distinguishing between types and constructors --------------------------------------------- -In the examples above, all promoted constructors are prefixed with a single -quote mark ``'``. This mark tells GHC to look in the data constructor namespace -for a name, not the type (constructor) namespace. Consider :: +Consider :: data P = MkP -- 1 data Prom = P -- 2 -We can thus distinguish the type ``P`` (which has a constructor ``MkP``) -from the promoted data constructor ``'P`` (of kind ``Prom``). +The name ``P`` on the type level will refer to the type ``P`` (which has +a constructor ``MkP``) rather than the promoted data constructor +``P`` of kind ``Prom``. To refer to the latter, prefix it with a +single quote mark: ``'P``. + +This syntax can be used even if there is no ambiguity (i.e. +there's no type ``P`` in scope). -As a convenience, GHC allows you to omit the quote mark when the name is -unambiguous. However, our experience has shown that the quote mark helps -to make code more readable and less error-prone. GHC thus supports -:ghc-flag:`-Wunticked-promoted-constructors` that will warn you if you -use a promoted data constructor without a preceding quote mark. +GHC supports :ghc-flag:`-Wunticked-promoted-constructors` that warns +whenever a promoted data constructor is written without a quote mark. +As of GHC 9.4, this warning is no longer enabled by :ghc-flag:`-Wall`; +we no longer recommend quote marks as a preferred default +(see :ghc-ticket:`20531`). Just as in the case of Template Haskell (:ref:`th-syntax`), GHC gets confused if you put a quote mark before a data constructor whose second @@ -224,11 +226,11 @@ only equality constraints are supported. Here is an example of a constrained kind: :: type family IsTypeLit a where - IsTypeLit Nat = 'True - IsTypeLit Symbol = 'True - IsTypeLit a = 'False + IsTypeLit Nat = True + IsTypeLit Symbol = True + IsTypeLit a = False - data T :: forall a. (IsTypeLit a ~ 'True) => a -> Type where + data T :: forall a. (IsTypeLit a ~ True) => a -> Type where MkNat :: T 42 MkSymbol :: T "Don't panic!" diff --git a/docs/users_guide/exts/linear_types.rst b/docs/users_guide/exts/linear_types.rst index 9985310d49..2d6e60112b 100644 --- a/docs/users_guide/exts/linear_types.rst +++ b/docs/users_guide/exts/linear_types.rst @@ -117,7 +117,7 @@ It is also possible to define a multiplicity-polymorphic field: While linear fields are generalized (``MkT1 :: forall {m} a. a %m -> T1 a`` in the previous example), multiplicity-polymorphic fields are not; -it is not possible to directly use ``MkT3`` as a function ``a -> T3 a 'One``. +it is not possible to directly use ``MkT3`` as a function ``a -> T3 a One``. If :extension:`LinearTypes` is disabled, all fields are considered to be linear fields, including GADT fields defined with the ``->`` arrow. diff --git a/docs/users_guide/exts/poly_kinds.rst b/docs/users_guide/exts/poly_kinds.rst index 25843aedb0..ad10e1b188 100644 --- a/docs/users_guide/exts/poly_kinds.rst +++ b/docs/users_guide/exts/poly_kinds.rst @@ -318,7 +318,7 @@ signature" for a type constructor? These are the forms: {-# LANGUAGE UnliftedNewtypes #-} newtype N1 where -- No; missing kind signature - newtype N2 :: TYPE 'IntRep where -- Yes; kind signature present + newtype N2 :: TYPE IntRep where -- Yes; kind signature present newtype N3 (a :: Type) where -- No; missing kind signature newtype N4 :: k -> Type where -- No; `k` is not explicitly quantified newtype N5 :: forall (k :: Type). k -> Type where -- Yes; good signature @@ -711,37 +711,37 @@ would become a *visible* parameter:: Note that we only look at the *outermost* kind signature to decide which variables to quantify implicitly. As a counter-example, consider ``M1``: :: - type M1 = 'Just ('Nothing :: Maybe k) -- rejected: k not in scope + type M1 = Just (Nothing :: Maybe k) -- rejected: k not in scope -Here, the kind signature is hidden inside ``'Just``, and there is no outermost +Here, the kind signature is hidden inside ``Just``, and there is no outermost kind signature. We can fix this example by providing an outermost kind signature: :: - type M2 = 'Just ('Nothing :: Maybe k) :: Maybe (Maybe k) + type M2 = Just (Nothing :: Maybe k) :: Maybe (Maybe k) Here, ``k`` is brought into scope by ``:: Maybe (Maybe k)``. A kind signature is considered to be outermost regardless of redundant parentheses: :: - type P = 'Nothing :: Maybe a -- accepted - type P = ((('Nothing :: Maybe a))) -- accepted + type P = Nothing :: Maybe a -- accepted + type P = (((Nothing :: Maybe a))) -- accepted Closed type family instances are subject to the same rules: :: type family F where - F = 'Nothing :: Maybe k -- accepted + F = Nothing :: Maybe k -- accepted type family F where - F = 'Just ('Nothing :: Maybe k) -- rejected: k not in scope + F = Just (Nothing :: Maybe k) -- rejected: k not in scope type family F where - F = 'Just ('Nothing :: Maybe k) :: Maybe (Maybe k) -- accepted + F = Just (Nothing :: Maybe k) :: Maybe (Maybe k) -- accepted type family F :: Maybe (Maybe k) where - F = 'Just ('Nothing :: Maybe k) -- rejected: k not in scope + F = Just (Nothing :: Maybe k) -- rejected: k not in scope type family F :: Maybe (Maybe k) where - F @k = 'Just ('Nothing :: Maybe k) -- accepted + F @k = Just (Nothing :: Maybe k) -- accepted Kind variables can also be quantified in *visible* positions. Consider the following two examples: :: @@ -957,16 +957,16 @@ Here is an example of this in action: :: -- separate module having imported the first {-# LANGUAGE NoPolyKinds, DataKinds #-} - z = Proxy :: Proxy 'MkCompose + z = Proxy :: Proxy MkCompose -In the last line, we use the promoted constructor ``'MkCompose``, which has +In the last line, we use the promoted constructor ``MkCompose``, which has kind :: forall (a :: Type) (b :: Type) (f :: b -> Type) (g :: a -> b) (x :: a). f (g x) -> Compose f g x Now we must infer a type for ``z``. To do so without generalising over kind -variables, we must default the kind variables of ``'MkCompose``. We can easily +variables, we must default the kind variables of ``MkCompose``. We can easily default ``a`` and ``b`` to ``Type``, but ``f`` and ``g`` would be ill-kinded if defaulted. The definition for ``z`` is thus an error. diff --git a/docs/users_guide/exts/primitives.rst b/docs/users_guide/exts/primitives.rst index 2b8e88aa23..46c8dfb13b 100644 --- a/docs/users_guide/exts/primitives.rst +++ b/docs/users_guide/exts/primitives.rst @@ -83,11 +83,11 @@ The Haskell Report describes that ``*`` (spelled ``Type`` and imported from such as ``Int``. Furthermore, type constructors can have kinds with arrows; for example, ``Maybe`` has kind ``Type -> Type``. Unboxed types have a kind that specifies their runtime representation. For example, the type ``Int#`` has kind -``TYPE 'IntRep`` and ``Double#`` has kind ``TYPE 'DoubleRep``. These kinds say +``TYPE IntRep`` and ``Double#`` has kind ``TYPE DoubleRep``. These kinds say that the runtime representation of an ``Int#`` is a machine integer, and the runtime representation of a ``Double#`` is a machine double-precision floating point. In contrast, the kind ``Type`` is actually just a synonym for ``TYPE -'LiftedRep``. More details of the ``TYPE`` mechanisms appear in the `section +LiftedRep``. More details of the ``TYPE`` mechanisms appear in the `section on runtime representation polymorphism <#runtime-rep>`__. Given that ``Int#``'s kind is not ``Type``, then it follows that ``Maybe @@ -326,13 +326,13 @@ of a ``newtype``. For example, the type :: newtype A = MkA Int# is accepted when this extension is enabled. This creates a type -``A :: TYPE 'IntRep`` and a data constructor ``MkA :: Int# -> A``. +``A :: TYPE IntRep`` and a data constructor ``MkA :: Int# -> A``. Although the kind of ``A`` is inferred by GHC, there is nothing visually distinctive about this type that indicated that is it not of kind ``Type`` like newtypes typically are. `GADTSyntax <#gadt-style>`__ can be used to provide a kind signature for additional clarity :: - newtype A :: TYPE 'IntRep where + newtype A :: TYPE IntRep where MkA :: Int# -> A The ``Coercible`` machinery works with unlifted newtypes just like it does with @@ -362,14 +362,14 @@ instances. In particular, :extension:`UnliftedNewtypes` permits a permitted: :: class Foo a where - data FooKey a :: TYPE 'IntRep + data FooKey a :: TYPE IntRep class Bar (r :: RuntimeRep) where data BarType r :: TYPE r instance Foo Bool where newtype FooKey Bool = FooKeyBoolC Int# - instance Bar 'WordRep where - newtype BarType 'WordRep = BarTypeWordRepC Word# + instance Bar WordRep where + newtype BarType WordRep = BarTypeWordRepC Word# It is worth noting that :extension:`UnliftedNewtypes` is *not* required to give the data families themselves return kinds involving ``TYPE``, such as the diff --git a/docs/users_guide/exts/representation_polymorphism.rst b/docs/users_guide/exts/representation_polymorphism.rst index 28b3cc78bf..4d461e06fd 100644 --- a/docs/users_guide/exts/representation_polymorphism.rst +++ b/docs/users_guide/exts/representation_polymorphism.rst @@ -27,7 +27,7 @@ Here are the key definitions, all available from ``GHC.Exts``: :: type Type = TYPE LiftedRep -- Type is just an ordinary type synonym The idea is that we have a new fundamental type constant ``TYPE``, which -is parameterised by a ``RuntimeRep``. We thus get ``Int# :: TYPE 'IntRep`` +is parameterised by a ``RuntimeRep``. We thus get ``Int# :: TYPE IntRep`` and ``Bool :: TYPE LiftedRep``. Anything with a type of the form ``TYPE x`` can appear to either side of a function arrow ``->``. We can thus say that ``->`` has type |