Embrace Type :: Type
¶
GHC 8.0 included a major change to GHC’s type system: the Type :: Type
axiom.
Though casual users were protected from this by hiding its features behind the
-XTypeInType
extension, all programs written in GHC 8+ have the axiom behind
the scenes. In order to preserve backward compatibility, various legacy features
were left unchanged. For example, with -XDataKinds
but not -XTypeInType
,
GADTs could not be used in types.
This proposal suggests to remove the backward-compatibility features, embracing
Type :: Type
. Specifically:
Incorporate the features currently in
-XTypeInType
into the-XPolyKinds
and-XDataKinds
extensions.Deprecate the
-XTypeInType
extension (as it would be a synonym for-XPolyKinds -XDataKinds
).Introduce a new extension
-XStarIsType
to control how to parse*
in code and whether to print it in error messages.
Motivation¶
This is a simplification over the status quo, with two closely related extensions (
-XPolyKinds
and-XTypeInType
) and an arbitrary, historical distinction between them.GHC’s ability to parse
*
has a significant cost. It’s the only symbolic identifier that’s handled like an alphanumeric one. (Note thatT * Int
normally looks like an application of a binary operator*
toT
andInt
, but with the kind*
, it’sT
applied to*
andInt
.) Because*
is sometimes indeed a binary operator in types (seeGHC.TypeLits
), we can disambiguate the infix from the prefix case only in the renamer. This means that the parser has to treat a type-level expressionA B * C * E
essentially as a list of types, only to be rejigged by the renamer. (This rejigging is independent of the fixity-rejigging the renamer also has to do, so there’s no shared cost here.) GHC also has to handle both*
and its unicode variant identically, adding to this cost.The new approach to handling
*
makes it obvious in the parser whether*
is infix or not, vastly simplifying matters. Also, by using an extension to specify the handling of*
, it is straightforward also to have the same extension control output in error messages.If we plan to remove
*
from the language at some point, we should start updating error messages sooner than later.In truth, GHC always has
Type :: Type
, whether you say-XTypeInType
or no. Thus, the real extension name should be-XPolyKinds
, because it’s kind polymorphism that the user wants, not the always-trueType :: Type
.The reason for a distinction between the extensions was because
-XTypeInType
started out as rather buggy and experimental, whereas-XPolyKinds
and-XDataKinds
had settled down by GHC 8. There was the possibility that-XTypeInType
would allow you to shoot the gorillas (my suggestion for an update of “launch the rockets”; the latter seems just a bit too poignant these days) while-XPolyKinds -XDataKinds
wouldn’t. That possibility has not come to fruition (happily), and so the distinction isn’t really paying its way. Note that what we’re doing here is very much like the merger between-XRankNTypes
and-XRank2Types
.The one difference between
-XPolyKinds
and-XTypeInType
that’s worth preserving is that the former allows easy access to the kind*
. The-XStarIsType
extension is meant to preserve this difference.
Proposed Change Specification¶
Make
-XPolyKinds
incoporate the new features (other than expanded promotion of types) of-XTypeInType
. By scanning through GHC’s source code, I was able to find the places where GHC currently distinguishes between these extensions (labeled for easy reference):The meaning of CUSK is slightly different between
-XPolyKinds
and-XTypeInType
. See the second bullet of the CUSK section of the manual. The-XTypeInType
behavior would be retained. Migrating from the-XPolyKinds
behavior simply requires adding an explicitforall k
in some cases.Type and kind vars can be freely mixed in
-XTypeInType
code. This change is fully backward compatible; no migration would be necessary.Various constructs can appear in kinds with
-XTypeInType
, but not without. These include promoted lists,forall
, among others. This change is fully backward compatible; no migration would be necessary.
With
-XPolyKinds
, kind variables are assumed to have kindBOX
(which has becomeType
).-XTypeInType
, on the other hand, makes no assumption about the kind of a kind variable. This is a generalization over current behavior, which can potentially lead to trouble. I am unable to come up with an example, though.Kind-indexed GADTs are allowed with
-XTypeInType
. These would now be allowed with-XGADTs -XPolyKinds
only. This change is fully backward compatible; no migration would be necessary.
-XDataKinds
would now promote GADTs and GADT constructors. This change is fully backward compatible; no migration would be necessary.Two releases after this proposal is implemented, deprecate
-XTypeInType
.Introduce a new language extension
-XStarIsType
, with the following behavior:-XStarIsType
is on by default.When
-XStarIsType
is on, any occurrence of the symbol*
in a type is treated as the kind of types with values. It is parsed similarly to alphanumeric identifiers, never as a binary operator.When
-XStarIsType
is on, a user can use a binary operator*
only with a qualifying module name. For example,8 ~ (4 GHC.TypeLits.* 2)
, or8 ~ (4 L.* 2)
if we haveimport GHC.TypeLits as L
.When
-XStarIsType
is not on, the pretty-printer will printType
instead of*
in error messages.Without
-XStarIsType
, there is no way to use the symbol*
to refer to the kind of types with values. UseType
(which can be imported fromData.Kind
) instead. The symbol*
will refer to any type-level binary operator*
in scope, according to the normal scoping rules. (If-XTypeOperators
is not in effect, use of*
in a type will be an error.)
The
-XStarIsType
idea is due to David Feuer, @treeowl.
Effect and Interactions¶
One way to understand the changes to
*
is this:Currently, GHC follows this process to determine what a
*
in a type-level context means:If
-XTypeInType
is in effect:If the use of
*
refers toData.Kind.*
, then parse it as an alphanumeric identifier; it meansType
.If
*
refers to some other type, it is a binary operator.
If
-XTypeInType
is not in effect:If the use of
*
is in a context that is syntactically understood to be a kind,*
is parsed as an alphanumeric identifier and meansType
.Otherwise, it is a binary operator.
Under this proposal, this is all simplified to this:
If
-XStarIsType
is in effect,*
is parsed as an alphanumeric identifier and meansType
.Otherwise,
*
is a binary operator.
Much simpler!
Note that the design of this proposal conforms to the three-release policy, in that users will not need to use CPP to avoid warnings. (In particular, note that
import Data.Kind
is always a fine thing to do, even without-XTypeInType
.)This proposal paves the way for future proposals relating to type-level features. Specifically, implementing this will make it possible to treat kind-variable scoping the same way we do type-variable scoping, as proposed in #103.
Migration path: For most users, no migration will be necessary. The exception will be those programs which define or use
*
as a type family. Currently working code like:{-# LANGUAGE KindSignatures, DataKinds, TypeOperators #-} import Data.Proxy import GHC.TypeLits mult :: forall (m :: Nat) (n :: Nat). Proxy m -> Proxy n -> Proxy (m * n) mult _ _ = Proxy
will need to explicitly enable
-XNoStarIsType
. See Have TypeOperators imply NoStarIsType for an alternative.
Costs and Drawbacks¶
This is a simplification to the implementation and description of GHC. Hooray!
This will effectively create two different versions of
-XPolyKinds
and-XDataKinds
, which could be problematic for users who want tooling to choose compilers based on extension names. Is this a problem in practice? I don’t know. Even without this change,-XPolyKinds
evolved significantly during the GHC 7 releases, as do various other extensions, so users already have to resort to measures other that just looking at extensions when choosing a compiler version.Modules that use
*
both as a binary operator and as the kind of types with values will have to be updated to useType
instead, as imported fromData.Kind
. This change is backward compatible to GHC 8.0. (Alternatively, they could use-XStarIsType
and fully-qualify their uses of the binary operator*
.)
Alternatives¶
Come up with a new extension name that encompasses both
-XTypeInType
and-XPolyKinds
. All three would be synonymous.Live with the status quo, with quite a bit of code in GHC to support it.
Do not support fully-qualified uses of the binary operator
*
when-XStarIsType
is in effect. Under this alternative, users would have no workaround to access the binary operator*
with-XStarIsType
.Introduce a new extension
-XTypeColonOperators
, which allows only those type-level operators that begin with a:
, conveniently working withData.Type.Equality
andGHC.Generics
. This new extension would not disable-XStarIsType
, as the two don’t conflict.I personally do not think this addition is worth it, but it was suggested on the pull request.
Report
Type
in error messages, regardless of whether-XStarIsType
is enabled. An advantage here is that I thinkType
is easier to understand than*
: just about everyone whom I’ve taught about kinds gets very confused about the name*
, thinking that*
is some kind of universal kind that encompasses all other kinds. (Indeed, I thought this, too, once upon a time.)This alternative has two noteworthy drawbacks:
There are gobs of resources that use
*
. These would all go out of date.The Haskell Reports mention
*
by name. If error messages printType
instead of*
, we’ll be further from the behavior that the Report authors intended at the time. However, as the Reports do not specify error message text, this change does not bring us further from formal compliance to the letter of the Report. It would bring us further from the spirit of the Report.
Currently, and in this proposal, both
*
and its unicode variant ★ are treated identically. One way to have our cake and eat it too is to follow the plan above for*
but force ★ to always lex as an alphanumeric identifier (the way*
-as-Type
lexes now). That way, folks who are really wedded to using a star can still do so. This would not be backwards compatible, because anyone who uses ★ as a type-level infix operator would have to change the name of their operator; there would be no way to use ★ infix (without backquotes, as usual).Introduce a new way of writing
Type
:type
. That is, the keywordtype
would be the kind of types with values. We could sayclass Monad (m :: type -> type)
. This has the advantage that clients do not need to import anything, as we could maketype
always in scope (as it is a keyword). Furthermore, existing tools already apply syntax highlighting totype
, which I think is reasonable. Disadvantages include the fact thattype
will look like a type variable without syntax highlighting enabled, this is a new change to an area that has already undergone some disruptive changes, and it has been mentioned previously and rejected. But I still like it, so I’m mentioning it here.EDIT: After further discussion, I’m less enamored of this idea, for two reasons:
This
type
would simply be a type synonym forTYPE LiftedRep
, as it is today. It’s quite strange to have a keyword be an ordinary type synonym.@nomeata pointed out (offline discussion) that currently,
type
is used in export lists to denote a namespace. It’s quite possible that its use as a namespace selector might grow in the future, and usingtype
to meanType
would preclude this.
I find both arguments compelling independently, and so I withdraw support for this alternative. Nevertheless, I’m keeping it in the proposal in case someone wants to argue in support of it.
Have TypeOperators imply NoStarIsType¶
One alternative is to have an additional 4.f step in the Proposed Change Specification section:
For two releases,
-XTypeOperators
will imply-XNoStarIsType
, to provide a migration path for code that uses the binary operator*
. (After two releases, this code can include-XNoStarIsType
explicitly without going against the three-release policy.) Users can re-enable-XStarIsType
after-XTypeOperators
is enabled if they wish.
This alternative is problematic. It’s intended to help migration, but
implementation evidence shows it causes more trouble. If the code being
migrated only enables -XTypeOperators
, then 4.f will indeed be helpful, but
there is a lot of code which also enables -XKindSignatures
in which
-XNoStarInType
changes the semantics. For example, this code from the
hashable
library
newtype Tagged (s :: * -> *) = Tagged {unTagged :: Int}
would fail to compile with the following error:
Data/Hashable/Generic.hs:116:22: error:
Operator applied to too few arguments: *
With NoStarIsType (implied by TypeOperators), ‘*’ is treated as a regular type operator.
Did you mean to use ‘Type’ from Data.Kind instead?
|
116 | newtype Tagged (s :: * -> *) = Tagged {unTagged :: Int}
|
Many other libraries in the wild simultaneously enable -XTypeOperators
and use
*
as a kind, including servant, aeson, cereal, cassava, and others, so
including 4.f would break all of these libraries. While not having 4.f also
results in some breakage, far fewer libraries in the wild break without 4.f
than with 4.f, so this was ultimately decided against.
If -XTypeOperators
were to imply -XNoStarIsType
, then any code which
uses *
as kind instead of a binary operator would have to migrate somehow.
Two migration options are:
Declare
-XStarIsType
. If they ever use*
as a binary operator, those uses would have to be qualified with a module prefix.Import
Type
fromData.Kind
and change uses of*
toType
. If they already have aType
in scope, they may have to use qualified imports, etc.
Unresolved questions¶
Is this the right deprecation schedule? Is it moving too fast?
What is the educational impact of this proposal? Specifically,
-XPolyKinds
is now bigger and harder to learn. On the other hand, the previous implementation of-XPolyKinds
has some restrictions that may not have been obvious to users.What do we want the long-term future of
*
to be? I favor removing it after a long time (> 5 years). But deciding now what we want to have in the distant future can influence decisions made in the meantime. One particular decision: should-Wcompat
warn on uses of*
asType
? Relatedly, should there be a plan to deprecate-XStarIsType
?Regardless of the long-term future of
*
, is the migration path described around-XStarIsType
the best possible path? Notably, the current migration path will cause breakage in-XTypeOperators
code that uses*
as a kind, requiring users to change all uses of*
toType
when upgrading GHC. David Feuer has expressed unease at the migration path detailed here, but his counter-suggestion remains unclear to me. I am not without unease myself, but I don’t see a better way.
Summary of discussion¶
Much (just about all, really) of the discussion surrounds the future of *
. I’ve made
my case in the comments for eventually deprecating and removing it, though I’ve been
convinced by the -XStarIsType
plan (which grew out of the discussion) that supporting
*
into perpetuity isn’t so terrible, and that we should plan to keep it around for
years more. One vocal participant, @AntC2, has strenuously objected to any move toward
removing *
, but their points have not been echoed by anyone else in the discussion.
In particular, @AntC2 is worried about rotting of educational resources, something I was
perhaps too glib about in earlier versions of this proposal. I expect the committee will
carry on this debate, and I’m happy to submit to the view of the committee on this matter.
Other discussion concerns the details of the migration path and the -XStarIsType
aspect
of this proposal, briefly summarized in the last unresolved question, above.
Implementation Plan¶
I or a close collaborator volunteers to implement.