Specifying Kinds of Types
Mon, 11 Feb 2002 11:44:59 -0500
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 '(* -> *) -> (* -> *) -> * -> *'.