[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:                    |
-------------------------------------+-------------------------------------
Changes (by jstolarek):

 * owner:   => jstolarek
 * related:   => #6024


Comment:

 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.

 Here is my proposal for the syntax:

 {{{#!hs
 -- (1) closed kinds, normal syntax
 kind Universe = Sum  Universe Universe
               | Prod Universe Universe
               | K *

 -- (2) closed kinds, GADT syntax.
 kind Universe where
    Sum  :: Universe -> Universe -> Universe
    Prod :: Universe -> Universe -> Universe
    K    :: *                    -> Universe

 -- (3) open kinds
 kind Universe
 kind instance Sum  :: Universe -> Universe -> Universe
 kind instance Prod :: Universe -> Universe -> Universe
 kind instance K    :: *                    -> Universe
 }}}

 This syntax would steal `kind` as a keyword. Do we feel bad about it?
 Importantly, do we put this new feature into its own language extension or
 do we make it part of `DataKinds`? If the former then I don't feel bad
 about stealing `kind`, as we won't break any of the existing code. But if
 we put this into `DataKinds` then I might reconsider my preference for
 syntax. Then again I still would rather break backwards compatibility and
 have nice syntax then construct verbose syntax for the sake of backwards
 compatibility.  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).

 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?

 How does this feature interact with `* :: *`? In #6024 dreixel says: "[in
 the future] types and kinds might be collapsed into a single level. That
 would also destroy the possibility of doing what is asked in this ticket,
 though." I believe that dreixel's line of reasoning was this:

 > When we declare `kind K = T`, then `K` is a kind a `T` is a type. But
 since types and kinds are now the same then we must be able to treat `K`
 as a type, which makes `T` a value and thus we arrived at declaring a data
 type.

 If this was what dreixel meant then I disagree with it. It's like saying
 that since `Int :: *`, then `*` can be treated as a type and thus `Int`
 can be treated as a value (whatever that would mean).

 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

 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.

 Aside: if we can index kinds does this mean we have 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.

--
Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/11080#comment:6>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler