[ghc-steering-committee] Proposal: Top-level kind signatures (#54)

[Simon Peyton Jones]

I’m strongly in favour of #54.   The current CUSK stuff is a huge mess.  The inability to write a kind signature for a type constructor is terrible.

One minor point that isn't clear to me: the proposal says that "Associated types may be given kind signatures within their classes". Are type variables mentioned in the class head visible in the kind signature for the associated type?

Good point.  I was going to say “behave like GADTs” where the variables in the header do not scope over the signatures; but unfortunately in class decls the variables in the header *do* scope over the (term-level) signatures.

Richard, what do you think?  Maybe associated types should only be given kind signatures at the top level (alongside the kind signature for the class).  That would at least be clear.

Simon

From: ghc-steering-committee <ghc-steering-committee-bounces at haskell.org> On Behalf Of Roman Leshchinskiy
Sent: 09 August 2018 20:46
To: ghc-steering-committee at haskell.org
Subject: [ghc-steering-committee] Proposal: Top-level kind signatures (#54)

Hi everyone,

The proposal is about adding stand-alone kind signatures for type declarations:

  https://github.com/ghc-proposals/ghc-proposals/pull/54<https://na01.safelinks.protection.outlook.com/?url=https%3A%2F%2Fgithub.com%2Fghc-proposals%2Fghc-proposals%2Fpull%2F54&data=02%7C01%7Csimonpj%40microsoft.com%7Cb58b9c99576e4727d9b808d5fe30c0a1%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C0%7C636694407703047991&sdata=%2Fw6%2F%2B57ofExBMZUoAU%2FfFOpfzIDoRGpsxoUScDx6xyw%3D&reserved=0>

The basic idea is to add support for kind signatures like this:

type T :: Type -> Type -> Type
data T a b = ...

Signatures would be introduced by the keyword 'type' and could be provided for data types, type synonyms, type families and classes. The extension would be enable via -XTopLevelKinds.

Additionally, complete user-supplied kind signatures (CUSKs, see https://downloads.haskell.org/~ghc/latest/docs/html/users_guide/glasgow_exts.html#complete-user-supplied-kind-signatures-and-polymorphic-recursion<https://na01.safelinks.protection.outlook.com/?url=https:%2F%2Fdownloads.haskell.org%2F~ghc%2Flatest%2Fdocs%2Fhtml%2Fusers_guide%2Fglasgow_exts.html%23complete-user-supplied-kind-signatures-and-polymorphic-recursion&data=02%7C01%7Csimonpj%40microsoft.com%7Cb58b9c99576e4727d9b808d5fe30c0a1%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C0%7C636694407703047991&sdata=lLCdw6ejJEa7iUVKRxh14yuQBjHkLjGDOHb9LtzfXQc%3D&reserved=0>) would be given a separate language extension, -XCUSKs which would be on by default for now but turned off in GHC 8.8 and then deprecated and removed.

The proposal depends on #81.

Feedback has been positive and this is rather cleaner than the current story so I'm in favour of accepting this.

Like Richard, I'm not really happy with the name "TopLevelKinds", especially since signatures for associated types aren't even on the top level. Would something like StandAloneKinds or ExplicitKindSignatures be better?

One minor point that isn't clear to me: the proposal says that "Associated types may be given kind signatures within their classes". Are type variables mentioned in the class head visible in the kind signature for the associated type?

Thanks,

Roman

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/ghc-steering-committee/attachments/20180817/b02f3c95/attachment.html>