[GHC] #11080: Open data kinds

11 Nov 2015

      #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

GHC

GHC

GHC

GHC

GHC

GHC

GHC

GHC

GHC

GHC

GHC

GHC

GHC

GHC

GHC

GHC

GHC

GHC

GHC

tags

participants (1)