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
Ashley Yakeley wondered: | 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; | | Actually, I wanted p and q to both have kind '* -> *'. The following workaround might be useful in this case: data CMap0 p q = MkCMap0 | DummyConstructor (p Int) (q Int) But that doesn't help with the following example: | type Composer c = forall x y z. (c y z) -> (c x y) -> (c x z); | | [..x..y..z..] But I wanted them to have kind '* -> *'. Here, you might do the following trick: type HasKind_Help x dummy = x type HasKind_Star_To_Star x = HasKind_Help x (x Int) type C c x y = c (HasKind_Star_To_Star x) (HasKind_Star_To_Star y) type Composer c = forall x y z . C c y z -> C c x y -> C c x z (not tested!) There might be an easier workaround, too, but you get the idea. /Koen. -- Koen Claessen http://www.cs.chalmers.se/~koen Chalmers University, Gothenburg, Sweden.
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
On Fri, Feb 08, 2002 at 12:39:30PM +0100, Rijk J.C.van Haaften wrote:
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.
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 [...]
data Set cxt a = Set [a] | Unused (cxt a -> ()) deriving Show
Another kludge, that works with newtypes too, is type Hint a b = a newtype Set cxt a = Set (Hint [a] (cxt a)) deriving Show
I'd like to be able to declare the kinds of new types and synonyms, because sometimes Haskell can't infer them.
The kind inferencer normally works quite well in Haskell. Only when you use phantom types (ie. unused type variables), you sometimes have to guide the kind inferencer -- either with phantom constructors (ie. unused constructors) or phantom type defintions in the case of newtypes. Allthough not described, we used this trick extensively in Haskell/DB in order to force phantom types into the T-REX kind "Row". (http://www.cs.uu.nl/~daan/papers/dsec.ps) All the best, Daan.
participants (5)
-
unknown＠example.com -
Ashley Yakeley -
Daan Leijen -
Koen Claessen -
Ross Paterson