Claus Reinke:
type family F a :: * -> * .. We made the design choice that type functions with a higher-kinded result type must be injective with respect to the additional paramters. I.e. in your case: F x y ~ F u v <=> F x ~ F u /\ y ~ v
i'm still trying to understand this remark:
- if we are talking about "type functions", i should be allowed to replace a function application with its result, and if that result doesn't mention some parameters, they shouldn't play a role at any stage, right?
- if anything other than the function result matters, isn't it somewhat misleading to speak of "type functions"?
You will notice that I avoid calling them "type functions". In fact, the official term is "type families". That is what they are called in the spec http://haskell.org/haskellwiki/GHC/Type_families and GHC's option is -XTypeFamilies, too. More precisely, they are "type-indexed type families". One difference between type families and (value-level) functions is that not all parameters of a type family are treated the same. A type family has a fixed number of type indicies. We call the number of type indicies the type family's arity and by convention, the type indicies come always before other type parameters. In the example type family F a :: * -> * F has arity 1, whereas type family G a b :: * has arity 2. So, the number of named parameters given is the arity. (The overall kind is still F :: * -> * -> *; ie, the arity is not obvious from the kind, which I am somewhat unhappy about.) In other words, in a type term like (F Int Bool), the two parameters Int and Bool are treated differently. Int is treated like a parameter to a function (which is what you where expecting), whereas Bool is treated like a parameter to a vanilla data constructor (the part you did not expect). To highlight this distinction, we call only Int a type index. Generally, if a type family F has arity n, it's first n parameters are type indicies, the rest are treated like the parameters of any other type constructor. Moreover, a type family of arity n, must always be applied to at least n parameters - ie, applications to type indicies cannot be partial. This is not just an arbitrary design decision, it is necessary to stay compatible with Haskell's existing notion of higher-kinded unification (see, Mark Jones' paper about constructor classes), while keeping the type system sound. To see why, consider that Haskell's higher-kinded type system, allows type terms, such as (c a), here c may be instantiated to be (F Int) or Maybe. This is only sound if F treats parameters beyond its arity like any other type constructor. A more formal discussion is in our TLDI paper about System F_C(X). Manuel