GitLab

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:

-- 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.)

Trac metadata

Trac field	Value
Version
Type	FeatureRequest
TypeOfFailure	OtherFailure
Priority	low
Resolution	Unresolved
Component	Compiler
Test case
Differential revisions
BlockedBy
Related
Blocking
CC	goldfire
Operating system
Architecture