[Haskell-cafe] Equality constraints in type families

[Manuel M T Chakravarty]

Claus Reinke:
>>>>> 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
>
> whereas
>
>   forall y1, y2: ConstT x y1 ~ ConstT x y2

But note that

   ConstT x ~ ConstT x

is malformed.

> 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.

Manuel