[GHC] #8090: MetaKinds - PolyKinds generalization
GHC
ghc-devs at haskell.org
Fri Jul 26 10:31:56 CEST 2013
#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
More information about the ghc-tickets
mailing list