... | ... | @@ -6,7 +6,7 @@ This page -- a description of the first phase of integrating full dependent type |
|
|
# User-facing changes
|
|
|
|
|
|
|
|
|
The changes described below are intended to be controlled by a new extension `-XStarInStar`, which will imply `-XPolyKinds` and `-XDataKinds`. But in some cases, it would be quite hard for GHC to know that the new features are being used. These cases all fall under the use of `-XPolyKinds`. So the `-XPolyKinds` language will become modestly more expressive under this proposal. But Haskell98 and Haskell2010 modes remain as standards-compliant as they are today.
|
|
|
The changes described below are intended to be controlled by a new extension `-XTypeInType`, which will imply `-XPolyKinds` and `-XDataKinds`. But in some cases, it would be quite hard for GHC to know that the new features are being used. These cases all fall under the use of `-XPolyKinds`. So the `-XPolyKinds` language will become modestly more expressive under this proposal. But Haskell98 and Haskell2010 modes remain as standards-compliant as they are today.
|
|
|
|
|
|
## Kinds and types are the same
|
|
|
|
... | ... | @@ -58,16 +58,21 @@ data TypeRep (a :: k) where |
|
|
TMaybe :: TypeRep Maybe
|
|
|
```
|
|
|
|
|
|
## `*` is hard to parse
|
|
|
## `*` is hard to parse, will become `type`
|
|
|
|
|
|
|
|
|
Say the phrase `Foo * Int` appears in a type. Is that the type operator `*` applied to `Foo` and `Int` or the the type `Foo` applied to the kind `*` and `Int`? It's impossible to know. So we have to do something strange here.
|
|
|
|
|
|
|
|
|
Without `-XStarInStar`, GHC will continue to use its knowledge of whether you are in a type or a kind to distinguish between the type operator `*` and the kind `*`. So all existing code will continue to work, quite conveniently.
|
|
|
Without `-XTypeInType`, GHC will continue to use its knowledge of whether you are in a type or a kind to distinguish between the type operator `*` and the kind `*`. So all existing code will continue to work, quite conveniently.
|
|
|
|
|
|
|
|
|
With `-XStarInStar`, GHC will treat the kind `*` as an identifier exported from the `Prelude` (and also from `GHC.Exts`). Currently, GHC must parse expressions with operators essentially as a space-separated list of tokens, because it can't know fixities until it figures out where all the operators have been imported from. Thus, when sorting out fixities, the kind `*` will just have a magical fixity which instructs the renamer to treat it like an alphanumeric identifier, not a symbol. This should all work out fine in most code. The only problem is when a user has both the kind `*` and some type operator `*` in scope, such as from `GHC.TypeLits`. Using `*` in this scenario will be a straightforward ambiguous identifier and is an error. Note that `-XStarInStar -XNoImplicitPrelude` will then mean that you cannot use the kind `*` in your program without importing it from somewhere.
|
|
|
With `-XTypeInType`, GHC will treat the kind `*` as an identifier exported from the `Prelude` (and also from `GHC.Exts`). Currently, GHC must parse expressions with operators essentially as a space-separated list of tokens, because it can't know fixities until it figures out where all the operators have been imported from. Thus, when sorting out fixities, the kind `*` will just have a magical fixity which instructs the renamer to treat it like an alphanumeric identifier, not a symbol. This should all work out fine in most code. The only problem is when a user has both the kind `*` and some type operator `*` in scope, such as from `GHC.TypeLits`. Using `*` in this scenario will be a straightforward ambiguous identifier and is an error. Note that `-XTypeInType -XNoImplicitPrelude` will then mean that you cannot use the kind `*` in your program without importing it from somewhere.
|
|
|
|
|
|
|
|
|
In addition to the above treatment, the keyword `type` will have the same meaning as `*`, as requested by several people in the community. The eventual plan is to deprecate and remove `*` as a parsing oddity. `type` will work both with and without `-XTypeInType`. The primary motivation for using `type` here (as opposed to `Type` or `TYPE` or `U`) is that it does not clobber any existing syntax.
|
|
|
|
|
|
**QUESTION:** Should `*` just be disabled in `-XTypeInType` code? This is backward compatible but creates a terrible migration story for someone who wants to use `-XTypeInType` in GHC 8.0 but not in previous versions.
|
|
|
|
|
|
## Visible type application
|
|
|
|
... | ... | |