[Haskell-cafe] Equality constraints in type families

[Manuel M T Chakravarty]

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