[GHC] #11080: Open data kinds

[GHC]

#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]:
 > 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
 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