[Haskell-cafe] Re: type families and type signatures
Manuel M T Chakravarty
chak at cse.unsw.edu.au
Thu Apr 10 00:32:28 EDT 2008
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
More information about the Haskell-Cafe
mailing list