Re: data kinds

2013-01-27 Thread Erik Hesselink

 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


Re: data kinds

2013-01-26 Thread John Meacham
On Fri, Jan 25, 2013 at 7:19 AM, Ross Paterson r...@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


Re: data kinds

2013-01-26 Thread Iavor Diatchki
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 j...@repetae.net wrote:


 On Fri, Jan 25, 2013 at 7:19 AM, Ross Paterson r...@soi.city.ac.ukwrote:

 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


___
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users


data kinds

2013-01-25 Thread Ross Paterson
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


Re: data kinds

2013-01-25 Thread José Pedro Magalhães
See http://hackage.haskell.org/trac/ghc/wiki/GhcKinds/KindsWithoutData


Cheers,
Pedro

On Fri, Jan 25, 2013 at 3:19 PM, Ross Paterson r...@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

___
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users