diff options
Diffstat (limited to 'docs')
| -rw-r--r-- | docs/users_guide/exts/gadt.rst | 2 | ||||
| -rw-r--r-- | docs/users_guide/exts/type_abstractions.rst | 95 | ||||
| -rw-r--r-- | docs/users_guide/exts/type_applications.rst | 81 | ||||
| -rw-r--r-- | docs/users_guide/exts/types.rst | 1 |
4 files changed, 99 insertions, 80 deletions
diff --git a/docs/users_guide/exts/gadt.rst b/docs/users_guide/exts/gadt.rst index 99902cc76d..89ecf8473d 100644 --- a/docs/users_guide/exts/gadt.rst +++ b/docs/users_guide/exts/gadt.rst @@ -227,7 +227,7 @@ also sets :extension:`GADTSyntax` and :extension:`MonoLocalBinds`. case f of (_ :: F (Maybe z) (Maybe z)) -> Nothing @z - Another way is to use :ref:`type-applications-in-patterns` instead of a + Another way is to use :ref:`type-abstractions-in-patterns` instead of a pattern type signature: :: g4 :: F a a -> a diff --git a/docs/users_guide/exts/type_abstractions.rst b/docs/users_guide/exts/type_abstractions.rst new file mode 100644 index 0000000000..02c147ed74 --- /dev/null +++ b/docs/users_guide/exts/type_abstractions.rst @@ -0,0 +1,95 @@ +Type abstractions +================= + +.. extension:: TypeAbstractions + :shortdesc: Enable type abstraction syntax in patterns and type variable binders. + + :since: 9.6.1 + + :status: Partially implemented + + Allow the use of type abstraction syntax. + +The :extension:`TypeAbstractions` extension provides a way to explicitly bind +scoped type or kind variables using the ``@a`` syntax. The feature is only +partially implemented, and this text covers only the implemented parts, whereas +the full specification can be found in GHC Proposals `#448 <https://github.com/ghc-proposals/ghc-proposals/blob/master/proposals/0448-type-variable-scoping.rst>`__ +and `#425 <https://github.com/ghc-proposals/ghc-proposals/blob/master/proposals/0425-decl-invis-binders.rst>`__. + + +.. _type-abstractions-in-patterns: + +Type Abstractions in Patterns +----------------------------- + +The type abstraction syntax can be used in patterns that match a data +constructor. The syntax can't be used with record patterns or infix patterns. +This is useful in particular to bind existential type variables associated with +a GADT data constructor as in the following example:: + + {-# LANGUAGE AllowAmbiguousTypes #-} + {-# LANGUAGE GADTs #-} + {-# LANGUAGE RankNTypes #-} + {-# LANGUAGE TypeApplications #-} + import Data.Proxy + + data Foo where + Foo :: forall a. (Show a, Num a) => Foo + + test :: Foo -> String + test x = case x of + Foo @t -> show @t 0 + + main :: IO () + main = print $ test (Foo @Float) + +In this example, the case in ``test``` is binding an existential variable introduced +by ``Foo`` that otherwise could not be named and used. + +It's possible to bind variables to any part of the type arguments to a constructor; +there is no need for them to be existential. In addition, it's possible to "match" against +part of the type argument using type constructors. + +For a somewhat-contrived example:: + + foo :: (Num a) => Maybe [a] -> String + foo (Nothing @[t]) = show (0 :: t) + foo (Just @[t] xs) = show (sum xs :: t) + +Here, we're binding the type variable t to be the type of the elements of the list type +which is itself the argument to Maybe. + +The order of the type arguments specified by the type applications in a pattern is the same +as that for an expression: either the order as given by the user in an explicit ``forall`` in the +definition of the data constructor, or if that is not present, the order in which the type +variables appear in its type signature from left to right. + +For example if we have the following declaration in GADT syntax:: + + data Foo :: * -> * where + A :: forall s t. [(t,s)] -> Foo (t,s) + B :: (t,s) -> Foo (t,s) + +Then the type arguments to ``A`` will match first ``s`` and then ``t``, while the type arguments +to ``B`` will match first ``t`` and then ``s``. + +Type arguments appearing in patterns can influence the inferred type of a definition:: + + foo (Nothing @Int) = 0 + foo (Just x) = x + +will have inferred type:: + + foo :: Maybe Int -> Int + +which is more restricted than what it would be without the application:: + + foo :: Num a => Maybe a -> a + +For more information and detail regarding type applications in patterns, see the paper +`Type variables in patterns <https://arxiv.org/pdf/1806.03476>`__ by Eisenberg, Breitner +and Peyton Jones. Relative to that paper, the implementation in GHC for now at least makes one +additional conservative restriction, that type variables occurring in patterns must not +already be in scope, and so are always new variables that only bind whatever type is +matched, rather than ever referring to a variable from an outer scope. Type wildcards +``_`` may be used in any place where no new variable needs binding. diff --git a/docs/users_guide/exts/type_applications.rst b/docs/users_guide/exts/type_applications.rst index d2a0e4ca16..f37325d9cd 100644 --- a/docs/users_guide/exts/type_applications.rst +++ b/docs/users_guide/exts/type_applications.rst @@ -4,7 +4,7 @@ Visible type application ======================== .. extension:: TypeApplications - :shortdesc: Enable type application syntax in terms, patterns and types. + :shortdesc: Enable type application syntax in terms and types. :since: 8.0.1 @@ -261,81 +261,4 @@ of equality over types. For example, given the following definitions: :: app2 g x = g x GHC will deem all of ``app1 id1``, ``app1 id2``, ``app2 id1``, and ``app2 id2`` -to be well typed. - -.. _type-applications-in-patterns: - -Type Applications in Patterns ------------------------------ - -The type application syntax can be used in patterns that match a data -constructor. The syntax can't be used with record patterns or infix patterns. -This is useful in particular to bind existential type variables associated with -a GADT data constructor as in the following example:: - - {-# LANGUAGE AllowAmbiguousTypes #-} - {-# LANGUAGE GADTs #-} - {-# LANGUAGE RankNTypes #-} - {-# LANGUAGE TypeApplications #-} - import Data.Proxy - - data Foo where - Foo :: forall a. (Show a, Num a) => Foo - - test :: Foo -> String - test x = case x of - Foo @t -> show @t 0 - - main :: IO () - main = print $ test (Foo @Float) - -In this example, the case in ``test``` is binding an existential variable introduced -by ``Foo`` that otherwise could not be named and used. - -It's possible to bind variables to any part of the type arguments to a constructor; -there is no need for them to be existential. In addition, it's possible to "match" against -part of the type argument using type constructors. - -For a somewhat-contrived example:: - - foo :: (Num a) => Maybe [a] -> String - foo (Nothing @[t]) = show (0 :: t) - foo (Just @[t] xs) = show (sum xs :: t) - -Here, we're binding the type variable t to be the type of the elements of the list type -which is itself the argument to Maybe. - -The order of the type arguments specified by the type applications in a pattern is the same -as that for an expression: either the order as given by the user in an explicit ``forall`` in the -definition of the data constructor, or if that is not present, the order in which the type -variables appear in its type signature from left to right. - -For example if we have the following declaration in GADT syntax:: - - data Foo :: * -> * where - A :: forall s t. [(t,s)] -> Foo (t,s) - B :: (t,s) -> Foo (t,s) - -Then the type arguments to ``A`` will match first ``s`` and then ``t``, while the type arguments -to ``B`` will match first ``t`` and then ``s``. - -Type arguments appearing in patterns can influence the inferred type of a definition:: - - foo (Nothing @Int) = 0 - foo (Just x) = x - -will have inferred type:: - - foo :: Maybe Int -> Int - -which is more restricted than what it would be without the application:: - - foo :: Num a => Maybe a -> a - -For more information and detail regarding type applications in patterns, see the paper -`Type variables in patterns <https://arxiv.org/pdf/1806.03476>`__ by Eisenberg, Breitner -and Peyton Jones. Relative to that paper, the implementation in GHC for now at least makes one -additional conservative restriction, that type variables occurring in patterns must not -already be in scope, and so are always new variables that only bind whatever type is -matched, rather than ever referring to a variable from an outer scope. Type wildcards -``_`` may be used in any place where no new variable needs binding. +to be well typed.
\ No newline at end of file diff --git a/docs/users_guide/exts/types.rst b/docs/users_guide/exts/types.rst index ea85223184..8d2b6f9f90 100644 --- a/docs/users_guide/exts/types.rst +++ b/docs/users_guide/exts/types.rst @@ -21,6 +21,7 @@ Types representation_polymorphism type_literals type_applications + type_abstractions rank_polymorphism impredicative_types linear_types |