Specifying Kinds of Types

RijkJ.C.vanHaaften RijkJ.C.vanHaaften
Fri, 08 Feb 2002 12:39:30 +0100


Ashley Yakeley wrote:
>I'd like to be able to declare the kinds of new types and synonyms,
>because sometimes Haskell can't infer them. For instance:
>
>     data CMap0 p q = MkCMap0;
>
>Without evidence, Haskell assumes that p and q have kind '*' (as per sec.
>4.6), and therefore CMap0 has kind '* -> * -> *'. Actually, I wanted p
>and q to both have kind '* -> *', giving CMap0 kind '(* -> *) -> (* -> *)
>-> *'.
...
>It's not currently possible to specify kinds, is it?

It is possible using a trick due to John Hughes. In
     Proceedings of the 1999 Haskell Workshop,
he wrote in his article
     Restricted Data Types in Haskell
this note:

      3 There is one unpleasant hack in the figure: The constructor Unused 
in the
     data type definition for Set. It is there purely in order to force the 
compiler
     to assign the parameter cxt the correct kind: without it, cxt does not 
appear
     at all in the right hand side of the definition, and is therefore 
assigned the
     (incorrect) kind *. The application cxt a forces the correct kind * -> 
* to be
     assigned, and embedding it in the type cxt a -> () prevents the type 
of the
     context from interfering with the derivation of a Show instance.

The figure mentioned contains

     data Set cxt a = Set [a] | Unused (cxt a -> ()) deriving Show

You can follow the example of John, writing

data CMap0 p q = MkCMap0 | Unused (p a -> ()) (q a -> ());

(I think I'm correctly applying the trick, but other
Proceedings-readers will correct me if I'm wrong.)

As John writes, this is a hack, but we have no
other choice.

Rijk-Jan van Haaften