[GHC] #8090: MetaKinds - PolyKinds generalization

[GHC]

#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