GHC implements data kinds by promoting data declarations of a certain restricted form, but I wonder if it would be better to have a special syntax for kind definitions, say data kind Nat = Zero | Succ Nat At the moment, things get promoted whether you need them or not, and if you've made some mistake that makes your definition non-promotable you don't find out until you try to use it. More importantly, a separate form for kinds would allow one to use existing kinds, i.e. *, in definitions of new kinds.
See http://hackage.haskell.org/trac/ghc/wiki/GhcKinds/KindsWithoutData Cheers, Pedro On Fri, Jan 25, 2013 at 3:19 PM, Ross Paterson <ross@soi.city.ac.uk> wrote:
GHC implements data kinds by promoting data declarations of a certain restricted form, but I wonder if it would be better to have a special syntax for kind definitions, say
data kind Nat = Zero | Succ Nat
At the moment, things get promoted whether you need them or not, and if you've made some mistake that makes your definition non-promotable you don't find out until you try to use it.
More importantly, a separate form for kinds would allow one to use existing kinds, i.e. *, in definitions of new kinds.
_______________________________________________ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
On Fri, Jan 25, 2013 at 7:19 AM, Ross Paterson <ross@soi.city.ac.uk> wrote:
GHC implements data kinds by promoting data declarations of a certain restricted form, but I wonder if it would be better to have a special syntax for kind definitions, say
data kind Nat = Zero | Succ Nat
This is exactly the syntax jhc uses for user defined kinds. John
Hello, I think that it'd be really useful to be able to just declare a `kind` without having to promote a datatype. When we discussed this last time (summarized by the link Pedro sent, I think) it came up that it might be nice to also have kind synonyms, which would be analogous to type synonyms, but one level up. The "natural" syntax for that would be to have a "type kind" declaration, but this seems a bit confusing... John, did you implement kind synonyms in jhc, and if so what syntax did you use? -Iavor On Sat, Jan 26, 2013 at 6:11 PM, John Meacham <john@repetae.net> wrote:
On Fri, Jan 25, 2013 at 7:19 AM, Ross Paterson <ross@soi.city.ac.uk>wrote:
GHC implements data kinds by promoting data declarations of a certain restricted form, but I wonder if it would be better to have a special syntax for kind definitions, say
data kind Nat = Zero | Succ Nat
This is exactly the syntax jhc uses for user defined kinds.
John
_______________________________________________ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
When we discussed this last time (summarized by the link Pedro sent, I think) it came up that it might be nice to also have kind synonyms, which would be analogous to type synonyms, but one level up. The "natural" syntax for that would be to have a "type kind" declaration, but this seems a bit confusing...
What about just 'kind'? It's symmetric with 'type'. Erik
This has the problem that kind is currently a valid function name, so it would take a new keyword, or at least on conditional on the DataKinds extension. -Edward On Sun, Jan 27, 2013 at 3:02 AM, Erik Hesselink <hesselink@gmail.com> wrote:
When we discussed this last time (summarized by the link Pedro sent, I
think) it came up that it might be nice to also have kind synonyms, which would be analogous to type synonyms, but one level up. The "natural" syntax for that would be to have a "type kind" declaration, but this seems a bit confusing...
What about just 'kind'? It's symmetric with 'type'.
Erik
_______________________________________________ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
participants (6)
-
Edward Kmett -
Erik Hesselink -
Iavor Diatchki -
John Meacham -
José Pedro Magalhães -
Ross Paterson