[Haskell-cafe] Equality constraints in type families
Manuel M T Chakravarty
chak at cse.unsw.edu.au
Mon Mar 24 22:28:27 EDT 2008
>>>>> type family F a :: * -> *
>>>> F x y ~ F u v <=> F x ~ F u /\ y ~ v
>> 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.
> i'm not sure haskell offers the kind of distinction that we
> need to talk about this: 'data constructor' is value-level,
> 'type constructor' doesn't distinguish between type- vs
> data-defined type constructors. i think i know what you
> mean, but it confuses me that you use 'data constructor'
> (should be data/newtype-defined type constructor?)
Yes, I meant to write "data type constructor".
> and 'type constructor' (don't you want to exclude
> type-defined type constructors here).
It may have been clearer if I had written data type constructor, but
then the Haskell 98 report doesn't bother with that either (so I tend
to be slack about it, too).
> data ConstD x y = ConstD x
> type ConstT x y = x
> 'ConstD x' and 'ConstT x' have the same kind, that
> of type constructors: * -> *. but:
> ConstD x y1 ~ ConstD x y2 => y1 ~ y2
> forall y1, y2: ConstT x y1 ~ ConstT x y2
But note that
ConstT x ~ ConstT x
> and i thought 'type family' was meant to suggest type
> synonym families, in contrast to 'data family'?
My nomenclature is as follows. The keywords 'type family' introduces
a "type synonym family" and 'data family' introduces a "data type
family" (or just "data family"). The term "type family" includes
both. This follows Haskell's common use of "type constructor", "type
synonym constructor", and "data type constructor".
> you did notice that i gave an example of how ghc does
> not seem to follow that decomposition rule, didn't you?
Yes, but I didn't see why you think GHC does the wrong thing.
More information about the Haskell-Cafe