[Haskell-cafe] Re: type families and type signatures

[Manuel M T Chakravarty]

apfelmus:
> Manuel M T Chakravarty wrote:
>> Ganesh Sittampalam:
>> Let's alpha-rename the signatures and use explicit foralls for  
>> clarity:
>>  foo  :: forall a. Id a -> Id a
>>  foo' :: forall b. Id b -> Id b
>> GHC will try to match (Id a) against (Id b).  As Id is a type  
>> synonym family, it would *not* be valid to derive (a ~ b) from  
>> this.  After all, Id could have the same result for different  
>> argument types.  (That's not the case for your one instance, but  
>> maybe in another module, there are additional instances for Id,  
>> where that is the case.)
>
> While in general  (Id a ~ Id b)  -/->  (a ~ b) , parametricity makes  
> it "true" in the case of  foo . For instance, let  Id a ~ Int .  
> Then, the signature specializes to  foo :: Int -> Int . But due to  
> parametricity,  foo  does not care at all what  a  is and will be  
> the very same function for every  a  with  Id a ~ Int . In other  
> words, it's as if the type variable  a  is not in scope in the  
> definition of  foo .

Be careful, Id is a type-indexed type family and *not* a parametric  
type.  Parametricity does not apply.  For more details about the  
situation with GADTs alone, see

   Foundations for Structured Programming with GADTs. Patricia Johann  
and Neil Ghani. Proceedings, Principles of Programming Languages 2008  
(POPL'08).

> In full System F , neither definition would be a problem since the  
> type  a  is an explicit parameter.

You can't generally translate type family/GADT programs into System  
F.  We proposed an extension of System F called System F_C(X); see our  
TLDI'07 paper:

   http://www.cse.unsw.edu.au/~chak/papers/SCPD07.html

Manuel