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
_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
