#8090: MetaKinds - PolyKinds generalization -------------------------------------+------------------------------------ Reporter: wvv | Owner: Type: feature request | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.6.3 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Unknown/Multiple Type of failure: None/Unknown | Difficulty: Unknown Test Case: | Blocked By: Blocking: | Related Tickets: -------------------------------------+------------------------------------ Comment (by wvv): MetaKinds could be name as RankNKinds -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/8090#comment:1 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#8090: MetaKinds - PolyKinds generalization -------------------------------------+------------------------------------ Reporter: wvv | Owner: Type: feature request | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.6.3 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Unknown/Multiple Type of failure: None/Unknown | Difficulty: Unknown Test Case: | Blocked By: Blocking: | Related Tickets: -------------------------------------+------------------------------------ Comment (by wvv): 1) This is a part of lambda-cube. {{{ Agda Haskell Set0 a::* Set1 a::k <<==>> a :: (k :: *) Set2 a :: (k2 :: (k :: *)) ... }}} 2) rankNkinds is essential to work with rank(N-1)kinds: classes and (G)ADTs. We already have a lot of rank2kinds(PolyKinds), so we already need to have rank3kinds. Developers said they did new Typeable in GHC 7.8, but it is impossible to write {{{ data Foo (a::(b::k)->*) deriving Typeable }}} new Typeable = Typeable2kinds; but Foo is a part of Typeable3kinds 3) I think for several years max rank kind = 7 is enough (Bill Gates said "640K ought to be enough for anybody") -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/8090#comment:3 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#8090: MetaKinds - PolyKinds generalization -------------------------------------+------------------------------------ Reporter: wvv | Owner: Type: feature request | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.6.3 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Unknown/Multiple Type of failure: None/Unknown | Difficulty: Unknown Test Case: | Blocked By: Blocking: | Related Tickets: -------------------------------------+------------------------------------ Comment (by goldfire): To remove ambiguity, I'll adopt the "many stars" notation. If we assume an infinite hierarchy of classifications ("sorts") (and a right-associative ::), we have {{{ True :: Bool :: * :: ** :: *** :: **** :: ... }}} We currently have mono-kinded type variables {{{(a :: *)}}} and poly- kinded type variables {{{(a :: k :: **)}}. If we have the next level, {{{(a :: k :: m :: ***)}}}, what useful value could {{{m}}} have other than {{{**}}}? My understanding is that, in this scenario, any value other than {{{**}}} for {{{m}}} would mean that the kind `k` would be empty -- that is, `a` wouldn't exist. I still don't see where this extension would be helpful. For example, you propose this type: {{{ data Foo (a::(b::k)->*) }}} What would its right-hand side look like? -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/8090#comment:5 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#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