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