[Haskell-cafe] Equality constraints in type families
Manuel M T Chakravarty
chak at cse.unsw.edu.au
Mon Mar 24 00:14:09 EDT 2008
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
More information about the Haskell-Cafe
mailing list