#11080: Open data kinds -------------------------------------+------------------------------------- Reporter: dmcclean | Owner: Type: feature | Status: new request | Priority: low | Milestone: Component: Compiler | Version: Keywords: | Operating System: Unknown/Multiple Architecture: | Type of failure: None/Unknown Unknown/Multiple | Test Case: | Blocked By: Blocking: | Related Tickets: Differential Rev(s): | Wiki Page: -------------------------------------+------------------------------------- When we need type level symbols, we used to only have one option, `EmptyDataDecls`. The symbolic type parameters would be given kind `*`, but the convention would be to use types that are (mostly) uninhabited and that were made for the purpose of serving as symbols. For an example of this see http://hackage.haskell.org/package/servant-0.4.4.5/docs/Servant- API-ContentTypes.html. Now we also have the `Symbol` kind which can serve a similar purpose. Neither of these options is fully satisfactory for examples like servant's type-level encoding of content types, or the `units` libraries type-level encoding of physical dimensions, for the following reasons: We would prefer to give these types a kind other than `*` both because they are uninhabited and because we wish to provide documentation of what types are acceptable in these parameter positions. But the only facility we have for creating new kinds is `DataKinds`, and the kinds it creates are all closed. This is problematic because we wish to allow client modules to declare new content types or new physical dimensions. We could provide "newkind" wrappers around `Symbol` using `DataKinds`, but that runs in to name collision issues. The `EmptyDataDecls` solution is superior here because types with the same name declared in different modules remain distinct. Instead I propose the addition of a new feature where data kinds can be open. In a discussion at https://github.com/bjornbm/dimensional-dk/issues/96 in which @goldfire participated, we arrived at the following proposal for concrete syntax, but certainly there are many possible variations one could imagine which might have equal or greater merit: {{{#!hs -- declares a new kind which initially has no inhabitants data open ContentType -- declares a new type of kind ContentType, which is distinct -- from any others that may have been declared elsewhere, -- even if they have the same non-module-qualified name data constructor JSON :: ContentType }}} (@goldfire raised the possibility of one day interpreting the same `data constructor ...` syntax at the type level to declare inhabited types for which some constructors are defined in one module but which are open to extension with new constructors by other modules, but that is a distinct issue in all other ways apart from possibly wishing to share syntax.) -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11080 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler