data kinds

Ross Paterson ross at
Fri Jan 25 16:19:13 CET 2013

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.

More information about the Glasgow-haskell-users mailing list