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

[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". Likewise,

   bar :: forall a . Show a => Phantom a -> String

is not parametric in  a  since the result may depend on the type  a  .

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 . Every guess 
is fine. I don't think that this can be squeezed into a type 
inference/checking algorithm, though.


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

Yes of course. I just wanted to remark that the whole ambiguity stuff is 
only there because we don't (want to) have explicit type application à 
la System F(_C(X)).


Regards,
apfelmus