[Haskell-cafe] Re: type families and type signatures
apfelmus at quantentunnel.de
Fri Apr 11 05:22:18 EDT 2008
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
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.)
More information about the Haskell-Cafe