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

[Manuel M T Chakravarty]

apfelmus:
> Manuel M T Chakravarty wrote:
>> apfelmus:
>>> Manuel M T Chakravarty wrote:
>>>> 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).
>
> Yes and no. In the GADT case, a function like
>
>  bar :: forall a . GADT a -> String
>
> is clearly not "parametric" in a, in the sense that pattern matching  
> on the GADT can specialize  a  which means that we have some form of  
> "pattern matching" on the type  a . The resulting String may depend  
> on the type  a . So, by "parametricity", I mean "type arguments may  
> not be inspected".
[..]
> However, I have this feeling that
>
>  bar :: forall a . Id a -> String
>
> with a type family  Id  *is* parametric in the sense that no matter  
> what  a  is, the result always has to be the same. Intuitively,  
> that's because we may not "pattern match on the branch" of a  
> definition like
>
>  type instance Id String = ..
>  type instance Id Int    = ..
>  ..
>
> So, in the special case of  foo  and  foo' , solving  Id b ~ Id a   
> by guessing  a ~ b  is safe since  foo  is parametric in  a .

We don't know that.  We could have

   type instance Id [a] = GADT a

Just looking at the signature, we don't know.

Manuel