[Haskell-cafe] Promoting associated data types

[Kosyrev Serge]

Richard Eisenberg <eir at cis.upenn.edu> writes:
> 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.