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

[apfelmus]

Tom Schrijvers wrote:
> apfelmus wrote:
>> 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    = ..
>>  ..
> 
> But in a degenerate case there could be just this one instance:
> 
>     type instance Id x = GADT x
> 
> which then reduces this example to the GADT case of which you said that 
> is was "clearly parametric".

Manuel M T Chakravarty wrote:
> type instance Id [a] = GADT a


Oh right, just setting the instance to a GADT makes it non-parametric. 
Still, it's not the type family that is the problem, but "parametricity" 
is not the right word for that. What I want to say is that although the 
type signature

   bar :: forall a . Id a ~ b => b -> String

looks ambiguous, it is not. A trivial example of "seeming" ambiguity 
would be  (foo :: forall a . Int) . Here, parametricity tells us that 
this is not ambiguous.

The proper formulation is probably: a value  f :: forall a . t  is 
/unambiguous/ iff any choices  a1, a2  for  a  that yield the same 
static type necessarily also yield the same dynamic value

      t[a1/a] = t[a2/a]  -- types are equal
   =>  f @ a1 = f @ a2   -- values are equal

In the case of  bar , this would mean that anything not injective like

   type instance Id Int  = Int
   type instance Id Char = Int

would not change the dynamic semantics of  bar  at all, i.e.  (bar @ Int 
:: Int -> String) = (bar @ Char :: Int -> String).

I believe that this is indeed the case for  bar  and for type synonym 
families in general. (Not so for type classes, of course.)


Regards
apfelmus