Ross Paterson | 25 Jan 16:19 2013
Picon

data kinds

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.
José Pedro Magalhães | 25 Jan 16:22 2013
Picon

Re: data 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 <at> 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 <at> haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users

_______________________________________________
Glasgow-haskell-users mailing list
Glasgow-haskell-users <at> haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
John Meacham | 27 Jan 03:11 2013
Picon

Re: data kinds


On Fri, Jan 25, 2013 at 7:19 AM, Ross Paterson <ross <at> 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 <at> haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Iavor Diatchki | 27 Jan 03:54 2013
Picon

Re: data kinds

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 <at> repetae.net> wrote:

On Fri, Jan 25, 2013 at 7:19 AM, Ross Paterson <ross <at> 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 <at> haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users


_______________________________________________
Glasgow-haskell-users mailing list
Glasgow-haskell-users <at> haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Erik Hesselink | 27 Jan 09:02 2013
Picon

Re: data kinds

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 <at> haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Edward Kmett | 27 Jan 23:28 2013
Picon

Re: data kinds

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 <at> 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 <at> haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users


_______________________________________________
Glasgow-haskell-users mailing list
Glasgow-haskell-users <at> haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users

Gmane