[Haskell-cafe] Re: type families and type signatures
apfelmus
apfelmus at quantentunnel.de
Wed Apr 9 04:45:11 EDT 2008
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
More information about the Haskell-Cafe
mailing list