#8090: MetaKinds - PolyKinds generalization -------------------------------------+------------------------------------ Reporter: wvv | Owner: Type: feature request | Status: closed Priority: normal | Milestone: Component: Compiler | Version: 7.6.3 Resolution: invalid | Keywords: Operating System: Unknown/Multiple | Architecture: Unknown/Multiple Type of failure: None/Unknown | Difficulty: Unknown Test Case: | Blocked By: Blocking: | Related Tickets: -------------------------------------+------------------------------------ Changes (by carter): * status: new => closed * resolution: => invalid Comment: Hey wvv, We really appreciate your enthusiasm and interest. But type system design discussions on GHC Trac generally take one of the following forms (not always, but most of the time): 1. someone has concocted a snippet of haskell code that uses a combination of type system features that results in an unsoundness issue that needs be fixed, and which often can often some substantial research time to come to a satisfactory solution. A good example of this that looks to be getting a fix soon is Newtype Deriving based unsoundness issues, which I believe has necessitated the creation of "Role" types, though I've not read up on them closely as yet. 2. An extension of the type system that increases the expressive power of the GHC Haskell Type system, where this proposed extension has already been proven to be SOUND, as well as a clear translation into to the type calculus that GHC reduces are the language constructs to internally. A great example of this is Richard's (Goldfire's) recent (exciting) work on closed type families. Phrased differently, before a type system extension can be proposed (and be seriously considered for inclusion): IDEALLY , there must be a clear formal model (not just some examples in a notation that is under specified), proofs of type soundness for that formal model, a clear type preserving translation into the current GHC core calculus (or a minimal extension thereof), and also a compelling case that motivates the type system extension as accomplishing some blend of increased type safety and increased programmer/program expressivity (ideally both!). your proposal is a variant of type universes, and GHC haskell has a sufficiently sophisticated rich type system that theres MANY subtleties to adding such to GHC / haskell. Indeed, two distinct research groups are currently exploring ways to soundly add type universe like machinery to GHC. wvv, a better fora for you nascent type system design ideas would be #haskell irc on freenode, or the haskell-cafe mailing list. Many of the community members would be happy to give you feedback on your ideas, and/or suggested reading to help you come up with even better ones! GHC Trac is not the right forum for this conversation, accordingly I am closing this ticket, look forward to seeing the conversations that ensue on the mailing lists and irc! -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/8090#comment:7 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler