[Haskell-cafe] Type-Level Programming

[wren ng thornton]

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