Andrew Coppin wrote:
I did wonder what the heck a "type function" is or why you'd want one. And then a while later I wrote some code along the lines of
class Collection c where type Element c :: * empty :: c -> Bool first :: c -> Element c
So now it's like Element is a function that takes a collection type and returns the type of its elements - a *type function*.
Suddenly the usual approach of doing something like
class Collection c where empty :: c x -> Bool first :: c x -> x
seems like a clumsy kludge, and the first snippet seems much nicer. (I gather that GHC's implementation of all this is still "fragile" though? Certainly I regularly get some very, very strange type errors if I try to use this stuff...)
Adding type functions introduces a lot of theoretical complexity to the type system. It's very easy to end up loosing decidability of type inference/checking, not giving the power/properties you want, or both. I get the impression that folks are still figuring out exactly how to balance these issues in Haskell. For example, should type functions be injective (i.e. (F x = F y) ==> (x = y)) or not? If we make them injective then that rules out writing non-injective functions. But if we don't, then we cripple the type inferencer. This is why there's a distinction between associated datatypes (injective) vs associated type aliases (not).
the only kinds available are * and (k1 -> k2)
Does # not count?
The other kinds like #, ?, and ?? are just implementation details in GHC. By and large they are not theoretically significant. Also, other compilers (e.g. jhc) have different kinding systems for optimizations. Some folks have advocated for distinguishing the kind of proper types from the kind of type indices. This is theoretically significant, and I think it's a fabulous idea. But it hasn't been implemented AFAIK. -- Live well, ~wren