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