#11080: Open data kinds -------------------------------------+------------------------------------- Reporter: dmcclean | Owner: 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: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by goldfire): Simon PJ, Stephanie Weirich, Andres Löh, Kenny Foner, and I discussed this recently, and we didn't spot any problems with the proposal, neither in terms of theory nor implementation. * Question: can open kinds be parameterized? Answer: Yes. Example: {{{ data open Dimension :: * data constructor Length :: Dimension data open Unit :: Dimension -> * data constructor Meter :: Unit 'Length data constructor Foot :: Unit 'Length }}} * Alternative syntax: `data constructor` is noisy. Just omit, allowing a declaration like `Length :: Dimension`. Objection: this overlaps with a naked top-level Template Haskell splice. * Alternative syntax: `data constructor` is noisy. How about this: {{{ data open Unit :: * data extension Unit where Meter :: Unit Foot :: Unit }}} My (Richard's) objection: But this grouping of `Meter` and `Foot` is meaningless. Breaking up the group is the same as grouping. It's just syntactic. But this isn't a hard objection if others like the idea. * Related topic: What about other design points as explored in comment:6:ticket:9840? In particular, how does this relate to non- generative, non-injective symbols whose equational theory is given by a plugin? (Non-generative, non-injective symbols whose equational theory is given by GHC are known as type families.) Defining such a symbol was the point of #9840 to begin with, and we settled on an empty closed type family as the nearest approximation. After some discussion, it seemed that the open kind proposal was separate enough that these don't need to be considered together. But a suggestion for a unifying syntax would be welcome! Bottom line: let's do it, once we decide on a syntax. I still favor the syntax proposed, with `data constructor`. Other opinions are welcome. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11080#comment:2 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler