Skip to content

GitLab

  • Menu
Projects Groups Snippets
    • Loading...
  • Help
    • Help
    • Support
    • Community forum
    • Submit feedback
  • Sign in / Register
  • GHC GHC
  • Project information
    • Project information
    • Activity
    • Labels
    • Members
  • Repository
    • Repository
    • Files
    • Commits
    • Branches
    • Tags
    • Contributors
    • Graph
    • Compare
    • Locked Files
  • Issues 4,836
    • Issues 4,836
    • List
    • Boards
    • Service Desk
    • Milestones
    • Iterations
  • Merge requests 457
    • Merge requests 457
  • CI/CD
    • CI/CD
    • Pipelines
    • Jobs
    • Schedules
    • Test Cases
  • Deployments
    • Deployments
    • Releases
  • Analytics
    • Analytics
    • CI/CD
    • Code review
    • Insights
    • Issue
    • Repository
    • Value stream
  • Wiki
    • Wiki
  • Snippets
    • Snippets
  • Activity
  • Graph
  • Create a new issue
  • Jobs
  • Commits
  • Issue Boards
Collapse sidebar
  • Glasgow Haskell Compiler
  • GHCGHC
  • Issues
  • #11080

Closed
Open
Created Nov 11, 2015 by dmcclean@trac-dmcclean

Open data kinds

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
To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information
Assignee
Assign to
Time tracking