Richard Eisenberg
Your second example, though, is ill-formed: you can't have a type variable of kind `D`, as `D`, by itself, isn't a kind. You could say this, if you wanted, though:
class C1 a (b :: D a)
Do you have an use case for this? I'm always curious to see how Haskellers want to use these advanced features!
You are probably going to be disappointed -- I'm actually trying to model some kind of stereotypical OO type hierarchy. Basically, I have a known finite set of Categories (in a non-mathematical sense) of data, that I insist on modeling as a type class [1]. Each Category has a number of highly-custom Layouts capable of representing its data. Due to my irrational stubbornness, I insist on modeling them as type classes as well. I'm also trying to preserve as much user-extensibility, as I can -- through type class instancing. (Which seemingly inevitably leads to existential wrappers -- which is widely discouraged, but, for now, let's forget about this.) So, two type classes for Categories and Layouts -- this gives rise to two indices, a total of four types. For indexing the Category type class I can use a regular promoted ADT:
data CatName = Graph | Dag | Set deriving (Eq)
class Category (a ∷ CatName) where data CatX a ∷ *
..which suddenly allows to do something I couldn't figure out how to do without XDataKinds -- a simple decision procedure over a list of existentials:
data CatEntry where CatEntry ∷ Category a ⇒ (a, (CatX a)) → CatEntry
data CatAssoc where CatAssoc ∷ [CatEntry] → CatAssoc
prefer ∷ Category c ⇒ c → CatEntry → CatX c → CatX c prefer cat (CatAssoc xs) defx = case find (\(CatEntry (icat, _)) → cat == icat) xs of Just (CatEntry (icat, x)) → x Nothing → defx
Basically, DataKinds allows constraining the type class index, so that its members become directly comparable. ..however. There seems to be a need to go further, and to extend the same trick to Layouts -- remember that I need to index them as well -- so let me revisit the definition of Category (and elucidate the nature of CatX along the way):
class Category (a ∷ CatName) where data LayoutName a ∷ *
class Category cat ⇒ Layout cat (lay ∷ LayoutName cat) | lay → cat where
..which suddenly explains the meaning of 'prefer' -- a choice function for layouts:
data CatEntry where CatEntry ∷ Category a ⇒ (a, (LayoutName a)) → CatEntry
prefer ∷ Category c ⇒ c → CatEntry → LayoutName c → LayoutName c prefer cat (CatAssoc xs) deflayout = case find (\(CatEntry (icat, _)) → cat == icat) xs of Just (CatEntry (icat, lay)) → lay Nothing → deflayout
..but, of course, that can't be done yet : -) So, in the end, I'm trading off extensibility for ability to quantify over the type index. I'm not sure if I will need the quantification part in the end, but I sure as hell would like to have the choice : -) -- respectfully, Косырев Серёга -- 1. The why of type class choice is a separate question, and my reasoning is likely highly debatable. Let's assume it's aesthetics/usability, for now.