Note that we also have #6024 (and its wiki page [[wiki:GhcKinds/KindsWithoutData]]), which is about implementing close data kinds without the need for declaring a data type. Can we implement
#11080: Open data kinds -------------------------------------+------------------------------------- Reporter: dmcclean | Owner: jstolarek Type: feature request | Status: new Priority: low | Milestone: Component: Compiler | Version: Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: #6024 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by goldfire): Replying to [comment:6 jstolarek]: this and #6024 at the same time? It seems to me that the answer is yes. Agreed. That would be nice.
Here is my proposal for the syntax: ...
This syntax would steal `kind` as a keyword. Do we feel bad about it?
I think it's easily avoidable, by just writing `data kind`. Using just `kind` here could be confusing, because your `kind` is not at all analogous to Haskell's `type`.
Also, I don't like `data constructor` syntax. I find it misleading as data constructor is a totally different thing than what we are declaring (in fact, in #6024 we specifically wish to avoid creating data constructors).
We are precisely declaring a data constructor. It's just a data constructor that makes compile-time data. I recognize that others may usefully disagree about the meaning of a data constructor here, but I really to think that these are data constructors. (Compare to what other dependently typed languages do.)
If we made this into a separate language extension, I wonder if that
extension would have to be enabled only in modules that declare kinds or also in the ones that use them? Only at declaration sites. Infectious extensions are annoying.
... If this was what dreixel meant then I disagree with it.
I agree with you. `* :: *` does not obviate this or #6024.
Another question related to `* :: *` is about namespace collision. If I
say:
{{{#!hs -- assume DataKinds are enabled, so that C becomes a type data T = C }}}
Ah. But `C` does not become a type. `C` lives in the data namespace. It's just that the renamer looks in both the type namespace and then the data namespace. `C` is always just a data constructor, even when used in a type.
{{{ kind K = T | C }}} do we have collisions beetwen definitions of `T`s and `C`s? They are all in namespace of types. On the other hand they could be disambiguated by kind, but I'm not sure if this is acceptable.
You are suggesting type-directed name resolution. That's a bigger pickle than we need to crack at the moment.
Aside: if we can index kinds does this mean we have sort polymorphism?
No no no. We have type polymorphism. And that's it. There are no kinds and no sorts. Just types. We humans have small brains and it is thus helpful to use both kind and type in speech to keep the ideas apart. But the terms are now truly synonymous. So, a type that classifies a type can be indexed, perhaps polymorphically. But let's not call it sort polymorphism. :)
I will work on extending [[wiki:GhcKinds/KindsWithoutData]] wiki page,
as I think this discussion belongs there (even if closed and open kinds should be implemented separately). Yell if you think otherwise. Fine by me. Thanks! -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11080#comment:7 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler