Specifying Kinds of Types

Ashley Yakeley ashley@semantic.org
Fri, 8 Feb 2002 03:26:09 -0800


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 '(* -> *) -> (* -> *) -> * -> *'.

It's not currently possible to specify kinds, is it? Actually I think 
polymorphic kinds would be nice, but I can't say I desperately need them. 
I'd just like to be able to specify kinds somehow. For instance:

    data CMap0 (p ::: * -> *) (q ::: * -> *) = MkCMap0;

...or perhaps

    data ({* -> *} p,{* -> *} q) => CMap0 p q = MkCMap0;

...or whatever.


-- 
Ashley Yakeley, Seattle WA