#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