Specifying Kinds of Types

[Zhanyong Wan]

Hi Ashley,

If you don't want to build ghc, or would rather use hugs, here's a (dirty)
trick which John Hughes used in his "restricted data types" paper (I hope I
recall correctly) to specify kinds.

For your first example, you can write:

data CMap0 p q = MkCMap0
        | CMap0_Unused (p Int) (q Int)

The idea is that you never use the CMap0_Unused branch, but it tells
Haskell that p and q have kind * -> *.  Your code would become less
efficient if what you had was a newtype.

For your second example, you have to turn it into a data declaration:

data Composer c = Composer (forall x y z. (c y z) -> (c x y) -> (c x z))
  | Composer_Unused (c [] [])

Of course, you cannot insist on Composer being a type synonym any more.  Is
this solution acceptable to you?

- Zhanyong Wan

Simon Peyton-Jones wrote:

> OK, it's done.  In GHC you can specify kinds in
> [...]
>
>
> And you can put kind signatures on arbitrary types, rather
> like you can put type signatures on arbitrary expressions.
>
> No kind polymorphism though!
>
> All this is in the HEAD.  You'll need to build from source to get it
> until we make a release.

> | 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 '(* -> *)
> | -> (* -> *)
> | -> *'.
> |
> | Here's another example:
> |
> |     type Composer c = forall x y z. (c y z) -> (c x y) -> (c x z);
> |
> | Haskell gives x, y and z all the kind '*'. But I wanted them
> | to have kind
> | '* -> *', giving c the kind '(* -> *) -> (* -> *) -> *' and
> | Composer the
> | kind '(* -> *) -> (* -> *) -> * -> *'.